Ajout construction If primitive dans constr_expr et rawconstr

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

16 files changed, 174 insertions, 116 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 3e4d486a8f..afa9226e11 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -323,6 +323,10 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
 		   CT_if(xlate_formula_opt po,
                    xlate_formula c,xlate_formula b1,xlate_formula b2)		
    | CLetTuple (_,l, (na,po), c, b) -> xlate_error "LetTuple: TODO"
+   | CIf (_,c, (na,None), b1, b2) ->
+		   CT_if(ctv_FORMULA_OPT_NONE,
+                   xlate_formula c,xlate_formula b1,xlate_formula b2)
+   | CIf (_,c, (na,Some p), b1, b2) -> xlate_error "If: TODO"
 
    | COrderedCase (_,Term.LetStyle, po, c, [CLambdaN(_,[l,_],b)]) ->
        CT_inductive_let(xlate_formula_opt po,
diff --git a/interp/reserve.ml b/interp/reserve.ml
index daffc3945a..5c9c3a6885 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -53,6 +53,8 @@ let rec unloc = function
       (dummy_loc,b,option_app unloc tyopt,unloc tm, Array.map unloc bv,x)
   | RLetTuple (_,nal,(na,po),b,c) ->
       RLetTuple (dummy_loc,nal,(na,option_app unloc po),unloc b,unloc c)
+  | RIf (_,c,(na,po),b1,b2) ->
+      RIf (dummy_loc,unloc c,(na,option_app unloc po),unloc b1,unloc b2)
   | RRec (_,fk,idl,tyl,bv) ->
       RRec (dummy_loc,fk,idl,Array.map unloc tyl,Array.map unloc bv)
   | RCast (_,c,t) -> RCast (dummy_loc,unloc c,unloc t)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 17a4410200..c3b44b9e2c 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -33,6 +33,7 @@ type aconstr =
       (identifier list * cases_pattern list * aconstr) list
   | AOrderedCase of case_style * aconstr option * aconstr * aconstr array
   | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
+  | AIf of aconstr * (name * aconstr option) * aconstr * aconstr
   | ASort of rawsort
   | AHole of hole_kind
   | APatVar of patvar
@@ -69,6 +70,8 @@ let map_aconstr_with_binders_loc loc g f e = function
       ROrderedCase (loc,b,option_app (f e) tyopt,f e tm,Array.map (f e) bv,ref None)
   | ALetTuple (nal,(na,po),b,c) ->
       RLetTuple (loc,nal,(na,option_app (f e) po),f e b,f e c)
+  | AIf (c,(na,po),b1,b2) ->
+      RIf (loc,f e c,(na,option_app (f e) po),f e b1,f e b2)
   | ACast (c,t) -> RCast (loc,f e c,f e t)
   | ASort x -> RSort (loc,x)
   | AHole x  -> RHole (loc,x)
@@ -151,6 +154,14 @@ let rec subst_aconstr subst raw =
 	if po' == po && b' == b && c' == c then raw else
 	  ALetTuple (nal,(na,po'),b',c')
 
+  | AIf (c,(na,po),b1,b2) ->
+      let po' = option_smartmap (subst_aconstr subst) po
+      and b1' = subst_aconstr subst b1
+      and b2' = subst_aconstr subst b2 
+      and c' = subst_aconstr subst c in
+	if po' == po && b1' == b1 && b2' == b2 && c' == c then raw else
+	  AIf (c',(na,po'),b1',b2')
+
   | APatVar _ | ASort _ -> raw
 
   | AHole (ImplicitArg (ref,i)) ->
@@ -196,6 +207,8 @@ let aconstr_of_rawconstr vars a =
       AOrderedCase (b,option_app aux tyopt,aux tm, Array.map aux bv)
   | RLetTuple (loc,nal,(na,po),b,c) ->
       ALetTuple (nal,(na,option_app aux po),aux b,aux c)
+  | RIf (loc,c,(na,po),b1,b2) ->
+      AIf (aux c,(na,option_app aux po),aux b1,aux b2)
   | RCast (_,c,t) -> ACast (aux c,aux t)
   | RSort (_,s) -> ASort s
   | RHole (_,w) -> AHole w
@@ -416,6 +429,8 @@ type constr_expr =
       * constr_expr list
   | CLetTuple of loc * name list * (name * constr_expr option) *
       constr_expr * constr_expr
+  | CIf of loc * constr_expr * (name * constr_expr option)
+      * constr_expr * constr_expr
   | CHole of loc
   | CPatVar of loc * (bool * patvar)
   | CEvar of loc * existential_key
@@ -459,6 +474,7 @@ let constr_loc = function
   | CCases (loc,_,_,_) -> loc
   | COrderedCase (loc,_,_,_,_) -> loc
   | CLetTuple (loc,_,_,_,_) -> loc
+  | CIf (loc,_,_,_,_) -> loc
   | CHole loc -> loc
   | CPatVar (loc,_) -> loc
   | CEvar (loc,_) -> loc
@@ -498,6 +514,7 @@ let rec occur_var_constr_expr id = function
   | CCases (loc,_,_,_) 
   | COrderedCase (loc,_,_,_,_) 
   | CLetTuple (loc,_,_,_,_) 
+  | CIf (loc,_,_,_,_) 
   | CFix (loc,_,_) 
   | CCoFix (loc,_,_) -> 
       Pp.warning "Capture check in multiple binders not done"; false
@@ -560,6 +577,9 @@ let map_constr_expr_with_binders f g e = function
       let e' = List.fold_right (name_fold g) nal e in
       let e'' = name_fold g na e in
       CLetTuple (loc,nal,(na,option_app (f e'') po),f e b,f e' c)
+  | CIf (loc,c,(na,po),b1,b2) ->
+      let e' = name_fold g na e in
+      CIf (loc,f e c,(na,option_app (f e') po),f e b1,f e b2)
   | CFix (loc,id,dl) ->
       CFix (loc,id,List.map (fun (id,n,t,d) -> (id,n,f e t,f e d)) dl)
   | CCoFix (loc,id,dl) ->
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 071af9d374..1636edfd3b 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -34,6 +34,7 @@ type aconstr =
       (identifier list * cases_pattern list * aconstr) list
   | AOrderedCase of case_style * aconstr option * aconstr * aconstr array
   | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
+  | AIf of aconstr * (name * aconstr option) * aconstr * aconstr
   | ASort of rawsort
   | AHole of hole_kind
   | APatVar of patvar
@@ -91,6 +92,8 @@ type constr_expr =
       * constr_expr list
   | CLetTuple of loc * name list * (name * constr_expr option) *
       constr_expr * constr_expr
+  | CIf of loc * constr_expr * (name * constr_expr option)
+      * constr_expr * constr_expr
   | CHole of loc
   | CPatVar of loc * (bool * patvar)
   | CEvar of loc * existential_key
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 60848fdfd0..88c8211670 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -295,6 +295,9 @@ let subst_constr_expr a loc subs =
       let na = name_app (subst_id subs) na in
       let nal = List.map (name_app (subst_id subs)) nal in
       CLetTuple (loc,nal,(na,option_app subst po),subst a,subst b)
+  | CIf (_,c,(na,po),b1,b2) ->
+      let na = name_app (subst_id subs) na in
+      CIf (loc,subst c,(na,option_app subst po),subst b1,subst b2)
   | CFix (_,id,dl) ->
       CFix (loc,id,List.map (fun (id,n,t,d) -> (id,n,subst t,subst d)) dl)
   | CCoFix (_,id,dl) ->
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index 700ac67349..9aed2b1d55 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -204,9 +204,10 @@ GEXTEND Gram
 	  po = return_type;
 	  ":="; c1 = operconstr; "in"; c2 = operconstr LEVEL "200" ->
           CLetTuple (loc,List.map snd lb,po,c1,c2)
-      | "if"; c1=operconstr; "then"; c2=operconstr LEVEL "200";
-        "else"; c3=operconstr LEVEL "200" ->
-          COrderedCase (loc, IfStyle, None, c1, [c2; c3])
+      | "if"; c=operconstr; po = return_type;
+	"then"; b1=operconstr LEVEL "200";
+        "else"; b2=operconstr LEVEL "200" ->
+          CIf (loc, c, po, b1, b2)
       | c=fix_constr -> c ] ]
   ;
   appl_arg:
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 7421460539..af651a4f20 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -262,7 +262,7 @@ let rec pr inherited a =
 	  str "if " ++ pr ltop c ++ spc () ++
 	  hov 0 (str "then" ++ brk (1,1) ++ pr ltop b1) ++ spc () ++
 	  hov 0 (str "else" ++ brk (1,1) ++ pr ltop b2))), lif
-  | CLetTuple (_,nal,(na,po),c,b) ->
+  | CLetTuple _ | CIf _ ->
       error "Let tuple not supported in v7"
 
   | COrderedCase (_,(MatchStyle|RegularStyle as style),po,c,bl) ->
diff --git a/parsing/termast.ml b/parsing/termast.ml
index b4914583e9..da683e5fa8 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -257,7 +257,7 @@ let rec ast_of_raw = function
 	    ::(ast_of_raw tm)
 	    ::(Array.to_list (Array.map ast_of_raw bv)))
 
-  | RLetTuple (loc,nal,(na,typopt),tm,b) ->
+  | RLetTuple _ | RIf _ ->
       error "Let tuple not supported in v7"
 
   | RRec (_,fk,idv,tyv,bv) ->
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index e2aa74cba5..a79c2a523c 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -130,10 +130,11 @@ let count_rec_arg j =
  * [a_bar:A'_bar](lift k pred) 
  * where A'_bar = A_bar[p_bar <- globargs] *)
 
-let build_notdep_pred env sigma indf pred =
+let build_dep_pred env sigma indf pred =
   let arsign,_ = get_arity env indf in
-  let nar = List.length arsign in
-  it_mkLambda_or_LetIn_name env (lift nar pred) arsign
+  let psign = (Anonymous,None,build_dependent_inductive env indf)::arsign in
+  let nar = List.length psign in
+  it_mkLambda_or_LetIn_name env (lift nar pred) psign
 
 type ml_case_error =
   | MlCaseAbsurd
@@ -157,10 +158,7 @@ let pred_case_ml env sigma isrec (IndType (indf,realargs)) (i,ft) =
     else 
       raise (NotInferable MlCaseDependent)
   in
-  if realargs = [] then 
-    pred
-  else (* we try with [_:T1]..[_:Tn](lift n pred) *)
-    build_notdep_pred env sigma indf pred  
+  build_dep_pred env sigma indf pred  
 
 (************************************************************************)
 (*            Pattern-matching compilation (Cases)                      *)
@@ -597,9 +595,11 @@ let occur_rawconstr id =
 	or (List.exists occur_pattern pl)
     | ROrderedCase (loc,b,tyopt,tm,bv,_) -> 
 	(occur_option tyopt) or (occur tm) or (array_exists occur bv)
-    | RLetTuple (loc,nal,(na,tyopt),b,c) -> 
-	(na <> Name id & occur_option tyopt)
+    | RLetTuple (loc,nal,rtntyp,b,c) -> 
+	occur_return_type rtntyp id
         or (occur b) or (not (List.mem (Name id) nal) & (occur c))
+    | RIf (loc,c,rtntyp,b1,b2) -> 
+	occur_return_type rtntyp id or (occur c) or (occur b1) or (occur b2)
     | RRec (loc,fk,idl,tyl,bv) ->
 	(array_exists occur tyl) or
 	(not (array_exists (fun id2 -> id=id2) idl) & array_exists occur bv)
@@ -610,6 +610,8 @@ let occur_rawconstr id =
 
   and occur_option = function None -> false | Some p -> occur p
 
+  and occur_return_type (na,tyopt) id = na <> Name id & occur_option tyopt
+
   in occur
 
 let occur_in_rhs na rhs =
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 49034b1b1f..00895a1f65 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -276,6 +276,8 @@ let detype_case computable detype detype_eqn tenv avoid env indsp st p k c bl =
                     | _ -> (RApp (dummy_loc,p,[a]))) in
       let (nal,d) = decomp_lam_force consnargsl.(0) avoid [] bl.(0) in
       RLetTuple (dummy_loc,nal,(alias,newpred),tomatch,d)
+    else if not !Options.v7 && tag = IfStyle && aliastyp = None then
+      RIf (dummy_loc,tomatch,(alias,newpred),bl.(0),bl.(1))
     else
       let rec remove_type avoid args c =
 	match c,args with
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 78c23ae61e..bf7e13158c 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -464,29 +464,25 @@ let build_indrec env sigma ind =
 (**********************************************************************)
 (* To handle old Case/Match syntax in Pretyping                       *)
 
-(***********************************)
+(*****************************************)
 (* To interpret Case and Match operators *)
+(* Expects a dependent predicate *)
 
-let type_rec_branches recursive env sigma indt pj c = 
+let type_rec_branches recursive env sigma indt p c = 
   let IndType (indf,realargs) = indt in
-  let p = pj.uj_val in
   let (ind,params) = dest_ind_family indf in
   let (mib,mip) = lookup_mind_specif env ind in
   let recargs = mip.mind_recargs in
   let tyi = snd ind in
-  let is_rec = recursive && mis_is_recursive_subset [tyi] recargs in
-  let dep = is_dependent_elimination env pj.uj_type indf in 
-  let init_depPvec i = if i = tyi then Some(dep,p) else None in
+  let init_depPvec i = if i = tyi then Some(true,p) else None in
   let depPvec = Array.init mib.mind_ntypes init_depPvec in
   let vargs = Array.of_list params in
   let constructors = get_constructors env indf in
   let lft =
     array_map2
-      (type_rec_branch recursive dep env sigma (params,depPvec,0) tyi)
+      (type_rec_branch recursive true env sigma (params,depPvec,0) tyi)
       constructors (dest_subterms recargs) in
-  (lft,
-   if dep then Reduction.beta_appvect p (Array.of_list (realargs@[c])) 
-   else Reduction.beta_appvect p (Array.of_list realargs))
+  (lft,Reduction.beta_appvect p (Array.of_list (realargs@[c])))
 (* Non recursive case. Pb: does not deal with unification
     let (p,ra,_) = type_case_branches env (ind,params@realargs) pj c in
     (p,ra)
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index 65fefb83fd..38d07d1d90 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -42,7 +42,7 @@ val build_mutual_indrec :
 (* These are for old Case/Match typing *)
 
 val type_rec_branches : bool -> env -> evar_map -> inductive_type
-  -> unsafe_judgment -> constr -> constr array * constr
+  -> constr -> constr -> constr array * constr
 val make_rec_branch_arg : 
   env -> evar_map ->
     int * ('b * constr) option array * int ->
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index d3479a8466..f453e911e4 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -241,6 +241,9 @@ let rec pat_of_raw metas vars = function
       PCase ((None,st),option_app (pat_of_raw metas vars) po,
              pat_of_raw metas vars c,
              Array.map (pat_of_raw metas vars) br)
+  | RIf (_,c,(_,None),b1,b2) ->
+      PCase ((None,IfStyle),None, pat_of_raw metas vars c,
+             [|pat_of_raw metas vars b1; pat_of_raw metas vars b2|])
   | RCases (loc,(po,_),[c,_],brs) ->
       let sp =
 	match brs with
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index ffbca83eac..0dbcaef448 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -349,7 +349,9 @@ let rec pretype tycon env isevars lvar = function
       let fsign = List.map2 (fun na (_,c,t) -> (na,c,t))
         (List.rev nal) cs.cs_args in
       let env_f = push_rels fsign env in
+      (* Make dependencies from arity signature impossible *)
       let arsgn,_ = get_arity env indf in
+      let arsgn = List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn in
       let psign = (na,None,build_dependent_inductive env indf)::arsgn in
       let nar = List.length arsgn in
       (match po with
@@ -410,7 +412,7 @@ let rec pretype tycon env isevars lvar = function
 	     let pj = if dep then pj else make_dep_of_undep env indt pj in
 	     let (bty,rsty) = 
 	       Indrec.type_rec_branches 
-		 false env (evars_of isevars) indt pj cj.uj_val 
+		 false env (evars_of isevars) indt pj.uj_val cj.uj_val 
 	     in
 	     if Array.length bty <> 1 then
 	       error_number_branches_loc 
@@ -443,6 +445,10 @@ let rec pretype tycon env isevars lvar = function
                (* may be Type while Prop or Set would be expected *)
 	       match tycon with
 		 | Some pred ->
+		     let arsgn = make_arity_signature env true indf in
+  		     let pred = 
+		       it_mkLambda_or_LetIn (nf_evar (evars_of isevars) pred)
+			 arsgn in
                      false,
 		     Retyping.get_judgment_of env (evars_of isevars) pred
 	         | None ->
@@ -461,19 +467,21 @@ let rec pretype tycon env isevars lvar = function
 		   let pty =
                      Retyping.get_type_of env (evars_of isevars) pred in
 		   let pj = { uj_val = pred; uj_type = pty } in
+(*
                    let _ = 
 		     option_app (the_conv_x_leq env isevars pred) tycon 
 		   in
+*)
 		   true, pj
 	       with Cases.NotInferable _ ->
 		 use_constraint ()
 	     in 
 	     let pj = j_nf_evar (evars_of isevars) pj in
-	     let pj = make_dep_of_undep env indt pj in
 	     let (bty,rsty) =
 	       Indrec.type_rec_branches
-		 false env (evars_of isevars) indt pj cj.uj_val 
+		 false env (evars_of isevars) indt pj.uj_val cj.uj_val 
 	     in
+	     let _ = option_app (the_conv_x_leq env isevars rsty) tycon in
 	     let fj = 
 	       if ok then fj 
 	       else pretype (mk_tycon bty.(0)) env isevars lvar f 
@@ -588,6 +596,80 @@ let rec pretype tycon env isevars lvar = function
       (* End building the v8 syntax *)
       j
 
+  | RIf (loc,c,(na,po),b1,b2) ->
+      let cj = pretype empty_tycon env isevars lvar c in
+      let (IndType (indf,realargs) as indt) = 
+	try find_rectype env (evars_of isevars) cj.uj_type
+	with Not_found ->
+	  let cloc = loc_of_rawconstr c in
+	  error_case_not_inductive_loc cloc env (evars_of isevars) cj in
+      (* Make dependencies from arity signature impossible *)
+      let arsgn,_ = get_arity env indf in
+      let arsgn = List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn in
+      let psign = (na,None,build_dependent_inductive env indf)::arsgn in
+      let nar = List.length arsgn in
+      let p = 
+	match po with
+	| Some p ->
+            let env_p = push_rels psign env in
+            let pj = pretype_type empty_valcon env_p isevars lvar p in
+            let ccl = nf_evar (evars_of isevars) pj.utj_val in
+	    it_mkLambda_or_LetIn ccl psign
+	| None ->
+            (* get type information from type of branches *)
+	    let expbr = Cases.branch_scheme env isevars false indf in
+	    try
+	      let fj = pretype (mk_tycon expbr.(0)) env isevars lvar b1 in
+	      let pred = 
+		Cases.pred_case_ml
+                  env (evars_of isevars) false indt (0,fj.uj_type) in
+	      if has_undefined_isevars isevars pred then 
+		raise Not_found
+	      else
+(*
+                let _ = option_app (the_conv_x_leq env isevars pred) tycon in
+*)
+                pred
+	    with Cases.NotInferable _ | Not_found ->
+	    try
+	      let fj = pretype (mk_tycon expbr.(1)) env isevars lvar b2 in
+	      let pred = 
+		Cases.pred_case_ml
+                  env (evars_of isevars) false indt (1,fj.uj_type) in
+	      if has_undefined_isevars isevars pred then 
+		raise Not_found
+	      else
+(*
+                let _ = option_app (the_conv_x_leq env isevars pred) tycon in
+*)
+                pred
+	    with Cases.NotInferable _ | Not_found ->
+            (* get type information from constraint *)
+            (* warning: if the constraint comes from an evar type, it *)
+            (* may be Type while Prop or Set would be expected *)
+	    match tycon with
+	      | Some pred ->
+		  let arsgn = make_arity_signature env true indf in
+  		  it_mkLambda_or_LetIn (nf_evar (evars_of isevars) pred) arsgn 
+	      | None ->
+                  let sigma = evars_of isevars in
+                  error_cant_find_case_type_loc loc env sigma cj.uj_val in
+      let (bty,rsty) =
+	Indrec.type_rec_branches false
+	  env (evars_of isevars) indt p cj.uj_val in
+      let _ = option_app (the_conv_x_leq env isevars rsty) tycon in
+      if Array.length bty <> 2 then
+        user_err_loc (loc,"",
+	  str "If is only for inductive types with two constructors");
+      let bj1 = pretype (mk_tycon bty.(0)) env isevars lvar b1 in
+      let bj2 = pretype (mk_tycon bty.(1)) env isevars lvar b2 in
+      let v =
+	let mis,_ = dest_ind_family indf in
+	let ci = make_default_case_info env IfStyle mis in
+	mkCase (ci, p, cj.uj_val, [|bj1.uj_val;bj2.uj_val|])
+      in
+      { uj_val = v; uj_type = rsty }
+
   | ROrderedCase (loc,st,po,c,lf,x) ->
       let isrec = (st = MatchStyle) in
       let cj = pretype empty_tycon env isevars lvar c in
@@ -615,7 +697,11 @@ let rec pretype tycon env isevars lvar = function
                 (* may be Type while Prop or Set would be expected *)
 	        match tycon with
 		  | Some pred ->
-                      (false,
+		      let arsgn = make_arity_signature env true indf in
+  		      let pred = 
+			it_mkLambda_or_LetIn (nf_evar (evars_of isevars) pred)
+			  arsgn in
+                      (true, 
                        Retyping.get_judgment_of env (evars_of isevars) pred)
 	          | None ->
                       let sigma = evars_of isevars in
@@ -626,15 +712,18 @@ let rec pretype tycon env isevars lvar = function
 		  let fj =
 		    pretype (mk_tycon expti) env isevars lvar lf.(i) in
 		  let pred = 
-		    Cases.pred_case_ml
+		    Cases.pred_case_ml (* eta-expanse *)
                       env (evars_of isevars) isrec indt (i,fj.uj_type) in
 		  if has_undefined_isevars isevars pred then findtype (i+1)
 		  else 
 		    let pty =
                       Retyping.get_type_of env (evars_of isevars) pred in
 		    let pj = { uj_val = pred; uj_type = pty } in
+(*
                     let _ = option_app (the_conv_x_leq env isevars pred) tycon
-                    in (false,pj)
+                    in
+*)
+                    (true,pj)
 		with Cases.NotInferable _ -> findtype (i+1) in
 	    findtype 0 
       in
@@ -642,7 +731,8 @@ let rec pretype tycon env isevars lvar = function
       let pj = if dep then pj else make_dep_of_undep env indt pj in
       let (bty,rsty) =
 	Indrec.type_rec_branches
-          isrec env (evars_of isevars) indt pj cj.uj_val in
+          isrec env (evars_of isevars) indt pj.uj_val cj.uj_val in
+      let _ = option_app (the_conv_x_leq env isevars rsty) tycon in
       if Array.length bty <> Array.length lf then
 	error_number_branches_loc loc env (evars_of isevars) 
 	  cj (Array.length bty)
@@ -676,67 +766,6 @@ let rec pretype tycon env isevars lvar = function
             Some (Detyping.detype env 
 	      (ids_of_context env) (names_of_rel_context env)
               (nf_evar (evars_of isevars) v))
-  (*
-            let sigma = evars_of isevars in
-            let init_depFvec i = if i = tyi then Some(dep,mkRel 1) else None in
-            let depFvec = Array.init mib.mind_ntypes init_depFvec in
-            (* build now the fixpoint *)
-            let lnames,_ = get_arity env indf in
-            let nar = List.length lnames in
-            let nparams = mip.mind_nparams in
-            let constrs = get_constructors env (lift_inductive_family (nar+2) indf) in
-            let branches = 
-              array_map3
-	        (fun f t reca -> 
-	          whd_beta
-                  (Indrec.make_rec_branch_arg env sigma
-                    (nparams,depFvec,nar+1)
-                    f t reca))
-                (Array.map (lift (nar+2)) lfv) constrs (dest_subterms recargs) 
-            in 
-            let ci = make_default_case_info env RegularStyle ind in
-            let deffix = 
-              it_mkLambda_or_LetIn_name env
-	        (lambda_create env
-	          (applist (mI,List.append (List.map (lift (nar+1)) params)
-                    (extended_rel_list 0 lnames)),
-                  mkCase (ci, lift (nar+2) pj.uj_val, mkRel 1, branches)))
-                (lift_rel_context 1 lnames) 
-            in
-            if noccurn 1 deffix then 
-              Some
-                (Detyping.detype env [] (names_of_rel_context env)
-                  (whd_beta (applist (pop deffix,realargs@[cj.uj_val]))))
-            else
-              let ind = applist (mI,(List.append 
-		(List.map (lift nar) params)
-		(extended_rel_list 0 lnames))) in
-              let typPfix =
-                let rec aux = function
-                  | (na,Some b,t)::l -> 
-                  | (na,None,t)::l -> RProd (dummy_loc,na,
-                  | [] -> 
-	        it_mkProd_or_LetIn_name env
-	          (prod_create env 
-	            (ind,
-	            (if dep then
-		      let ext_lnames = (Anonymous,None,ind)::lnames in
-		      let args = extended_rel_list 0 ext_lnames in
-		      whd_beta (applist (lift (nar+1) p, args))
-	            else
-		      let args = extended_rel_list 1 lnames in
-		      whd_beta (applist (lift (nar+1) p, args)))))
-                  lnames in
-              let fix =
-                RRec (dummy_loc,RFix ([|nar|],0),
-	        ([|(id_of_string "F")|],[|typPfix|],[|deffix|])) in
-              RApp (dummy_loc,fix,realargs@[c])
-              (msgerrnl (str "Warning: could't translate Match"); None)
-*)
-          else if st = IfStyle & po = None then
-	    (* Translate into a "if ... then ... else" *)
-	    (* TODO: translate into a "if" even if po is dependent *)
-	    None
 	  else
 	    (* Translate into a "match ... with" *)
             let rtntypopt, indnalopt = match po with
@@ -762,10 +791,10 @@ let rec pretype tycon env isevars lvar = function
                     else [Anonymous],p,[] in
                   let args = List.map (fun _ -> Anonymous) params @ nal in
                   (Some rtntyopt,(List.hd na,Some (dummy_loc,ind,args))) in
-	    if st = IfStyle & po = None then
+	    if st = IfStyle & snd indnalopt = None then
 	      (* Translate into a "if ... then ... else" *)
 	      (* TODO: translate into a "if" even if po is dependent *)
-	      None
+	      Some (RIf (loc,c,(fst indnalopt,rtntypopt),lf.(0),lf.(1)))
 	    else
             let detype_eqn constr construct_nargs branch =
               let name_cons = function 
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index bdb6914c24..a1eb589ff3 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -75,6 +75,7 @@ type rawconstr =
       rawconstr array * rawconstr option ref
   | RLetTuple of loc * name list * (name * rawconstr option) * 
       rawconstr * rawconstr
+  | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
   | RRec of loc * fix_kind * identifier array * 
       rawconstr array * rawconstr array
   | RSort of loc * rawsort
@@ -97,24 +98,6 @@ let cases_predicate_names tml =
    - boolean in POldCase means it is recursive
 i*)
 
-let loc = function
-  | RVar (loc,_) -> loc
-  | RApp (loc,_,_) -> loc
-  | RLambda (loc,_,_,_) -> loc
-  | RProd (loc,_,_,_) -> loc
-  | RLetIn (loc,_,_,_) -> loc
-  | RCases (loc,_,_,_) -> loc
-  | ROrderedCase (loc,_,_,_,_,_) -> loc
-  | RLetTuple (loc,_,_,_,_) -> loc
-  | RRec (loc,_,_,_,_) -> loc
-  | RCast (loc,_,_) -> loc
-  | RSort (loc,_) -> loc
-  | RHole (loc,_) -> loc
-  | RRef (loc,_) -> loc
-  | REvar (loc,_) -> loc
-  | RPatVar (loc,_) -> loc
-  | RDynamic (loc,_) -> loc
-
 let map_rawconstr f = function
   | RVar (loc,id) -> RVar (loc,id)
   | RApp (loc,g,args) -> RApp (loc,f g, List.map f args)
@@ -129,6 +112,8 @@ let map_rawconstr f = function
       ROrderedCase (loc,b,option_app f tyopt,f tm, Array.map f bv,ref (option_app f !x))
   | RLetTuple (loc,nal,(na,po),b,c) ->
       RLetTuple (loc,nal,(na,option_app f po),f b,f c)
+  | RIf (loc,c,(na,po),b1,b2) ->
+      RIf (loc,f c,(na,option_app f po),f b1,f b2)
   | RRec (loc,fk,idl,tyl,bv) -> RRec (loc,fk,idl,Array.map f tyl,Array.map f bv)
   | RCast (loc,c,t) -> RCast (loc,f c,f t)
   | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) as x -> x
@@ -248,8 +233,16 @@ let rec subst_raw subst raw =
       and b' = subst_raw subst b 
       and c' = subst_raw subst c in
 	if po' == po && b' == b && c' == c then raw else
-          RLetTuple (loc,nal,(na,po),b,c)
+          RLetTuple (loc,nal,(na,po'),b',c')
       
+  | RIf (loc,c,(na,po),b1,b2) ->
+      let po' = option_smartmap (subst_raw subst) po
+      and b1' = subst_raw subst b1 
+      and b2' = subst_raw subst b2 
+      and c' = subst_raw subst c in
+	if c' == c & po' == po && b1' == b1 && b2' == b2 then raw else
+          RIf (loc,c',(na,po'),b1',b2')
+
   | RRec (loc,fix,ida,ra1,ra2) -> 
       let ra1' = array_smartmap (subst_raw subst) ra1
       and ra2' = array_smartmap (subst_raw subst) ra2 in
@@ -284,6 +277,7 @@ let loc_of_rawconstr = function
   | RCases (loc,_,_,_) -> loc
   | ROrderedCase (loc,_,_,_,_,_) -> loc
   | RLetTuple (loc,_,_,_,_) -> loc
+  | RIf (loc,_,_,_,_) -> loc
   | RRec (loc,_,_,_,_) -> loc
   | RSort (loc,_) -> loc
   | RHole (loc,_) -> loc
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 27bb76b69a..2718cf9bbc 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -72,6 +72,7 @@ type rawconstr =
       rawconstr array * rawconstr option ref
   | RLetTuple of loc * name list * (name * rawconstr option) * 
       rawconstr * rawconstr
+  | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
   | RRec of loc * fix_kind * identifier array * 
       rawconstr array * rawconstr array
   | RSort of loc * rawsort
@@ -94,8 +95,6 @@ val cases_predicate_names :
    - option in PHole tell if the "?" was apparent or has been implicitely added
 i*)
 
-val loc : rawconstr -> loc
-
 val map_rawconstr : (rawconstr -> rawconstr) -> rawconstr -> rawconstr
 
 (*