diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-12 11:38:09 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-12 11:38:09 +0000 |
| commit | 34bc13e0ef3642244fe77fe8a8a7869fbc8d2fca (patch) | |
| tree | 1b681cce520d8ba260651969ee96d0fb313ef166 /pretyping/unification.mli | |
| parent | 5cd3851617123736fafa3b81688bb63d850b9dd4 (diff) | |
inclusion de meta_map dans evar_defs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6099 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/unification.mli')
| -rw-r--r-- | pretyping/unification.mli | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 02d1918be..d3007e69d 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -18,19 +18,19 @@ open Evd open Evarutil (*i*) -type maps = evar_defs * meta_map - -val w_Declare : env -> evar -> types -> maps -> maps -val w_Define : evar -> constr -> maps -> maps +val w_Declare : env -> evar -> types -> evar_defs -> evar_defs +val w_Define : evar -> constr -> evar_defs -> evar_defs (* The "unique" unification fonction *) val w_unify : - bool -> env -> Reductionops.conv_pb -> constr -> constr -> maps -> maps + bool -> env -> Reductionops.conv_pb -> constr -> constr -> + evar_defs -> evar_defs (* [w_unify_to_subterm env (c,t) m] performs unification of [c] with a subterm of [t]. Constraints are added to [m] and the matched subterm of [t] is also returned. *) -val w_unify_to_subterm : env -> constr * constr -> maps -> maps * constr +val w_unify_to_subterm : + env -> constr * constr -> evar_defs -> evar_defs * constr (*i This should be in another module i*) |