diff options
| author | herbelin | 2008-10-18 15:57:24 +0000 |
|---|---|---|
| committer | herbelin | 2008-10-18 15:57:24 +0000 |
| commit | 8cf4e04fa817cf7ff9d73cb5cb7fff8b3b950387 (patch) | |
| tree | 30fbd47a7c79a0bc4e5d8a94db78294e6b62b02f /pretyping/clenv.mli | |
| parent | 41dcb1603ea2e212a9167918f3d5dcb6f166e27b (diff) | |
Optimisation de clenv.ml pour que meta_instance ne soit pas appelé
abusivement sur les clauses.
Nettoyage au passage de metamap qui était utilisé à la fois pour les
substitutions de meta et pour les contextes de typage de meta.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11467 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/clenv.mli')
| -rw-r--r-- | pretyping/clenv.mli | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index dfa7513495..de5a1e3758 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -43,10 +43,16 @@ val subst_clenv : substitution -> clausenv -> clausenv (* subject of clenv (instantiated) *) val clenv_value : clausenv -> constr +(* subject of clenv (assume it is pre-instantiated) *) +val clenv_direct_value : clausenv -> constr (* type of clenv (instantiated) *) val clenv_type : clausenv -> types +(* type of clenv (assume it is pre-instantiated) *) +val clenv_direct_nf_type : clausenv -> types (* substitute resolved metas *) val clenv_nf_meta : clausenv -> constr -> constr +(* substitute resolved metas (assume the metas in clausenv are expanded) *) +val clenv_direct_nf_meta : clausenv -> constr -> constr (* type of a meta in clenv context *) val clenv_meta_type : clausenv -> metavariable -> types @@ -83,6 +89,8 @@ val clenv_dependent : bool -> clausenv -> metavariable list val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv +val clenv_expand_metas : clausenv -> clausenv + (***************************************************************) (* Bindings *) |