From ae9f6d13b63f30168d2eaa2289108a117ad840f7 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 7 Sep 2016 18:51:52 +0200 Subject: Unplugging Tacexpr in several interface files. --- lib/future.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib/future.mli') 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 -- cgit v1.2.3