Poursuite intégration du Cases

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

7 files changed, 163 insertions, 115 deletions

diff --git a/.depend b/.depend
index 00ac16a451..17b668afe4 100644
--- a/.depend
+++ b/.depend
@@ -70,6 +70,10 @@ parsing/printer.cmi: parsing/coqast.cmi kernel/names.cmi lib/pp.cmi \
     pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi 
 parsing/termast.cmi: parsing/coqast.cmi kernel/names.cmi \
     pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi 
+pretyping/cases.debug.cmi: kernel/environ.cmi pretyping/evarutil.cmi \
+    kernel/evd.cmi kernel/generic.cmi kernel/names.cmi lib/pp.cmi \
+    pretyping/rawterm.cmi pretyping/retyping.cmi kernel/sign.cmi \
+    kernel/term.cmi kernel/type_errors.cmi 
 pretyping/cases.cmi: kernel/environ.cmi pretyping/evarutil.cmi kernel/evd.cmi \
     kernel/names.cmi pretyping/rawterm.cmi kernel/term.cmi 
 pretyping/classops.cmi: library/declare.cmi kernel/environ.cmi kernel/evd.cmi \
@@ -821,8 +825,6 @@ tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo
 tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx 
 tools/coqdep_lexer.cmo: config/coq_config.cmi 
 tools/coqdep_lexer.cmx: config/coq_config.cmx 
-tools/gallina.cmo: tools/gallina_lexer.cmo 
-tools/gallina.cmx: tools/gallina_lexer.cmx 
 toplevel/class.cmo: pretyping/classops.cmi kernel/constant.cmi \
     library/declare.cmi kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
     library/global.cmi kernel/inductive.cmi kernel/instantiate.cmi \
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 5ac91dc00d..eaa87b5be2 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -55,6 +55,20 @@ let change_hyps f env =
   let (ENVIRON(g,r)) = env.env_context in
   { env with env_context = ENVIRON (f g, r) }
 
+(* == functions to deal with names in contexts (previously in cases.ml) == *)
+
+(* If cur=(Rel j) then 
+ * if env = ENVIRON(sign,[na_h:Th]...[na_j:Tj]...[na_1:T1])
+ * then it yields ENVIRON(sign,[na_h:Th]...[Name id:Tj]...[na_1:T1])
+ *)
+let change_name_rel env j id =
+  let ENVIRON(sign,db) = context env in
+  (match list_chop (j-1) db with
+       db1,((_,ty)::db2) ->
+	 {env with env_context = ENVIRON(sign,db1@(Name id,ty)::db2)}
+     | _ -> assert false)
+(****)
+
 let push_rel idrel env =
   { env with env_context = add_rel idrel env.env_context }
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index cfcdf2d36c..ffb5861e1b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -27,6 +27,7 @@ val var_context : env -> var_context
 val push_var : identifier * typed_type -> env -> env
 val change_hyps : 
   (typed_type signature -> typed_type signature) -> env -> env
+val change_name_rel : env -> int -> identifier -> env
 
 val push_rel : name * typed_type -> env -> env
 
diff --git a/parsing/termast.ml b/parsing/termast.ml
index cfe85f7fda..1e6ff11fc8 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -20,14 +20,11 @@ open Rawterm
 (**********************************************************************)
 (* conversion of references                                           *)
 
-let ids_of_ctxt cl =
+let ids_of_var cl =
   List.map
     (function 
-       | VAR id -> id
-       | Rel n ->
-	   warning "ids_of_ctxt: rel";
-	   id_of_string ("REL "^(string_of_int n))
-       | _-> anomaly "ids_of_ctxt")
+       | RRef (_,RVar id) -> id
+       | _-> anomaly "ids_of_var")
     (Array.to_list cl)
 
 let ast_of_ident id = nvar (string_of_id id)
@@ -94,18 +91,6 @@ let rec ast_of_pattern = function   (* loc is thrown away for printing *)
 
 type used_idents = identifier list
 
-(*
-  let concrete_name (lo,l as ll) n c =
-    if n = Anonymous then
-      if dependent (Rel 1) c then anomaly "Anonymous should be non dependent"
-      else (None,ll)
-    else
-      let l' = match lo with None -> l | Some l0 -> l0@l in
-      let fresh_id = next_name_away n l' in
-      let idopt = if dependent (Rel 1) c then (Some fresh_id) else None in
-      (idopt, (lo,fresh_id::l))
-*)
-
 let occur_id env id0 c =
   let rec occur n = function
     | VAR id             -> id=id0
@@ -137,11 +122,11 @@ let next_name_not_occuring name l env t =
     | Name id   -> next id
     | Anonymous -> id_of_string "_"
 
+(* Remark: Anonymous var may be dependent in Evar's contexts *)
 let concrete_name l env n c =
-  if n = Anonymous then begin
-    if dependent (Rel 1) c then anomaly "Anonymous should be non dependent";
+  if n = Anonymous & not (dependent (Rel 1) c) then
     (None,l)
-  end else
+  else
     let fresh_id = next_name_not_occuring n l env c in
     let idopt = if dependent (Rel 1) c then (Some fresh_id) else None in
     (idopt, fresh_id::l)
@@ -712,8 +697,9 @@ let rec detype avoid env t =
 	 in RRef (dummy_loc, RVar (id_of_string s)))
     | IsMeta n -> RRef (dummy_loc,RMeta n)
     | IsVar id -> RRef (dummy_loc,RVar id)
-    | IsXtra s -> anomaly "bdize: Xtra should no longer occur in constr"
-	(*       ope("XTRA",((str s):: pl@(List.map detype cl)))*)
+    | IsXtra s -> warning "bdize: Xtra should no longer occur in constr";
+	RRef(dummy_loc,RVar (id_of_string ("XTRA"^s)))
+        (* ope("XTRA",((str s):: pl@(List.map detype cl)))*) 
     | IsSort (Prop c) -> RSort (dummy_loc,RProp c)
     | IsSort (Type _) -> RSort (dummy_loc,RType)
     | IsCast (c1,c2) ->
@@ -722,14 +708,18 @@ let rec detype avoid env t =
     | IsLambda (na,ty,c) -> detype_binder BLambda avoid env na ty c
     | IsAppL (f,args) ->
 	RApp (dummy_loc,detype avoid env f,List.map (detype avoid env) args)
-    | IsConst (sp,cl) -> RRef (dummy_loc,RConst (sp,ids_of_ctxt cl))
-    | IsEvar (ev,cl) -> RRef (dummy_loc,REVar (ev,ids_of_ctxt cl))
+    | IsConst (sp,cl) ->
+	RRef(dummy_loc,RConst(sp,ids_of_var (Array.map (detype avoid env) cl)))
+    | IsEvar (ev,cl) ->
+	RRef(dummy_loc,REVar(ev,ids_of_var (Array.map (detype avoid env) cl)))
     | IsAbst (sp,cl) -> 
 	anomaly "bdize: Abst should no longer occur in constr"
     | IsMutInd (sp,tyi,cl) ->
-	RRef (dummy_loc,RInd ((sp,tyi),ids_of_ctxt cl))
-    | IsMutConstruct (sp,tyi,n,cl) -> 
-	RRef (dummy_loc,RConstruct (((sp,tyi),n),ids_of_ctxt cl))
+	let ids = ids_of_var (Array.map (detype avoid env) cl) in
+	RRef (dummy_loc,RInd ((sp,tyi),ids))
+    | IsMutConstruct (sp,tyi,n,cl) ->
+	let ids = ids_of_var (Array.map (detype avoid env) cl) in
+	RRef (dummy_loc,RConstruct (((sp,tyi),n),ids))
     | IsMutCase (annot,p,c,bl) ->
 	let synth_type = synthetize_type () in
 	let tomatch = detype avoid env c in
diff --git a/parsing/termast.mli b/parsing/termast.mli
index 220662ab34..d0c0d237af 100644
--- a/parsing/termast.mli
+++ b/parsing/termast.mli
@@ -21,7 +21,3 @@ val bdize_no_casts : bool -> unit assumptions -> constr -> Coqast.t
 val lookup_name_as_renamed :
   unit assumptions -> constr -> identifier -> int option
 val lookup_index_as_renamed : constr -> int -> int option
-
-(*i This is temporary *)
-val ids_of_ctxt : constr array -> identifier list
-(*i*)
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 0e0ae0ea62..30c88a227f 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -24,14 +24,6 @@ exception CasesError of env * type_error
 let starts_with_underscore id = 
  let s=string_of_id id in (String.get s 0)='_'
 
-
-let makelist n elem =
- let rec makerec n  =
-   if n=0 then []
-    else elem::(makerec (n-1)) 
- in makerec n 
-
- 
 let rec map_append_vect f v = 
   let length = Array.length v in 
   let rec map_rec i =
@@ -130,7 +122,7 @@ let check_pat_arity env = function
 (* Usage of this function should be avoided, because it requires that the
  * params are infered.
  *)
-let rec constr_of_pat = function
+let rec constr_of_pat isevars env = function
     PatVar (_,Name id) -> VAR id
   | PatVar (_,Anonymous) -> VAR (id_of_string "_")
   (* invalid_arg "constr_of_pat"*)
@@ -139,7 +131,12 @@ let rec constr_of_pat = function
       let mispec = Global.lookup_mind_specif ity in 
       let nparams = mis_nparams mispec in
       let c = mutconstruct_of_constructor c in
-      applist(c, makelist nparams mkExistential @ List.map constr_of_pat args)
+      let exl =
+	list_tabulate
+	  (fun _ ->
+	     fst (new_isevar isevars env (mkCast dummy_sort dummy_sort) CCI))
+	  nparams in
+      applist(c, exl @ List.map (constr_of_pat isevars env) args)
 
 
 
@@ -492,27 +489,6 @@ let check_patt_are_correct ity mat = List.iter (check_pattern ity) mat
   lifted when pushing inthe context. *)
 
 
-(* == functions to deal with names in contexts == *)
-
-(* If cur=(Rel j) then 
- * if env = ENVIRON(sign,[na_h:Th]...[na_j:Tj]...[na_1:T1])
- * then it yields ENVIRON(sign,[na_h:Th]...[Name id:Tj]...[na_1:T1])
- *)
-let change_name_rel env current id =
-  warning "change_name_rel not implemented"; env
-(*
- match current with 
-  (Rel j) -> 
-    if starts_with_underscore id 
-    then env 
-    else let ENVIRON(sign,db) = env in
-     ( match list_chop (j-1) db with
-	   db1,((_,ty)::db2) -> (ENVIRON(sign,db1@(Name id,ty)::db2))
-	 | _ -> assert false)
- |  _  -> env
-*)
- 
-
 (* == Function dealing with constraints in compilation of dep case == *)
 
 let xtra_tm = DOP0(XTRA("TMPATT"))
@@ -651,8 +627,15 @@ let get_names_for_constructor_arg cstr_sp mat =
   List.fold_left egalize_names anonymous_list mat
 *)
 
+let mychange_name_rel env current id =
+  match current with 
+      (Rel j) -> 
+	if starts_with_underscore id 
+	then env 
+	else change_name_rel env j id
+    |  _  -> env
 
-let submat depcase sigma env i ind_data params current mat =
+let submat depcase isevars env i ind_data params current mat =
 (* Futur...
   let concl_realargs = realargs_of_constructor_concl ind_data i in
   let constraints = matching concl_realargs ind_data.realargs in
@@ -671,7 +654,7 @@ let submat depcase sigma env i ind_data params current mat =
 	      List.map (fun id -> VAR id) new_ids
 	  | Some patts ->
 	      patts,
-              List.map constr_of_pat patts in
+              List.map (constr_of_pat isevars env) patts in
       let value =
 	if (is_predicate ind_data) or depcase
 	then applist (ci, params@largs)
@@ -685,7 +668,7 @@ let submat depcase sigma env i ind_data params current mat =
       | PatVar (_,name) ->
 	  let envopt = match name with
 	    | Anonymous -> None
-	    | Name id -> Some (change_name_rel env current id) in
+	    | Name id -> Some (mychange_name_rel env current id) in
 	  (envopt, [build_new_row None name])
       | PatCstr(_,c,largs,alias) when mutconstruct_of_constructor c = ci ->
 	(* Avant: il y aurait eu un problème si un des largs contenait
@@ -699,7 +682,7 @@ let submat depcase sigma env i ind_data params current mat =
 	   fait par "build_new_row" *)
 	  let envopt = match alias with
 	    | Anonymous -> None
-	    | Name id -> Some (change_name_rel env current id) in
+	    | Name id -> Some (mychange_name_rel env current id) in
 	    (envopt,[build_new_row (Some largs) alias])
       | PatCstr _ -> (None,[]) in
 
@@ -899,7 +882,7 @@ let rename_cur_ctxt env cur gd =
     let current = row_current r in
     match current with
       PatVar (_,Name id) when not (starts_with_underscore id) ->
- 	change_name_rel env cur id
+ 	mychange_name_rel env cur id
     | _ -> env
 
 
@@ -1114,32 +1097,56 @@ let rec to_lambda_pred isevars ind_data n env prod =
 (* =================================== *)
 (*   Principal functions               *)
 (* =================================== *)
+let type_one_branch dep env sigma ind_data p im =
+  let i = im + 1 in
+  let {mind=ity;params=params;nparams=nparams} = ind_data in
+  let ct =
+    type_of_constructor env sigma (ith_constructor_of_inductive ity i) in
+  let rec typrec n c =
+    match whd_betadeltaiota env sigma c with 
+      | DOP2(Prod,a1,DLAM(x,a2)) -> DOP2(Prod,a1,DLAM(x,typrec (n+1) a2))
+      | x -> let lAV = destAppL(ensure_appl x) in
+             let (_,vargs) = array_chop (nparams+1) lAV in
+	     let c1 = appvect (lift n p,vargs) in
+	     if dep then 
+	       let co = ith_constructor i ind_data in
+	       applist
+		 (c1,[applist(co,((List.map (lift n) params)@(rel_list 0 n)))])
+	     else c1
+  in 
+  typrec 0 (hnf_prod_applist env sigma "type_case" ct params)
 
-let my_norec_branch_scheme env sigma i mind = 
-  let typc = type_inst_construct env sigma i mind in
-  let rec crec typc =
-    match whd_betadeltaiota env sigma typc with 
-      DOP2(Prod,c,DLAM(name,t)) -> DOP2(Prod,c,DLAM(name,crec t))
-    | (DOPN(AppL,v))  ->  appvect (mkExistential, array_tl v)
-    | _ -> mkExistential
-  in crec typc
+let find_type_case_branches sigma env dep ind_data p =
+  let {nconstr=nconstr;mind=ity;params=params} = ind_data in
+  Array.init nconstr (type_one_branch dep env sigma ind_data p)
 
+(*
+let my_norec_branch_scheme env sigma i ind_data =
+  let typc = type_inst_construct env sigma i (mutind_to_ind mind) in
+  let rec typrec n typc =
+    match whd_betadeltaiota env sigma typc with
+      DOP2(Prod,c,DLAM(name,t)) -> DOP2(Prod,c,DLAM(name,typrec (n+1) t))
+      | x -> let lAV = destAppL(ensure_appl x) in
+             let (_,vargs) = array_chop (nparams+1) lAV in
+             appvect (lift n p,vargs)
+  in
+  typrec 0 (hnf_prod_applist env sigma "type_case" t globargs)
 
-let find_type_case_branches sigma env (current,ind_data,_) p =
+let find_type_case_branches isevars env (current,ind_data,_) p =
   let {fullmind=ct;mind=ity;params=params;realargs=args} = ind_data in
   if not (is_for_mlcase p) then
 
     (* En attendant mieux ... *)
-    let pt = get_type_of env sigma p in
+    let pt = get_type_of env !isevars p in
 
-    let evalpt = nf_ise1 sigma pt in
-    let (_,bty,_)= type_case_branches env sigma ct evalpt p current
+    let evalpt = nf_ise1 !isevars pt in
+    let (_,bty,_)= type_case_branches env !isevars ct evalpt p current
     in bty
   else
-    let build_branch i = my_norec_branch_scheme env sigma i ct in
+    let build_branch i = my_norec_branch_scheme env isevars i ct in
     let lbr = List.map build_branch (interval 1 ind_data.nconstr)
     in  Array.of_list lbr
-
+*)
 
 (* if ityparam :(d_bar:D_bar)s
  * then we abstract the dependencies and the object building the non-binding
@@ -1239,7 +1246,7 @@ and build_dep_branch trad env gd bty (current,ind_data,info) i =
  let ngd =  pop_and_prepend_tomatch lpatt gd in
  let ci_param = applist (ith_constructor i ind_data, params) in
 
- let rnnext_env0,next_mat = submat ngd.case_dep sigma env i 
+ let rnnext_env0,next_mat = submat ngd.case_dep trad.isevars env i 
                                     ind_data params current ngd.mat in
  let next_predicate = insert_constraint env ngd bty.(i-1) 
                                        ((current,info),ci_param)  in
@@ -1317,7 +1324,7 @@ and build_nondep_branch trad env gd next_pred bty
  let lp = List.map (lift k) params in
  let ci = applist (ith_constructor i ind_data, lp@(rel_list 0 k)) in 
 
- let rnnext_env0,next_mat=submat ngd.case_dep !(trad.isevars) next_env i 
+ let rnnext_env0,next_mat=submat ngd.case_dep trad.isevars next_env i 
                                  ind_data lp nncur ngd.mat in
 
  if next_mat = [] then
@@ -1394,7 +1401,7 @@ and match_current trad env (current,ind_data,info as cji) gd =
    build_predicate !(trad.isevars) env cji gd in
 
   (* we build the branches *)
-  let bty = find_type_case_branches !(trad.isevars) env cji p  in
+  let bty = find_type_case_branches !(trad.isevars) env false ind_data p  in
 
   let build_ith_branch gd = build_nondep_branch trad env gd 
                                next_pred bty cji   in
@@ -1416,13 +1423,14 @@ and match_current trad env (current,ind_data,info as cji) gd =
 	    if not (Evarconv.the_conv_x_leq env trad.isevars lft.(i) bty.(i))
 	    then 
 	      let c = nf_ise1 !(trad.isevars) current
-	      and lfi = nf_betaiota env !(trad.isevars) (nf_ise1 !(trad.isevars) lf.(i)) in
+	      and lfi = nf_betaiota env !(trad.isevars) (nf_ise1 !(trad.isevars) lft.(i)) in
 	      error_ill_formed_branch CCI env c i lfi (nf_betaiota env !(trad.isevars) bty.(i))
 	    else check_conv (i+1)
 	in
 	check_conv 0;
         (common_prefix_ctxt (context env) bre1,
-         mkMutCaseA (ci_of_mind (mutind_of_ind ity)) (eta_reduce_if_rel p)
+         mkMutCaseA (ci_of_mind (mutind_of_ind ity))
+	   (eta_reduce_if_rel (nf_ise1 !(trad.isevars) p))
 	   current lf) in
     newenv,
     {uj_val = v;
@@ -1488,7 +1496,7 @@ and match_current_dep trad env (current,ind_data,info as cji) gd =
   let np=whd_constraint p in
   
   (* we build the branches *)
-  let bty = find_type_case_branches !(trad.isevars) nenv cji np  in
+  let bty = find_type_case_branches !(trad.isevars) nenv true ind_data np in
 
   let build_ith_branch env gd = build_dep_branch trad env gd bty cji in
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 5af5fb9156..d80810af51 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -114,12 +114,12 @@ and evar_conv_x env isevars pbty term1 term2 =
       (add_conv_pb (pbty,applist(t1,l1),applist(t2,l2)); true)
     else 
       evar_eqappr_x env isevars pbty (t1,l1) (t2,l2)
-	
+
 and evar_eqappr_x env isevars pbty appr1 appr2 =
+  (* Evar must be undefined since we have whd_ised *)
   match (appr1,appr2) with
-    | ((DOPN(Const sp1,al1) as term1,l1), (DOPN(Const sp2,al2) as term2,l2)) ->
-	let f1 () = 
-      	  (ise_undefined isevars term1 or ise_undefined isevars term2) &
+    | ((DOPN(Evar sp1,al1) as term1,l1), (DOPN(Evar sp2,al2) as term2,l2)) ->
+	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)
@@ -132,6 +132,43 @@ and evar_eqappr_x env isevars pbty appr1 appr2 =
           (sp1 = sp2)
 	  & (array_for_all2 (evar_conv_x env isevars CONV) al1 al2)  
 	  & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
+	in 
+	ise_try isevars [f1; f2]
+
+    | ((DOPN(Evar sp1,al1) as term1,l1), (DOPN(Const sp2,al2) as term2,l2)) ->
+	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))
+          & list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2
+	and f4 () =
+          if evaluable_constant env term2 then
+            evar_eqappr_x env isevars pbty
+              appr1 (evar_apprec env isevars l2 (constant_value env term2))
+          else false
+	in 
+	ise_try isevars [f1; f4]
+
+    | ((DOPN(Const sp1,al1) as term1,l1), (DOPN(Evar sp2,al2) as term2,l2)) ->
+	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)
+          & list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2
+	and f4 () =
+          if evaluable_constant env term1 then
+            evar_eqappr_x env isevars pbty
+              (evar_apprec env isevars l1 (constant_value env term1)) appr2
+          else 
+	    false
+	in 
+	ise_try isevars [f1; f4]
+
+    | ((DOPN(Const sp1,al1) as term1,l1), (DOPN(Const sp2,al2) as term2,l2)) ->
+	let f2 () =
+          (sp1 = sp2)
+	  & (array_for_all2 (evar_conv_x env isevars CONV) al1 al2)  
+	  & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
 	and f3 () =
 	  (try conv_record env isevars 
              (try check_conv_record appr1 appr2
@@ -147,41 +184,41 @@ and evar_eqappr_x env isevars pbty appr1 appr2 =
           else 
 	    false
 	in 
-	ise_try isevars [f1; f2; f3; f4]
-
-    | ((DOPN(Const _,_) as term1,l1),(t2,l2)) ->  
-	let f1 () =
-       	  ise_undefined isevars term1 &
-       	  (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(t2,deb2))
-          & list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2
-	and f2 () =
+	ise_try isevars [f2; f3; f4]
+
+    | ((DOPN(Evar _,_) as term1,l1),(t2,l2)) ->
+       	(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(t2,deb2))
+        & list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2
+
+    | ((t1,l1),(DOPN(Evar _,_) as t2,l2))  -> 
+       	(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(t1,deb1),t2)
+        & list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2
+
+    | ((DOPN(Const _,_) as term1,l1),(t2,l2)) ->
+	let f3 () =
 	  (try conv_record env isevars (check_conv_record appr1 appr2)
            with _ -> false)
-	and f3 () = 
+	and f4 () = 
 	  evaluable_constant env term1 &
  	  evar_eqappr_x env isevars pbty
             (evar_apprec env isevars l1 (constant_value env term1)) appr2
 	in 
-	ise_try isevars [f1; f2; f3]
+	ise_try isevars [f3; f4]
 	     
     | ((t1,l1),(DOPN(Const _,_) as t2,l2))  -> 
-	let f1 () =
-       	  ise_undefined isevars t2 &
-       	  (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(t1,deb1),t2)
-          & list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2
-	and f2 () = 
+	let f3 () = 
 	  (try (conv_record env isevars (check_conv_record appr2 appr1))
            with _ -> false)
-	and f3 () =
+	and f4 () =
           evaluable_constant env t2 &
  	  evar_eqappr_x env isevars pbty
             appr1 (evar_apprec env isevars l2 (constant_value env t2))
 	in 
-	ise_try isevars [f1; f2; f3]
+	ise_try isevars [f3; f4]
 
     | ((DOPN(Abst _,_) as term1,l1),(DOPN(Abst _,_) as term2,l2)) ->
 	let f1 () =