From 896dae9d436cb366c3f7fc3d608b0f834e5b168f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 27 Jun 2019 14:36:02 +0200
Subject: [PATCH] [wp] linting files
---
src/plugins/qed/logic.ml | 2 +-
src/plugins/wp/Lang.mli | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/plugins/qed/logic.ml b/src/plugins/qed/logic.ml
index 5aec0a471c1..83ed15378f0 100644
--- a/src/plugins/qed/logic.ml
+++ b/src/plugins/qed/logic.ml
@@ -308,7 +308,7 @@ sig
val e_open : pool:pool -> ?forall:bool -> ?exists:bool -> ?lambda:bool ->
term -> (binder * var) list * term
- (** Open all the specified binders (flags default to `true`, so all
+ (** Open all the specified binders (flags default to `true`, so all
consecutive top most binders are opened by default).
The pool must contain all free variables of the term. *)
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index 8e8e8951949..d02b68cdb98 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -295,7 +295,7 @@ sig
val e_open : pool:pool -> ?forall:bool -> ?exists:bool -> ?lambda:bool ->
term -> (binder * var) list * term
- (** Open all the specified binders (flags default to `true`, so all
+ (** Open all the specified binders (flags default to `true`, so all
consecutive top most binders are opened by default).
The pool must contain all free variables of the term. *)
--
GitLab