From 4f8c17c83c53d7fd857eccfc7e9de4e4df627fbd Mon Sep 17 00:00:00 2001
From: barras
Date: Wed, 20 Mar 2002 14:53:21 +0000
Subject: 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
---
 proofs/clenv.mli | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'proofs/clenv.mli')

diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 162698112c..3f67924c72 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
-- 
cgit v1.2.3