Petit nettoyage de Evarutil et Evarconv

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

6 files changed, 156 insertions, 209 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 08f46aef54..6280fc392b 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -156,7 +156,7 @@ let inh_conv_coerce_to loc env isevars cj t =
    each arg$_i$, if necessary *)
 
 let inh_apply_rel_list apploc env isevars argjl funj tycon =
-  let rec apply_rec n acc typ = function
+  let rec apply_rec env n acc typ = function
     | [] -> 
 	let resj =
       	  { uj_val = applist (j_val funj, List.rev acc);
@@ -170,7 +170,7 @@ let inh_apply_rel_list apploc env isevars argjl funj tycon =
 
     | hj::restjl ->
       	match kind_of_term (whd_betadeltaiota env !isevars typ) with
-          | IsProd (_,c1,c2) ->
+          | IsProd (na,c1,c2) ->
               let hj' =
 		(try 
 		   inh_conv_coerce_to_fail env isevars c1 hj 
@@ -181,10 +181,11 @@ let inh_apply_rel_list apploc env isevars argjl funj tycon =
 		     (j_nf_ise env !isevars funj)
 		     (jl_nf_ise env !isevars argjl))
 	      in
-	      apply_rec (n+1) ((j_val hj')::acc) (subst1 hj'.uj_val c2) restjl
+	      apply_rec (push_rel_assum (na,c1) env)
+		(n+1) ((j_val hj')::acc) (subst1 hj'.uj_val c2) restjl
           | _ ->
               error_cant_apply_not_functional_loc apploc env
 	      	(j_nf_ise env !isevars funj) (jl_nf_ise env !isevars argjl)
   in 
-  apply_rec 1 [] funj.uj_type argjl
+  apply_rec env 1 [] funj.uj_type argjl
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 15151ca9ba..fd52e0fa0f 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -13,37 +13,6 @@ open Classops
 open Recordops 
 open Evarutil
 
-(* Pb: Mach cannot type evar in the general case (all Const must be applied
- * to Vars). But evars may be applied to Rels or other terms! This is the
- * difference between type_of_const and type_of_const2.
- *)
-
-(* This code (i.e. try_solve_pb, solve_pb, etc.) takes a unification
- * problem, and tries to solve it. If it solves it, then it removes
- * all the conversion problems, and re-runs conversion on each one, in
- * the hopes that the new solution will aid in solving them.
- *
- * The kinds of problems it knows how to solve are those in which
- * the usable arguments of an existential var are all themselves
- * universal variables.
- * The solution to this problem is to do renaming for the Var's,
- * to make them match up with the Var's which are found in the
- * hyps of the existential, to do a "pop" for each Rel which is
- * not an argument of the existential, and a subst1 for each which
- * is, again, with the corresponding variable. This is done by
- * Tradevar.evar_define
- *
- * Thus, we take the arguments of the existential which we are about
- * to assign, and zip them with the identifiers in the hypotheses.
- * Then, we process all the Var's in the arguments, and sort the
- * Rel's into ascending order.  Then, we just march up, doing
- * subst1's and pop's.
- *
- * NOTE: We can do this more efficiently for the relative arguments,
- * by building a long substituend by hand, but this is a pain in the
- * ass.
- *)
-
 let evar_apprec env isevars stack c =
   let rec aux s =
     let (t,stack as s') = Reduction.apprec env !isevars s in
@@ -53,56 +22,31 @@ let evar_apprec env isevars stack c =
       | _ -> (t, list_of_stack stack)
   in aux (c, append_stack (Array.of_list stack) empty_stack)
 
-
-let conversion_problems = ref ([] : (conv_pb * constr * constr) list)
-
-let reset_problems () = conversion_problems := []
-
-let add_conv_pb pb = (conversion_problems := pb::!conversion_problems)
-
-let get_changed_pb lev =
-  let (pbs,pbs1) = 
-    List.fold_left
-      (fun (pbs,pbs1) pb ->
-    	 if status_changed lev pb then 
-	   (pb::pbs,pbs1)
-         else 
-	   (pbs,pb::pbs1))
-      ([],[])
-      !conversion_problems 
-  in
-  conversion_problems := pbs1;
-  pbs
-
 (* Precondition: one of the terms of the pb is an uninstanciated evar,
  * possibly applied to arguments. *)
 
-let rec solve_pb env isevars pb =
-  match solve_simple_eqn (evar_conv_x env isevars CONV) isevars pb with
-    | Some lsp ->
-	let pbs = get_changed_pb lsp in
-	List.for_all
- 	  (fun (pbty,t1,t2) -> evar_conv_x env isevars pbty t1 t2)
- 	  pbs
-    | None -> (add_conv_pb pb; true)
-
-and evar_conv_x env isevars pbty term1 term2 =
+let rec evar_conv_x env isevars pbty term1 term2 =
   let term1 = whd_ise1 !isevars term1 in
   let term2 = whd_ise1 !isevars term2 in
-  if eq_constr term1 term2 then 
+(*
+ if eq_constr term1 term2 then 
     true
   else if (not(has_undefined_isevars isevars term1)) &
     not(has_undefined_isevars isevars term2) 
   then 
     is_fconv pbty env !isevars term1 term2
-  else if ise_undefined isevars term1 or ise_undefined isevars term2
-  then 
-    solve_pb env isevars (pbty,term1,term2)
+  else
+*)
+  (is_fconv pbty env !isevars term1 term2) or
+  if ise_undefined isevars term1 then
+    solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term1,term2)
+  else if ise_undefined isevars term2 then
+    solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term2,term1)
   else 
     let (t1,l1) = evar_apprec env isevars [] term1 in
     let (t2,l2) = evar_apprec env isevars [] term2 in
-    if (head_is_embedded_exist isevars t1 & not(is_eliminator t2))
-      or (head_is_embedded_exist isevars t2 & not(is_eliminator t1))
+    if (head_is_embedded_evar isevars t1 & not(is_eliminator t2))
+      or (head_is_embedded_evar isevars t2 & not(is_eliminator t1))
     then 
       (add_conv_pb (pbty,applist(t1,l1),applist(t2,l2)); true)
     else 
@@ -111,15 +55,17 @@ and evar_conv_x env isevars pbty term1 term2 =
 and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
   (* Evar must be undefined since we have whd_ised *)
   match (kind_of_term term1, kind_of_term term2) with
-    | IsEvar (sp1,al1), IsEvar (sp2,al2) ->
+    | IsEvar (sp1,al1 as ev1), IsEvar (sp2,al2 as ev2) ->
 	let f1 () =
 	  if List.length l1 > List.length l2 then 
             let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
-            solve_pb env isevars(pbty,applist(term1,deb1),term2)
+            solve_simple_eqn evar_conv_x env isevars 
+	      (pbty,ev2,applist(term1,deb1))
             & list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2
 	  else
 	    let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
-	    solve_pb env isevars(pbty,term1,applist(term2,deb2))
+	    solve_simple_eqn evar_conv_x env isevars
+	      (pbty,ev1,applist(term2,deb2))
             & list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2
 	and f2 () =
           (sp1 = sp2)
@@ -128,11 +74,12 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	in 
 	ise_try isevars [f1; f2]
 
-    | IsEvar (sp1,al1), IsConst cst2 ->
+    | IsEvar ev1, IsConst cst2 ->
 	let f1 () =
 	  (List.length l1 <= List.length l2) &
 	  let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
-	  solve_pb env isevars(pbty,term1,applist(term2,deb2))
+	  solve_simple_eqn evar_conv_x env isevars
+	    (pbty,ev1,applist(term2,deb2))
           & list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2
 	and f4 () =
 	  match constant_opt_value env cst2 with
@@ -143,11 +90,12 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	in 
 	ise_try isevars [f1; f4]
 
-    | IsConst cst1, IsEvar (sp2,al2) ->
+    | IsConst cst1, IsEvar ev2 ->
 	let f1 () =
        	  (List.length l2 <= List.length l1) &
        	  let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
-	  solve_pb env isevars(pbty,applist(term1,deb1),term2)
+	  solve_simple_eqn evar_conv_x env isevars
+	    (pbty,ev2,applist(term1,deb1))
           & list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2
 	and f4 () =
 	  match constant_opt_value env cst1 with
@@ -182,16 +130,18 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	in 
 	ise_try isevars [f2; f3; f4]
 
-    | IsEvar (_,_), _ ->
+    | IsEvar ev1, _ ->
        	(List.length l1 <= List.length l2) &
        	let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
-	solve_pb env isevars(pbty,term1,applist(term2,deb2))
+	solve_simple_eqn evar_conv_x env isevars
+	  (pbty,ev1,applist(term2,deb2))
         & list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2
 
-    | _, IsEvar (_,_) ->
+    | _, IsEvar ev2 ->
        	(List.length l2 <= List.length l1) &
        	let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
-	solve_pb env isevars(pbty,applist(term1,deb1),term2)
+	solve_simple_eqn evar_conv_x env isevars
+	  (pbty,ev2,applist(term1,deb1))
         & list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2
 
     | IsConst cst1, _ ->
@@ -342,14 +292,6 @@ and check_conv_record (t1,l1) (t2,l2) =
   with _ -> 
     raise Not_found
 
-let the_conv_x env isevars t1 t2 =
-  is_conv env !isevars t1 t2 or evar_conv_x env isevars CONV t1 t2
-
-(* Si conv_x_leq repond true, pourquoi diable est-ce qu'on repasse une couche
- * avec evar_conv_x! Si quelqu'un comprend pourquoi, qu'il remplace ce
- * commentaire. Sinon, il va y avoir un bon coup de balai. B.B.
- *)
-let the_conv_x_leq env isevars t1 t2 =
-  is_conv_leq env !isevars t1 t2
-  or evar_conv_x env isevars CONV_LEQ t1 t2     
+let the_conv_x     env isevars t1 t2 = evar_conv_x env isevars CONV     t1 t2
+let the_conv_x_leq env isevars t1 t2 = evar_conv_x env isevars CONV_LEQ t1 t2
  
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 6672a3d4b0..7d53d31118 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -9,20 +9,12 @@ open Reduction
 open Evarutil
 (*i*)
 
-val reset_problems : unit -> unit
-
 val the_conv_x : env -> 'a evar_defs -> constr -> constr -> bool
 
 val the_conv_x_leq : env -> 'a evar_defs -> constr -> constr -> bool
 
 (*i For debugging *)
-val solve_pb : 
-  env -> 'a evar_defs -> conv_pb * constr * constr -> bool
-
-val evar_conv_x : 
-  env -> 'a evar_defs ->
-    conv_pb -> constr -> constr -> bool
-
+val evar_conv_x : env -> 'a evar_defs -> conv_pb -> constr -> constr -> bool
 val evar_eqappr_x : 
   env -> 'a evar_defs ->
     conv_pb -> constr * constr list -> constr * constr list -> bool
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 8cab61c947..ce08a0f390 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -125,6 +125,7 @@ let do_restrict_hyps sigma c =
  * operations on the evar constraints *
  *------------------------------------*)
 
+type evar_constraint = conv_pb * constr * constr
 type 'a evar_defs = 'a Evd.evar_map ref
 
 (* ise_try [f1;...;fn] tries fi() for i=1..n, restoring the evar constraints
@@ -169,10 +170,6 @@ let restrict_hyps isevars c =
   end else 
     c
 
-let has_ise sigma t = 
-  try let _ = whd_ise sigma t in false
-  with Uninstantiated_evar _ -> true
-
 (* We try to instanciate the evar assuming the body won't depend
  * on arguments that are not Rels or Vars, or appearing several times.
  *)
@@ -247,8 +244,7 @@ let keep_rels_and_vars c = match kind_of_term c with
   | IsVar _ | IsRel _ -> c
   | _ -> mkImplicit   (* Mettre mkMeta ?? *)
 
-let evar_define isevars lhs rhs =
-  let (ev,argsv) = destEvar lhs in
+let evar_define isevars (ev,argsv) rhs =
   if occur_evar ev rhs then error_occur_check CCI empty_env ev rhs;
   let args = List.map keep_rels_and_vars (Array.to_list argsv) in 
   let evd = ise_map isevars ev in
@@ -258,23 +254,108 @@ let evar_define isevars lhs rhs =
   ise_define isevars ev body;
   [ev]
 
+(*-------------------*)
+(* Auxiliary functions for the conversion algorithms modulo evars
+ *)
+
+let has_undefined_isevars isevars t = 
+  try let _ = whd_ise !isevars t in false
+  with Uninstantiated_evar _ -> true
+
+let head_is_evar isevars = 
+  let rec hrec k = match kind_of_term k with
+    | IsEvar (n,_)   -> not (Evd.is_defined !isevars n)
+    | IsApp (f,_) -> hrec f
+    | IsCast (c,_) -> hrec c
+    | _ -> false
+  in 
+  hrec 
+
+let rec is_eliminator c = match kind_of_term c with
+  | IsApp _    -> true
+  | IsMutCase _ -> true
+  | IsCast (c,_) -> is_eliminator c
+  | _ -> false
+
+let head_is_embedded_evar isevars c =
+  (head_is_evar isevars c) & (is_eliminator c)
+
+let head_evar = 
+  let rec hrec c = match kind_of_term c with
+    | IsEvar (ev,_)       -> ev
+    | IsMutCase (_,_,c,_) -> hrec c
+    | IsApp (c,_)        -> hrec c
+    | IsCast (c,_)        -> hrec c
+    | _                   -> failwith "headconstant"
+  in 
+  hrec 
 
+(* This code (i.e. solve_pb, etc.) takes a unification
+ * problem, and tries to solve it. If it solves it, then it removes
+ * all the conversion problems, and re-runs conversion on each one, in
+ * the hopes that the new solution will aid in solving them.
+ *
+ * The kinds of problems it knows how to solve are those in which
+ * the usable arguments of an existential var are all themselves
+ * universal variables.
+ * The solution to this problem is to do renaming for the Var's,
+ * to make them match up with the Var's which are found in the
+ * hyps of the existential, to do a "pop" for each Rel which is
+ * not an argument of the existential, and a subst1 for each which
+ * is, again, with the corresponding variable. This is done by
+ * Tradevar.evar_define
+ *
+ * Thus, we take the arguments of the existential which we are about
+ * to assign, and zip them with the identifiers in the hypotheses.
+ * Then, we process all the Var's in the arguments, and sort the
+ * Rel's into ascending order.  Then, we just march up, doing
+ * subst1's and pop's.
+ *
+ * NOTE: We can do this more efficiently for the relative arguments,
+ * by building a long substituend by hand, but this is a pain in the
+ * ass.
+ *)
+
+let conversion_problems = ref ([] : evar_constraint list)
+
+let reset_problems () = conversion_problems := []
+
+let add_conv_pb pb = (conversion_problems := pb::!conversion_problems)
+
+let status_changed lev (pbty,t1,t2) =
+  try 
+    List.mem (head_evar t1) lev or List.mem (head_evar t2) lev
+  with Failure _ ->
+    try List.mem (head_evar t2) lev with Failure _ -> false
+
+let get_changed_pb lev =
+  let (pbs,pbs1) = 
+    List.fold_left
+      (fun (pbs,pbs1) pb ->
+    	 if status_changed lev pb then 
+	   (pb::pbs,pbs1)
+         else 
+	   (pbs,pb::pbs1))
+      ([],[])
+      !conversion_problems 
+  in
+  conversion_problems := pbs1;
+  pbs
 
 (* Solve pbs (?i x1..xn) = (?i y1..yn) which arises often in fixpoint
  * definitions. We try to unify the xi with the yi pairwise. The pairs
  * that don't unify are discarded (i.e. ?i is redefined so that it does not
  * depend on these args). *)
 
-let solve_refl conv_algo isevars c1 c2 =
-  let (ev,argsv1) = destEvar c1
-  and (_,argsv2) = destEvar c2 in
+let solve_refl conv_algo env isevars ev argsv1 argsv2 =
+  if argsv1 = argsv2 then [] else
   let evd = Evd.map !isevars ev in
   let env = evd.evar_env in
   let hyps = named_context env in
   let (_,rsign) = 
     array_fold_left2
       (fun (sgn,rsgn) a1 a2 ->
-	 if conv_algo a1 a2 then 
+	 if conv_algo env isevars CONV a1 a2 then 
 	   (List.tl sgn, add_named_decl (List.hd sgn) rsgn)
 	 else 
 	   (List.tl  sgn, rsgn))
@@ -288,87 +369,32 @@ let solve_refl conv_algo isevars c1 c2 =
 	       evar_body = Evar_empty; evar_info = None } in
   isevars :=
     Evd.define (Evd.add !isevars newev info) ev (mkEvar (newev,nargs));
-  Some [ev]
+  [ev]
 
 
 (* Tries to solve problem t1 = t2.
- * Precondition: one of t1,t2 is an uninstanciated evar, possibly
- * applied to arguments.
+ * Precondition: t1 is an uninstanciated evar
  * Returns an optional list of evars that were instantiated, or None
  * if the problem couldn't be solved. *)
 
 (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *)
-let rec solve_simple_eqn conv_algo isevars ((pbty,t1,t2) as pb) =
-  let t1 = nf_ise1 !isevars t1 in
+let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) =
   let t2 = nf_ise1 !isevars t2 in
-  if eq_constr t1 t2 then 
-    Some []
-  else 
-    match (ise_undefined isevars t1, ise_undefined isevars t2) with
-      | (true,true) ->
-	  if num_of_evar t1 = num_of_evar t2 then 
-	    solve_refl conv_algo isevars t1 t2
-	  else if Array.length(snd (destEvar t1)) < 
-	          Array.length(snd (destEvar t2)) then 
-	    Some (evar_define isevars t2 t1)
-	  else 
-	    Some (evar_define isevars t1 t2)
-      | (true,false) -> Some (evar_define isevars t1 t2)
-      | (false,true) -> Some (evar_define isevars t2 t1)
-      | _ -> None
-
-(*-------------------*)
-(* Now several auxiliary functions for the conversion algorithms modulo
- * evars. used in trad and progmach
- *)
-
-
-let has_undefined_isevars isevars c =
-  let rec hasrec k = match splay_constr k with
-    | OpEvar ev, cl when ise_in_dom isevars ev ->
-	if ise_defined isevars k then 
-	  hasrec (existential_value !isevars (ev,cl))
+  let lsp = match kind_of_term t2 with
+    | IsEvar (n2,args2 as ev2) when not (Evd.is_defined !isevars n2) ->
+	if n1 = n2 then
+	  solve_refl conv_algo env isevars n1 args1 args2
 	else
-	  failwith "caught"
-    | _, cl -> Array.iter hasrec cl
-  in 
-  (try (hasrec c ; false) with Failure "caught" -> true)
-
-let head_is_exist isevars = 
-  let rec hrec k = match kind_of_term k with
-    | IsEvar _     -> ise_undefined isevars k
-    | IsApp (f,_) -> hrec f
-    | IsCast (c,_) -> hrec c
-    | _ -> false
-  in 
-  hrec 
-
-let rec is_eliminator c = match kind_of_term c with
-  | IsApp _    -> true
-  | IsMutCase _ -> true
-  | IsCast (c,_) -> is_eliminator c
-  | _ -> false
-
-let head_is_embedded_exist isevars c =
-  (head_is_exist isevars c) & (is_eliminator c)
-
-let head_evar = 
-  let rec hrec c = match kind_of_term c with
-    | IsEvar (ev,_)       -> ev
-    | IsMutCase (_,_,c,_) -> hrec c
-    | IsApp (c,_)        -> hrec c
-    | IsCast (c,_)        -> hrec c
-    | _                   -> failwith "headconstant"
-  in 
-  hrec 
-    
-let status_changed lev (pbty,t1,t2) =
-  try 
-    List.mem (head_evar t1) lev or List.mem (head_evar t2) lev
-  with Failure _ ->
-    try List.mem (head_evar t2) lev with Failure _ -> false
+	  if Array.length args1 < Array.length args2 then 
+	    evar_define isevars ev2 (mkEvar ev1)
+	  else 
+	    evar_define isevars ev1 t2
+    | _ ->
+	evar_define isevars ev1 t2 in
+  let pbs = get_changed_pb lsp in
+  List.for_all (fun (pbty,t1,t2) -> conv_algo env isevars pbty t1 t2) pbs
 
-(* Operations on value/type constraints used in trad and progmach *)
+(* Operations on value/type constraints *)
 
 type type_constraint = constr option
 type val_constraint = constr option
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index dbebeac984..069a0f1766 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -10,39 +10,26 @@ open Environ
 open Reduction
 (*i*)
 
-(* This modules provides useful functions for unification algorithms.
- * Used in Trad and Progmach.
- * This interface will have to be improved. *)
-
-val filter_unique : 'a list -> 'a list
-val distinct_id_list : identifier list -> identifier list
+(*s This modules provides useful functions for unification modulo evars *)
 
 val dummy_sort : constr
-val do_restrict_hyps : 'a evar_map -> constr -> 'a evar_map * constr
-val has_ise : 'a evar_map -> constr -> bool
-
+type evar_constraint = conv_pb * constr * constr
 type 'a evar_defs = 'a evar_map ref
 
-val ise_try : 'a evar_defs -> (unit -> bool) list -> bool
+val reset_problems : unit -> unit
+val add_conv_pb : evar_constraint -> unit
 
+val ise_try : 'a evar_defs -> (unit -> bool) list -> bool
 val ise_undefined : 'a evar_defs -> constr -> bool
-val ise_defined : 'a evar_defs -> constr -> bool
+val has_undefined_isevars : 'a evar_defs -> constr -> bool
 
-val real_clean :
-  'a evar_defs -> int -> (identifier * constr) list -> constr -> constr
-val new_isevar :
-  'a evar_defs -> env -> constr -> path_kind -> constr
-val evar_define : 'a evar_defs -> constr -> constr -> int list
-val solve_simple_eqn : (constr -> constr -> bool) -> 'a evar_defs ->
-  (conv_pb * constr * constr) -> int list option
+val new_isevar : 'a evar_defs -> env -> constr -> path_kind -> constr
 
-val has_undefined_isevars : 'a evar_defs -> constr -> bool
-val head_is_exist : 'a evar_defs -> constr -> bool
 val is_eliminator : constr -> bool
-val head_is_embedded_exist : 'a evar_defs -> constr -> bool
-val head_evar : constr -> int
-val status_changed : int list -> conv_pb * constr * constr -> bool
-
+val head_is_embedded_evar : 'a evar_defs -> constr -> bool
+val solve_simple_eqn :
+  (env -> 'a evar_defs -> conv_pb -> constr -> constr -> bool)
+  -> env -> 'a evar_defs -> conv_pb * existential * constr -> bool
 
 (* Value/Type constraints *)
 
@@ -51,7 +38,6 @@ type val_constraint = constr option
 
 val empty_tycon : type_constraint
 val mk_tycon : constr -> type_constraint
-
 val empty_valcon : val_constraint
 val mk_valcon : constr -> val_constraint
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 2ae6d435aa..67e793c54f 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -315,7 +315,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 		let pred = 
 		  Cases.pred_case_ml_onebranch env !isevars isrec indt
 		    (i,fj.uj_val,efjt) in
-		if has_ise !isevars pred then findtype (i+1)
+		if has_undefined_isevars isevars pred then findtype (i+1)
 		else 
 		  let pty = Retyping.get_type_of env !isevars pred in
 		  { uj_val = pred;