diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-03-20 14:53:21 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-03-20 14:53:21 +0000 |
| commit | 4f8c17c83c53d7fd857eccfc7e9de4e4df627fbd (patch) | |
| tree | 2da62f53237a1d4f1f1844768836744e3d8d83bd /proofs/clenv.mli | |
| parent | 34ce92b048ee33d78f40b661da5e35db782bcce5 (diff) | |
encore quelques petites modif de l'unification
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2553 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/clenv.mli')
| -rw-r--r-- | proofs/clenv.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 162698112..3f67924c7 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -56,9 +56,6 @@ 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 @@ -131,3 +128,7 @@ 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 |