diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-03-21 17:13:54 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-03-21 17:13:54 +0000 |
| commit | c5315c60d2a78f9f34f9963540390f543142d488 (patch) | |
| tree | e0c6a8295ca3fd074745c88492d3a01176354a93 /proofs/clenv.mli | |
| parent | 88ff300b20833b71ec5d31fffcc766dda9aba365 (diff) | |
backtrack de l'unification
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2562 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/clenv.mli')
| -rw-r--r-- | proofs/clenv.mli | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 3f67924c7..162698112 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -56,6 +56,9 @@ type 'a clausenv = { type wc = named_context sigma (* for a better reading of the following *) val unify : constr -> tactic +val unify_0 : + Reductionops.conv_pb -> wc -> constr -> constr + -> (int * constr) list * (constr * constr) list val collect_metas : constr -> int list val mk_clenv : 'a -> constr -> 'a clausenv @@ -128,7 +131,3 @@ val pr_clenv : 'a clausenv -> Pp.std_ppcmds val abstract_list_all : Environ.env -> Evd.evar_map -> constr -> constr -> constr list -> constr -(* For debug *) -val unify_0 : - bool -> Reductionops.conv_pb -> wc -> constr -> constr - -> (int * constr) list * (constr * constr) list |