aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-09-07 18:51:52 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-09-08 16:55:46 +0200
commitae9f6d13b63f30168d2eaa2289108a117ad840f7 (patch)
treed937467dd5c1913960d58932df19853c93675acb /lib
parentdfac5aa2285de5b89f08ada3c30c0a1594737440 (diff)
Unplugging Tacexpr in several interface files.
Diffstat (limited to 'lib')
-rw-r--r--lib/future.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/future.mli b/lib/future.mli
index 114c59176..c780faf32 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -87,7 +87,7 @@ val from_val : ?fix_exn:fix_exn -> 'a -> 'a computation
the value is not just the 'a but also the global system state *)
val from_here : ?fix_exn:fix_exn -> 'a -> 'a computation
-(* To get the fix_exn of a computation and build a Tacexpr.declaration_hook.
+(* To get the fix_exn of a computation and build a Lemmas.declaration_hook.
* When a future enters the environment a corresponding hook is run to perform
* some work. If this fails, then its failure has to be annotated with the
* same state id that corresponds to the future computation end. I.e. Qed