diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-25 17:27:34 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-25 17:27:34 +0000 |
| commit | ef2c3cc02409949f19c70903a86a8181f4ed03e7 (patch) | |
| tree | a731973d524c608b11944325895f77e883e733a7 /kernel/environ.mli | |
| parent | f99c2ac25b8d4582b509063f0386fb5d445bd86f (diff) | |
First attempt at making Print Assumption compatible with opaque modules (fix #2168)
We replace Global.lookup_constant by our own code that looks for a module
and enters its implementation. This is still preliminary work, I would prefer
to understand more completely the part about module substitutions when
entering an applied functor. But this code already appears to work quite well.
Anyway, since we only search for constants, we don't need to reconstitute a
100% accurate environment, as long as the same objects are in it.
Note:
- Digging inside module structures is slower than just using
Global.lookup_constant. Hence we try to avoid it as long as we could.
Only in front of axioms (or in front of constant unknown to Global)
do we check whether we have an inner-module implementation for this
constant. There is some memoization of the search for internal
structure_body out of a module_path.
- In case of inner-module axioms, we might not be able to print
its type, but only its long name.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14600 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 17 |
1 files changed, 0 insertions, 17 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index af1e17591..aa6f52128 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -228,20 +228,3 @@ val unregister : env -> field -> env val register : env -> field -> Retroknowledge.entry -> env - -(** a few declarations for the "Print Assumption" command - @author spiwack *) -type context_object = - | Variable of identifier (** A section variable or a Let definition *) - | Axiom of constant (** An axiom or a constant. *) - | Opaque of constant (** An opaque constant. *) - -(** AssumptionSet.t is a set of [assumption] *) -module OrderedContextObject : Set.OrderedType with type t = context_object -module ContextObjectMap : Map.S with type key = context_object - -(** collects all the assumptions (optionally including opaque definitions) - on which a term relies (together with their type) *) -val assumptions : ?add_opaque:bool -> transparent_state -> constr -> env -> Term.types ContextObjectMap.t - - |