suite du commit precedent

- amelioration des messages d'erreurs de la condition de garde
- reorganisation de clenv.ml


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3457 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 336 insertions, 354 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 40060165e0..83aa907514 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -70,219 +70,11 @@ let exist_to_meta sigma (emap, c) =
       | _ -> map_constr replace c in
   (!metamap, replace c)
 
+
 type 'a freelisted = {
   rebus : 'a;
   freemetas : Intset.t }
 
-type clbinding = 
-  | Cltyp of constr freelisted
-  | Clval of constr freelisted * constr freelisted
-
-type 'a clausenv = {
-  templval : constr freelisted;
-  templtyp : constr freelisted;
-  namenv : identifier Intmap.t;
-  env : clbinding Intmap.t;
-  hook : 'a }
-
-let applyHead n c wc = 
-  let rec apprec n c cty wc =
-    if n = 0 then 
-      (wc,c)
-    else 
-      match kind_of_term (w_whd_betadeltaiota wc cty) with
-        | Prod (_,c1,c2) ->
-	    let evar = Evarutil.new_evar_in_sign (w_env wc) in
-            let (evar_n, _) = destEvar evar in
-	    (compose 
-	       (apprec (n-1) (applist(c,[evar])) (subst1 evar c2))
-	       (w_Declare evar_n c1))
-	    wc
-	| _ -> error "Apply_Head_Then"
-  in 
-  apprec n c (w_type_of wc c) wc
-
-let mimick_evar hdc nargs sp wc =
-  let evd = Evd.map wc.sigma sp in
-  let wc' = extract_decl sp wc in
-  let (wc'', c) = applyHead nargs hdc wc' in
-    if wc'==wc''
-    then w_Define sp c wc
-    else 
-      let wc''' = restore_decl sp evd wc'' in
-	w_Define sp c {it = wc.it ; sigma = wc'''.sigma}
-
-(*  (w_Focusing_THEN sp
-     (applyHead nargs hdc)
-     (fun c wc -> w_Define sp c wc)) wc *)
-
-
-(* Unification à l'ordre 0 de m et n: [unify_0 mc wc m n] renvoie deux listes:
-
-   metasubst:(int*constr)list    récolte les instances des (Meta k)
-   evarsubst:(constr*constr)list récolte les instances des (Const "?k")
-
-   Attention : pas d'unification entre les différences instances d'une
-   même meta ou evar, il peut rester des doublons *)
-
-(* Unification order: *)
-(* Left to right: unifies first argument and then the other arguments *)
-let unify_l2r x = List.rev x
-(* Right to left: unifies last argument and then the other arguments *)
-let unify_r2l x = x
-
-let sort_eqns = unify_r2l
-
-
-let unify_0 cv_pb wc m n =
-  let env = w_env wc
-  and sigma = w_Underlying wc in
-  let trivial_unify pb substn m n =
-    if (not(occur_meta m)) & is_fconv pb env sigma m n then substn
-    else error_cannot_unify (m,n) in
-  let rec unirec_rec pb ((metasubst,evarsubst) as substn) m n =
-    let cM = Evarutil.whd_castappevar sigma m
-    and cN = Evarutil.whd_castappevar sigma n in 
-    match (kind_of_term cM,kind_of_term cN) with
-      | Meta k1, Meta k2 ->
-	  if k1 < k2 then (k1,cN)::metasubst,evarsubst
-	  else if k1 = k2 then substn
-	  else (k2,cM)::metasubst,evarsubst
-      | Meta k, _    -> (k,cN)::metasubst,evarsubst
-      | _, Meta k    -> (k,cM)::metasubst,evarsubst
-      | Evar _, _ -> metasubst,((cM,cN)::evarsubst)
-      | _, Evar _ -> metasubst,((cN,cM)::evarsubst)
-
-      | Lambda (_,t1,c1), Lambda (_,t2,c2) ->
-	  unirec_rec CONV (unirec_rec CONV substn t1 t2) c1 c2
-      | Prod (_,t1,c1), Prod (_,t2,c2) ->
-	  unirec_rec pb (unirec_rec CONV substn t1 t2) c1 c2
-      | LetIn (_,b,_,c), _ -> unirec_rec pb substn (subst1 b c) cN
-      | _, LetIn (_,b,_,c) -> unirec_rec pb substn cM (subst1 b c)
-
-      | App (f1,l1), App (f2,l2) ->
-	  let len1 = Array.length l1
-	  and len2 = Array.length l2 in
-          let (f1,l1,f2,l2) =
-	    if len1 = len2 then (f1,l1,f2,l2)
-	    else if len1 < len2 then
-              let extras,restl2 = array_chop (len2-len1) l2 in 
-              (f1, l1, appvect (f2,extras), restl2)
-	    else 
-	      let extras,restl1 = array_chop (len1-len2) l1 in 
-              (appvect (f1,extras), restl1, f2, l2) in
-          (try
-            array_fold_left2 (unirec_rec CONV)
-	      (unirec_rec CONV substn f1 f2) l1 l2
-	  with ex when catchable_exception ex ->
-            trivial_unify pb substn cM cN)
-      | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
-          array_fold_left2 (unirec_rec CONV)
-	    (unirec_rec CONV (unirec_rec CONV substn p1 p2) c1 c2) cl1 cl2
-
-      | _ -> trivial_unify pb substn cM cN
-
-  in
-  if (not(occur_meta m)) & is_fconv cv_pb env sigma m n then 
-    ([],[])
-  else 
-    let (mc,ec) = unirec_rec cv_pb ([],[]) m n in
-    (sort_eqns mc, sort_eqns ec)
-
-
-(* Unification
- *
- * Procedure:
- * (1) The function [unify mc wc M N] produces two lists:
- *     (a) a list of bindings Meta->RHS
- *     (b) a list of bindings EVAR->RHS
- *
- * The Meta->RHS bindings cannot themselves contain
- * meta-vars, so they get applied eagerly to the other
- * bindings.  This may or may not close off all RHSs of
- * the EVARs.  For each EVAR whose RHS is closed off,
- * we can just apply it, and go on.  For each which
- * is not closed off, we need to do a mimick step -
- * in general, we have something like:
- *
- *      ?X == (c e1 e2 ... ei[Meta(k)] ... en)
- *
- * so we need to do a mimick step, converting ?X
- * into
- *
- *      ?X -> (c ?z1 ... ?zn)
- *
- * of the proper types.  Then, we can decompose the
- * equation into
- *
- *      ?z1 --> e1
- *          ...
- *      ?zi --> ei[Meta(k)]
- *          ...
- *      ?zn --> en
- *
- * and keep on going.  Whenever we find that a R.H.S.
- * is closed, we can, as before, apply the constraint
- * directly.  Whenever we find an equation of the form:
- *
- *      ?z -> Meta(n)
- *
- * we can reverse the equation, put it into our metavar
- * substitution, and keep going.
- *
- * The most efficient mimick possible is, for each
- * Meta-var remaining in the term, to declare a
- * new EVAR of the same type.  This is supposedly
- * determinable from the clausale form context -
- * we look up the metavar, take its type there,
- * and apply the metavar substitution to it, to
- * close it off.  But this might not always work,
- * since other metavars might also need to be resolved. *)
-
-let rec w_Unify cv_pb m n wc =
-  let (mc',ec') = unify_0 cv_pb wc m n in 
-  w_resrec mc' ec' wc
-
-and w_resrec metas evars wc =
-  match evars with
-    | [] -> (wc,metas)
-
-    | (lhs,rhs) :: t ->
-    match kind_of_term rhs with
-
-      | Meta k -> w_resrec ((k,lhs)::metas) t wc
-
-      | krhs ->
-      match kind_of_term lhs with
-
-	| Evar (evn,_) ->
-	    if w_defined_evar wc evn then
-	      let (wc',metas') = w_Unify CONV rhs lhs wc in 
-	      w_resrec (metas@metas') t wc'
-	    else
-	      (try 
-		 w_resrec metas t (w_Define evn rhs wc)
-               with ex when catchable_exception ex ->
-		 (match krhs with
-             	    | App (f,cl) when isConst f ->
-			let wc' = mimick_evar f (Array.length cl) evn wc in
-			w_resrec metas evars wc'
-		    | _ -> error "w_Unify"))
-	| _ -> anomaly "w_resrec"
-
-
-(* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
-   particulier ne semblent pas vérifier que des instances différentes
-   d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas
-   provenant de w_Unify. (Utilisé seulement dans prolog.ml) *)
-
-(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
-let unifyTerms m n gls = 
-  tclIDTAC {it = gls.it; 
-	    sigma = (get_gc (fst (w_Unify CONV m n (Refiner.project_with_focus gls))))}
-
-let unify m gls =
-  let n = pf_concl gls in unifyTerms m n gls
 
 (* collects all metavar occurences, in left-to-right order, preserving
  * repetitions and all. *)
@@ -306,6 +98,23 @@ let metavars_of c =
 let mk_freelisted c =
   { rebus = c; freemetas = metavars_of c }
 
+
+(* Clausal environments *)
+
+type clbinding = 
+  | Cltyp of constr freelisted
+  | Clval of constr freelisted * constr freelisted
+
+type 'a clausenv = {
+  templval : constr freelisted;
+  templtyp : constr freelisted;
+  namenv : identifier Intmap.t;
+  env : clbinding Intmap.t;
+  hook : 'a }
+
+type wc = named_context sigma
+
+
 (* [mentions clenv mv0 mv1] is true if mv1 is defined and mentions
  * mv0, or if one of the free vars on mv1's freelist mentions
  * mv0 *)
@@ -390,13 +199,7 @@ let subst_clenv f sub clenv =
     env = Intmap.map (map_clb (subst_mps sub)) clenv.env;
     hook = f sub clenv.hook }
 
-
-let connect_clenv wc clenv =
-  { templval = clenv.templval;
-    templtyp = clenv.templtyp;
-    namenv = clenv.namenv;
-    env = clenv.env;
-    hook = wc }
+let connect_clenv wc clenv = { clenv with hook = wc }
 
 (* Changes the head of a clenv with (templ,templty) *)
 let clenv_change_head (templ,templty) clenv =
@@ -573,6 +376,202 @@ let clenv_type_of ce c =
 let clenv_instance_type_of ce c =
   clenv_instance ce (mk_freelisted (clenv_type_of ce c))
 
+
+
+(* Unification à l'ordre 0 de m et n: [unify_0 mc wc m n] renvoie deux listes:
+
+   metasubst:(int*constr)list    récolte les instances des (Meta k)
+   evarsubst:(constr*constr)list récolte les instances des (Const "?k")
+
+   Attention : pas d'unification entre les différences instances d'une
+   même meta ou evar, il peut rester des doublons *)
+
+(* Unification order: *)
+(* Left to right: unifies first argument and then the other arguments *)
+let unify_l2r x = List.rev x
+(* Right to left: unifies last argument and then the other arguments *)
+let unify_r2l x = x
+
+let sort_eqns = unify_r2l
+
+
+let unify_0 cv_pb wc m n =
+  let env = w_env wc
+  and sigma = w_Underlying wc in
+  let trivial_unify pb substn m n =
+    if (not(occur_meta m)) & is_fconv pb env sigma m n then substn
+    else error_cannot_unify (m,n) in
+  let rec unirec_rec pb ((metasubst,evarsubst) as substn) m n =
+    let cM = Evarutil.whd_castappevar sigma m
+    and cN = Evarutil.whd_castappevar sigma n in 
+    match (kind_of_term cM,kind_of_term cN) with
+      | Meta k1, Meta k2 ->
+	  if k1 < k2 then (k1,cN)::metasubst,evarsubst
+	  else if k1 = k2 then substn
+	  else (k2,cM)::metasubst,evarsubst
+      | Meta k, _    -> (k,cN)::metasubst,evarsubst
+      | _, Meta k    -> (k,cM)::metasubst,evarsubst
+      | Evar _, _ -> metasubst,((cM,cN)::evarsubst)
+      | _, Evar _ -> metasubst,((cN,cM)::evarsubst)
+
+      | Lambda (_,t1,c1), Lambda (_,t2,c2) ->
+	  unirec_rec CONV (unirec_rec CONV substn t1 t2) c1 c2
+      | Prod (_,t1,c1), Prod (_,t2,c2) ->
+	  unirec_rec pb (unirec_rec CONV substn t1 t2) c1 c2
+      | LetIn (_,b,_,c), _ -> unirec_rec pb substn (subst1 b c) cN
+      | _, LetIn (_,b,_,c) -> unirec_rec pb substn cM (subst1 b c)
+
+      | App (f1,l1), App (f2,l2) ->
+	  let len1 = Array.length l1
+	  and len2 = Array.length l2 in
+          let (f1,l1,f2,l2) =
+	    if len1 = len2 then (f1,l1,f2,l2)
+	    else if len1 < len2 then
+              let extras,restl2 = array_chop (len2-len1) l2 in 
+              (f1, l1, appvect (f2,extras), restl2)
+	    else 
+	      let extras,restl1 = array_chop (len1-len2) l1 in 
+              (appvect (f1,extras), restl1, f2, l2) in
+          (try
+            array_fold_left2 (unirec_rec CONV)
+	      (unirec_rec CONV substn f1 f2) l1 l2
+	  with ex when catchable_exception ex ->
+            trivial_unify pb substn cM cN)
+      | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
+          array_fold_left2 (unirec_rec CONV)
+	    (unirec_rec CONV (unirec_rec CONV substn p1 p2) c1 c2) cl1 cl2
+
+      | _ -> trivial_unify pb substn cM cN
+
+  in
+  if (not(occur_meta m)) & is_fconv cv_pb env sigma m n then 
+    ([],[])
+  else 
+    let (mc,ec) = unirec_rec cv_pb ([],[]) m n in
+    (sort_eqns mc, sort_eqns ec)
+
+
+(* Unification
+ *
+ * Procedure:
+ * (1) The function [unify mc wc M N] produces two lists:
+ *     (a) a list of bindings Meta->RHS
+ *     (b) a list of bindings EVAR->RHS
+ *
+ * The Meta->RHS bindings cannot themselves contain
+ * meta-vars, so they get applied eagerly to the other
+ * bindings.  This may or may not close off all RHSs of
+ * the EVARs.  For each EVAR whose RHS is closed off,
+ * we can just apply it, and go on.  For each which
+ * is not closed off, we need to do a mimick step -
+ * in general, we have something like:
+ *
+ *      ?X == (c e1 e2 ... ei[Meta(k)] ... en)
+ *
+ * so we need to do a mimick step, converting ?X
+ * into
+ *
+ *      ?X -> (c ?z1 ... ?zn)
+ *
+ * of the proper types.  Then, we can decompose the
+ * equation into
+ *
+ *      ?z1 --> e1
+ *          ...
+ *      ?zi --> ei[Meta(k)]
+ *          ...
+ *      ?zn --> en
+ *
+ * and keep on going.  Whenever we find that a R.H.S.
+ * is closed, we can, as before, apply the constraint
+ * directly.  Whenever we find an equation of the form:
+ *
+ *      ?z -> Meta(n)
+ *
+ * we can reverse the equation, put it into our metavar
+ * substitution, and keep going.
+ *
+ * The most efficient mimick possible is, for each
+ * Meta-var remaining in the term, to declare a
+ * new EVAR of the same type.  This is supposedly
+ * determinable from the clausale form context -
+ * we look up the metavar, take its type there,
+ * and apply the metavar substitution to it, to
+ * close it off.  But this might not always work,
+ * since other metavars might also need to be resolved. *)
+
+let applyHead n c wc = 
+  let rec apprec n c cty wc =
+    if n = 0 then 
+      (wc,c)
+    else 
+      match kind_of_term (w_whd_betadeltaiota wc cty) with
+        | Prod (_,c1,c2) ->
+	    let evar = Evarutil.new_evar_in_sign (w_env wc) in
+            let (evar_n, _) = destEvar evar in
+	    (compose 
+	       (apprec (n-1) (applist(c,[evar])) (subst1 evar c2))
+	       (w_Declare evar_n c1))
+	    wc
+	| _ -> error "Apply_Head_Then"
+  in 
+  apprec n c (w_type_of wc c) wc
+
+let mimick_evar hdc nargs sp wc =
+  let evd = Evd.map wc.sigma sp in
+  let wc' = extract_decl sp wc in
+  let (wc'', c) = applyHead nargs hdc wc' in
+    if wc'==wc''
+    then w_Define sp c wc
+    else 
+      let wc''' = restore_decl sp evd wc'' in
+	w_Define sp c {it = wc.it ; sigma = wc'''.sigma}
+
+let rec w_Unify cv_pb m n wc =
+  let (mc',ec') = unify_0 cv_pb wc m n in 
+  w_resrec mc' ec' wc
+
+and w_resrec metas evars wc =
+  match evars with
+    | [] -> (wc,metas)
+
+    | (lhs,rhs) :: t ->
+    match kind_of_term rhs with
+
+      | Meta k -> w_resrec ((k,lhs)::metas) t wc
+
+      | krhs ->
+      match kind_of_term lhs with
+
+	| Evar (evn,_) ->
+	    if w_defined_evar wc evn then
+	      let (wc',metas') = w_Unify CONV rhs lhs wc in 
+	      w_resrec (metas@metas') t wc'
+	    else
+	      (try 
+		 w_resrec metas t (w_Define evn rhs wc)
+               with ex when catchable_exception ex ->
+		 (match krhs with
+             	    | App (f,cl) when isConst f ->
+			let wc' = mimick_evar f (Array.length cl) evn wc in
+			w_resrec metas evars wc'
+		    | _ -> error "w_Unify"))
+	| _ -> anomaly "w_resrec"
+
+
+(* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
+   particulier ne semblent pas vérifier que des instances différentes
+   d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas
+   provenant de w_Unify. (Utilisé seulement dans prolog.ml) *)
+
+(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
+let unifyTerms m n gls = 
+  tclIDTAC {it = gls.it; 
+	    sigma = (get_gc (fst (w_Unify CONV m n (Refiner.project_with_focus gls))))}
+
+let unify m gls =
+  let n = pf_concl gls in unifyTerms m n gls
+
 (* [clenv_merge b metas evars clenv] merges common instances in metas
    or in evars, possibly generating new unification problems; if [b]
    is true, unification of types of metas is required *)
@@ -1007,6 +1006,36 @@ let clenv_match_args s clause =
   in 
   matchrec clause s
 
+type arg_bindings = (int * constr) list
+
+let clenv_constrain_with_bindings bl clause =
+  if bl = [] then 
+    clause 
+  else 
+    let all_mvs = collect_metas (clenv_template clause).rebus in
+    let rec matchrec clause = function
+      | []       -> clause
+      | (n,c)::t ->
+          let k = 
+            (try
+              if n > 0 then 
+		List.nth all_mvs (n-1)
+              else if n < 0 then 
+		List.nth (List.rev all_mvs) (-n-1)
+              else error "clenv_constrain_with_bindings" 
+            with Failure _ ->
+              errorlabstrm "clenv_constrain_with_bindings"
+                (str"Clause did not have " ++ int n ++ str"-th" ++
+                str" absolute argument")) in
+	  let env = Global.env () in
+	  let sigma = Evd.empty in
+	  let k_typ = nf_betaiota (clenv_instance_type clause k) in
+	  let c_typ = nf_betaiota (w_type_of clause.hook c) in 
+	  matchrec
+            (clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause)) t
+    in 
+    matchrec clause bl
+
 
 (* [clenv_pose_dependent_evars clenv]
  * For each dependent evar in the clause-env which does not have a value,
@@ -1026,13 +1055,6 @@ let clenv_pose_dependent_evars clenv =
     clenv
     dep_mvs
 
-let clenv_add_sign (id,sign) clenv =
-  { templval = clenv.templval;
-    templtyp = clenv.templtyp;
-    namenv = clenv.namenv;
-    env = clenv.env;
-    hook = w_add_sign (id,sign) clenv.hook}
-
 (***************************)
 
 let clenv_unique_resolver allow_K clause gl =
@@ -1048,6 +1070,10 @@ let res_pf_cast kONT clenv gls =
 let elim_res_pf kONT clenv gls =
   clenv_refine_cast kONT (clenv_unique_resolver true clenv gls) gls
 
+let elim_res_pf_THEN_i kONT clenv tac gls =  
+  let clenv' = (clenv_unique_resolver true clenv gls) in
+  tclTHENLASTn (clenv_refine kONT clenv') (tac clenv') gls
+
 let e_res_pf kONT clenv gls =
   clenv_refine kONT
     (clenv_pose_dependent_evars (clenv_unique_resolver false clenv gls)) gls
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index efd8dc302c..c056c3b2c8 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -13,9 +13,7 @@ open Util
 open Names
 open Term
 open Sign
-open Tacmach
 open Proof_type
-open Evar_refiner
 (*i*)
 
 (* [new_meta] is a generator of unique meta variables *)
@@ -44,6 +42,8 @@ type 'a clausenv = {
   env : clbinding Intmap.t;
   hook : 'a }
 
+type wc = named_context sigma (* for a better reading of the following *)
+
 (* [templval] is the template which we are trying to fill out.
  * [templtyp] is its type.
  * [namenv] is a mapping from metavar numbers to names, for
@@ -53,11 +53,6 @@ type 'a clausenv = {
  * [hook] is the pointer to the current walking context, for
  *        integrating existential vars and metavars. *)
 
-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
 val mk_clenv_from : 'a -> constr * constr -> 'a clausenv
@@ -80,14 +75,24 @@ val clenv_template_type : 'a clausenv -> constr freelisted
 val clenv_instance_type : wc clausenv -> int -> constr
 val clenv_instance_template : wc clausenv -> constr
 val clenv_instance_template_type : wc clausenv -> constr
+val clenv_type_of : wc clausenv -> constr -> constr
+val clenv_fchain : int -> 'a clausenv -> wc clausenv -> wc clausenv
+val clenv_bchain : int -> 'a clausenv -> wc clausenv -> wc clausenv
+
+(* Unification with clenv *)
+type arg_bindings = (int * constr) list
+
+val unify_0 : 
+  Reductionops.conv_pb -> wc -> constr -> constr 
+    -> (int * constr) list * (constr * constr) list
 val clenv_unify : 
   bool -> Reductionops.conv_pb -> constr -> constr ->
   wc clausenv -> wc clausenv
-val clenv_fchain : int -> 'a clausenv -> wc clausenv -> wc clausenv
-val clenv_refine : (wc -> tactic) -> wc clausenv -> tactic
-val res_pf      : (wc -> tactic) -> wc clausenv -> tactic
-val res_pf_cast : (wc -> tactic) -> wc clausenv -> tactic
-val elim_res_pf : (wc -> tactic) -> wc clausenv -> tactic
+val clenv_match_args :
+  constr Rawterm.explicit_substitution -> wc clausenv -> wc clausenv
+val clenv_constrain_with_bindings : arg_bindings -> wc clausenv -> wc clausenv
+
+(* Bindings *)
 val clenv_independent : wc clausenv -> int list
 val clenv_missing : 'a clausenv -> int list
 val clenv_constrain_missing_args : (* Used in user contrib Lannion *)
@@ -96,21 +101,27 @@ val clenv_constrain_missing_args : (* Used in user contrib Lannion *)
 val clenv_constrain_dep_args : constr list -> wc clausenv -> wc clausenv
 *)
 val clenv_lookup_name : 'a clausenv -> identifier -> int
-val clenv_match_args : constr Rawterm.explicit_substitution -> wc clausenv -> wc clausenv
-val e_res_pf : (wc -> tactic) -> wc clausenv -> tactic
-val clenv_type_of : wc clausenv -> constr -> constr
 val clenv_unique_resolver : bool -> wc clausenv -> goal sigma -> wc clausenv
 
 val make_clenv_binding_apply :
-  named_context sigma -> int -> constr * constr ->
-      types Rawterm.substitution -> named_context sigma clausenv
+  wc -> int -> constr * constr -> types Rawterm.substitution -> wc clausenv
 val make_clenv_binding :
-  named_context sigma -> constr * constr ->
-      types Rawterm.substitution -> named_context sigma clausenv
+  wc -> constr * constr -> types Rawterm.substitution -> wc clausenv
+
+(* Tactics *)
+val unify : constr -> tactic
+val clenv_refine : (wc -> tactic) -> wc clausenv -> tactic
+val res_pf      : (wc -> tactic) -> wc clausenv -> tactic
+val res_pf_cast : (wc -> tactic) -> wc clausenv -> tactic
+val elim_res_pf : (wc -> tactic) -> wc clausenv -> tactic
+val e_res_pf : (wc -> tactic) -> wc clausenv -> tactic
+val elim_res_pf_THEN_i : 
+  (wc -> tactic) -> wc clausenv -> (wc clausenv -> tactic array) -> tactic
+
+(* Pretty-print *)
+val pr_clenv : 'a clausenv -> Pp.std_ppcmds
 
-(* Exported for program.ml only *)
-val clenv_add_sign : 
-  (identifier * types) -> wc clausenv -> wc clausenv
+(* Exported for debugging *)
 val unify_to_subterm : 
   wc clausenv -> constr * constr -> wc clausenv * constr
 val unify_to_subterm_list : 
@@ -118,12 +129,9 @@ val unify_to_subterm_list :
 val clenv_typed_unify :
   Reductionops.conv_pb -> constr -> constr -> wc clausenv -> wc clausenv
 
-val pr_clenv : 'a clausenv -> Pp.std_ppcmds
-
 (*i This should be in another module i*)
 
 (* [abstract_list_all env sigma t c l]                     *)
 (* abstracts the terms in l over c to get a term of type t *)
 val abstract_list_all :
   Environ.env -> Evd.evar_map -> constr -> constr -> constr list -> constr
-
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 6edf56017b..fcc1884caf 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -290,7 +290,7 @@ let lemInv id c gls =
   try
     let (wc,kONT) = startWalk gls in
     let clause = mk_clenv_type_of wc c in
-    let clause = clenv_constrain_with_bindings [(Abs (-1),mkVar id)] clause in
+    let clause = clenv_constrain_with_bindings [(-1,mkVar id)] clause in
     res_pf kONT clause gls
   with 
 (* Ce n'est pas l'endroit pour cela
diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml
index 78f3890c5f..f5723fe368 100644
--- a/tactics/wcclausenv.ml
+++ b/tactics/wcclausenv.ml
@@ -29,8 +29,6 @@ open Evar_refiner
    write to Eduardo.Gimenez@inria.fr and ask for the prize :-)
    -- Eduardo (11/8/97) *)
 
-type wc = named_context sigma
-
 let pf_get_new_id id gls = 
   next_ident_away id (pf_ids_of_hyps gls)
 
@@ -40,73 +38,10 @@ let pf_get_new_ids ids gls =
     (fun id acc -> (next_ident_away id (acc@avoid))::acc)
     ids []
 
-type arg_binder =
-  | Dep of identifier
-  | Nodep of int
-  | Abs of int
-
-type arg_bindings = (arg_binder * constr) list
-
-let clenv_constrain_with_bindings bl clause =
-  if bl = [] then 
-    clause 
-  else 
-    let all_mvs = collect_metas (clenv_template clause).rebus
-    and ind_mvs = clenv_independent clause in
-    let nb_indep = List.length ind_mvs in
-    let rec matchrec clause = function
-      | []       -> clause
-      | (b,c)::t ->
-          let k = 
-            match b with
-              | Dep s ->
-		  if List.mem_assoc b t then 
-		    errorlabstrm "clenv_match_args" 
-                      (str "The variable " ++ pr_id s ++ 
-			 str " occurs more than once in binding");
-		  clenv_lookup_name clause s
-              | Nodep n ->
-		  let index = if n > 0 then n-1 else nb_indep+n in
-                  if List.mem_assoc (Nodep (index+1)) t or 
-                    List.mem_assoc (Nodep (index-nb_indep)) t
-                  then errorlabstrm "clenv_match_args"
-                    (str "The position " ++ int n ++
-		       str " occurs more than once in binding");
-		  (try 
-		     List.nth ind_mvs index
-		   with Failure _ ->
-                     errorlabstrm "clenv_constrain_with_bindings"
-                       (str"Clause did not have " ++ int n ++ str"-th" ++
-                          str" unnamed argument"))
-              | Abs n -> 
-                  (try
-                     if n > 0 then 
-		       List.nth all_mvs (n-1)
-                     else if n < 0 then 
-		       List.nth (List.rev all_mvs) (-n-1)
-                     else error "clenv_constrain_with_bindings" 
-                   with Failure _ ->
-                     errorlabstrm "clenv_constrain_with_bindings"
-                       (str"Clause did not have " ++ int n ++ str"-th" ++
-                          str" absolute argument"))
-	  in
-	  let env = Global.env () in
-	  let sigma = Evd.empty in
-	  let k_typ = nf_betaiota (clenv_instance_type clause k) in
-	  let c_typ = nf_betaiota (w_type_of clause.hook c) in 
-	  matchrec
-            (clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause)) t
-    in 
-    matchrec clause bl
-
 (* What follows is part of the contents of the former file tactics3.ml *)
 (* 2/2002: replaced THEN_i by THENSLAST to solve a bug in
    Tacticals.general_elim when the eliminator has missing bindings *)
 
-let elim_res_pf_THEN_i kONT clenv tac gls =  
-  let clenv' = (clenv_unique_resolver true clenv gls) in
-  tclTHENLASTn (clenv_refine kONT clenv') (tac clenv') gls
-
 let rec build_args acc ce p_0 p_1 =
   match kind_of_term p_0, p_1 with 
     | (Prod (na,a,b), (a_0::bargs)) ->
diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli
index 45b9553265..7493e813c7 100644
--- a/tactics/wcclausenv.mli
+++ b/tactics/wcclausenv.mli
@@ -25,17 +25,6 @@ open Clenv
 val pf_get_new_id  : identifier      -> goal sigma -> identifier
 val pf_get_new_ids : identifier list -> goal sigma -> identifier list
 
-type arg_binder = 
-  | Dep of identifier 
-  | Nodep of int 
-  | Abs of int
-
-type arg_bindings = (arg_binder * constr) list
-
-type wc = named_context sigma
-
-val clenv_constrain_with_bindings : arg_bindings -> wc clausenv -> wc clausenv
-
 (*i**
 val add_prod_sign : 
   'a evar_map -> constr * types signature -> constr * types signature
@@ -44,7 +33,4 @@ val add_prods_sign :
   'a evar_map -> constr * types signature -> constr * types signature
 **i*)
 
-val elim_res_pf_THEN_i : 
-  (wc -> tactic) -> wc clausenv -> (wc clausenv -> tactic array) -> tactic
-
 val applyUsing : constr -> tactic
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 63b310bc34..c3be3d98ab 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -30,8 +30,18 @@ open Rawterm
 
 let guill s = "\""^s^"\""
 
+let nth i =
+  let many = match i mod 10 with 1 -> "st" | 2 -> "nd" | _ -> "th" in
+  int i ++ str many
+
+let pr_db ctx i =
+  try
+    match lookup_rel i ctx with
+        Name id, _, _ -> pr_id id
+      | Anonymous, _, _ -> str"<>"
+  with Not_found -> str"UNBOUND_REL_"++int i
+
 let explain_unbound_rel ctx n =
-  let ctx = make_all_name_different ctx in
   let pe = pr_ne_context_of (str "In environment") ctx in
   str"Unbound reference: " ++ pe ++
   str"The reference " ++ int n ++ str " is free"
@@ -41,7 +51,6 @@ let explain_unbound_var ctx v =
   str"No such section variable or assumption : " ++ var
 
 let explain_not_type ctx j =
-  let ctx = make_all_name_different ctx in
   let pe = pr_ne_context_of (str"In environment") ctx in
   let pc,pt = prjudge_env ctx j in
   pe ++ str "the term" ++ brk(1,1) ++ pc ++ spc () ++
@@ -49,7 +58,6 @@ let explain_not_type ctx j =
   str"which should be Set, Prop or Type."
 
 let explain_bad_assumption ctx j =
-  let ctx = make_all_name_different ctx in
   let pe = pr_ne_context_of (str"In environment") ctx in
   let pc,pt = prjudge_env ctx j in
   pe ++ str "cannot declare a variable or hypothesis over the term" ++
@@ -121,7 +129,6 @@ let explain_ill_formed_branch ctx c i actty expty =
   str "which should be" ++ brk(1,1) ++ pe
 
 let explain_generalization ctx (name,var) j =
-  let ctx = make_all_name_different ctx in
   let pe = pr_ne_context_of (str "In environment") ctx in
   let pv = prtype_env ctx var in
   let (pc,pt) = prjudge_env (push_rel_assum (name,var) ctx) j in
@@ -132,7 +139,6 @@ let explain_generalization ctx (name,var) j =
   spc () ++ str"which should be Set, Prop or Type."
 
 let explain_actual_type ctx j pt =
-  let ctx = make_all_name_different ctx in
   let pe = pr_ne_context_of (str "In environment") ctx in
   let (pc,pct) = prjudge_env ctx j in
   let pt = prterm_env ctx pt in
@@ -143,15 +149,13 @@ let explain_actual_type ctx j pt =
 
 let explain_cant_apply_bad_type ctx (n,exptyp,actualtyp) rator randl =
   let randl = Array.to_list randl in
-  let ctx = make_all_name_different ctx in
 (*  let pe = pr_ne_context_of (str"in environment") ctx in*)
   let pr,prt = prjudge_env ctx rator in
   let term_string1,term_string2 =
     if List.length randl > 1 then
-      let many = match n mod 10 with 1 -> "st" | 2 -> "nd" | _ -> "th" in
-      "terms", "The "^(string_of_int n)^many^" term"
+      str "terms", (str"The "++nth n++str" term")
     else
-      "term","This term" in
+      str "term", str "This term" in
   let appl = prlist_with_sep pr_fnl 
 	       (fun c ->
 		  let pc,pct = prjudge_env ctx c in
@@ -160,14 +164,13 @@ let explain_cant_apply_bad_type ctx (n,exptyp,actualtyp) rator randl =
   str"Illegal application (Type Error): " ++ (* pe ++ *) fnl () ++
   str"The term" ++ brk(1,1) ++ pr ++ spc () ++
   str"of type" ++ brk(1,1) ++ prt ++ spc ()  ++
-  str("cannot be applied to the "^term_string1) ++ fnl () ++ 
-  str" " ++ v 0 appl ++ fnl () ++ str (term_string2^" has type") ++
+  str"cannot be applied to the " ++ term_string1 ++ fnl () ++ 
+  str" " ++ v 0 appl ++ fnl () ++ term_string2 ++ str" has type" ++
   brk(1,1) ++ prterm_env ctx actualtyp ++ spc () ++
   str"which should be coercible to" ++ brk(1,1) ++ prterm_env ctx exptyp
 
 let explain_cant_apply_not_functional ctx rator randl =
   let randl = Array.to_list randl in
-  let ctx = make_all_name_different ctx in
 (*  let pe = pr_ne_context_of (str"in environment") ctx in*)
   let pr = prterm_env ctx rator.uj_val in
   let prt = prterm_env ctx rator.uj_type in
@@ -202,7 +205,12 @@ let explain_not_product ctx c =
 
 (* TODO: use the names *)
 (* (co)fixpoints *)
-let explain_ill_formed_rec_body ctx err names i vdefs =
+let explain_ill_formed_rec_body ctx err names i =
+  let prt_name i =
+    match names.(i) with
+        Name id -> str "Recursive definition of " ++ pr_id id
+      | Anonymous -> str"The " ++ nth i ++ str" definition" in
+
   let st = match err with
 
   (* Fixpoint guard errors *)
@@ -210,10 +218,33 @@ let explain_ill_formed_rec_body ctx err names i vdefs =
       str "Not enough abstractions in the definition"
   | RecursionNotOnInductiveType ->
       str "Recursive definition on a non inductive type"
-  | RecursionOnIllegalTerm ->
-      str "Recursive call applied to an illegal term"
-  | NotEnoughArgumentsForFixCall ->
-      str "Not enough arguments for the recursive call"
+  | RecursionOnIllegalTerm(j,arg,le,lt) ->
+      let called =
+        match names.(j) with
+            Name id -> pr_id id
+          | Anonymous -> str"the " ++ nth i ++ str" definition" in
+      let vars =
+        match (lt,le) with
+            ([],[]) -> mt()
+          | ([],[x]) ->
+              str "a subterm of " ++ pr_db ctx x
+          | ([],_) ->
+              str "a subterm of the following variables: " ++
+              prlist_with_sep pr_spc (pr_db ctx) le
+          | ([x],_) -> pr_db ctx x
+          | _ ->
+              str "one of the following variables: " ++
+              prlist_with_sep pr_spc (pr_db ctx) lt in
+      str "Recursive call to " ++ called ++ spc() ++
+      str "has principal argument equal to" ++ spc() ++
+      prterm_env ctx arg ++ fnl() ++ str "instead of " ++ vars
+
+  | NotEnoughArgumentsForFixCall j ->
+      let called =
+        match names.(j) with
+            Name id -> pr_id id
+          | Anonymous -> str"the " ++ nth i ++ str" definition" in
+     str "Recursive call to " ++ called ++ str " had not enough arguments"
 
   (* CoFixpoint guard errors *)
   (* TODO : récupérer le contexte des termes pour pouvoir les afficher *)
@@ -239,13 +270,9 @@ let explain_ill_formed_rec_body ctx err names i vdefs =
   | NotGuardedForm ->
       str "Definition not in guarded form"
   in
-  let pvd = prterm_env ctx vdefs.(i) in
-  let s = match names.(i) with Name id -> string_of_id id | Anonymous -> "_" in
-  st ++ fnl () ++ str"The " ++
-  (if Array.length vdefs = 1 then mt () else (int (i+1) ++ str "-th ")) ++
-  str"recursive definition" ++ spc () ++ str s ++
-  spc ()  ++ str":=" ++ spc ()  ++ pvd ++ spc () ++
-  str "is not well-formed"
+  prt_name i ++ str" is ill-formed." ++ fnl() ++
+  pr_ne_context_of (str "In environment") ctx ++
+  st
 
 let explain_ill_typed_rec_body ctx i names vdefj vargs =
   let pvd,pvdt = prjudge_env ctx (vdefj.(i)) in
@@ -341,8 +368,8 @@ let explain_type_error ctx = function
       explain_cant_apply_bad_type ctx t rator randl
   | CantApplyNonFunctional (rator, randl) ->
       explain_cant_apply_not_functional ctx rator randl
-  | IllFormedRecBody (i, lna, vdefj, vargs) ->
-      explain_ill_formed_rec_body ctx i lna vdefj vargs
+  | IllFormedRecBody (err, lna, i) ->
+      explain_ill_formed_rec_body ctx err lna i
   | IllTypedRecBody (i, lna, vdefj, vargs) -> 
      explain_ill_typed_rec_body ctx i lna vdefj vargs
   | WrongCaseInfo (ind,ci) ->