aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-09-16 13:54:13 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-09-16 13:54:13 +0200
commit978dd21af8467aa483bce551b3d5df8895cfff0f (patch)
tree41f473bddf855d3daf179c83ed63166834ae3240 /lib
parent89f7bc53fbd558e3b5ff2ce1d1693f570afcc536 (diff)
parent7bd00a63015c4017d8209a4d495b9683d33d1d53 (diff)
Make the Coq codebase independent from Ltac-related code.
We untangle many dependencies on Ltac datastructures and modules from the lower strata, resulting in a self-contained ltac/ folder. While not a plugin yet, the change is now very easy to perform. The main API changes have been documented in the dev/doc/changes file. The patches are quite rough, and it may be the case that some parts of the code can migrate back from ltac/ to a core folder. This should be decided on a case-by-case basis, according to a more long-term consideration of what is exactly Ltac-dependent and whatnot.
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