The "clean integration of subtac" patch.

Adds a new kind of casts (CastCoerce) for coercing an object to its base type (e.g. inductive).
The new cast_type type subsumes usual casts ConvCasts. Much of the patch is just adding ConvCasts where needed.
The Pretyping module has been adapted to this change, although it doesn't change anything yet, but this construct could have 
a use with current coercions also. Pretyping is also cleaned from the "Use type constraints under lambdas" patch which is not yet ready
for wide use. It has been transferred to a copy of the Pretyping Functor in subtac_pretyping_F.ml.
Subtac is now working as well as I demonstrated at TYPES.



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

25 files changed, 829 insertions, 174 deletions

diff --git a/Makefile b/Makefile
index 70e20ac72..fe8d72908 100644
--- a/Makefile
+++ b/Makefile
@@ -301,6 +301,7 @@ SUBTACCMO=\
 	contrib/subtac/context.cmo \
 	contrib/subtac/subtac_errors.cmo \
 	contrib/subtac/subtac_coercion.cmo \
+	contrib/subtac/subtac_pretyping_F.cmo \
 	contrib/subtac/subtac_pretyping.cmo \
 	contrib/subtac/subtac_interp_fixpoint.cmo \
 	contrib/subtac/subtac_command.cmo \
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index 9acb10aef..db10cb2a1 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -1,20 +1,17 @@
 Set Implicit Arguments.
 
+Notation "'fun' { x : A | P } => Q" :=
+  (fun x:{x:A|P} => Q)
+  (at level 200, x ident, right associativity).
+
+Notation "( x & y )" := (@existS _ _ x y) : core_scope.
+
 Definition ex_pi1 (A : Prop) (P : A -> Prop) (t : ex P) : A.
 intros.
 induction t.
 exact x.
 Defined.
 
-Check proj1_sig.
-Lemma subset_simpl : forall (A : Set) (P : A -> Prop)
-  (t : sig P), P (proj1_sig t).
-Proof.
-intros.
-induction t.
- simpl ; auto.
-Qed.
-
 Lemma ex_pi2  : forall (A : Prop) (P : A -> Prop) (t : ex P),
  P (ex_pi1 t).
 intros A P.
@@ -23,12 +20,17 @@ simpl.
 exact p.
 Defined.
 
+
+Notation "` t" := (proj1_sig t) (at level 100) : core_scope.
 Notation "'forall' { x : A | P } , Q" :=
   (forall x:{x:A|P}, Q)
   (at level 200, x ident, right associativity).
 
-Notation "'fun' { x : A | P } => Q" :=
-  (fun x:{x:A|P} => Q)
-  (at level 200, x ident, right associativity).
+Lemma subset_simpl : forall (A : Set) (P : A -> Prop) 
+	(t : sig P), P (` t).
+Proof.
+intros.
+induction t.
+ simpl ; auto.
+Qed.
 
-Notation "( x & y )" := (@existS _ _ x y) : core_scope.
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 4a9cf8eb4..cdad00372 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -97,7 +97,7 @@ module Coercion = struct
 		       app_opt f (mkApp ((Lazy.force sig_).proj1, 
 					 [| u; p; x |]))),
 	       ct)
-	| None -> (None, t)
+	| None -> (None, v)
     in aux t
 
   and coerce loc env isevars (x : Term.constr) (y : Term.constr) 
@@ -153,7 +153,7 @@ module Coercion = struct
 			 if i = Term.destInd existS.typ 
 			 then
 			   begin 
-			     debug 1 (str "In coerce sigma types");
+			     trace (str "In coerce sigma types");
 			     let (a, pb), (a', pb') = 
 			       pair_of_array l, pair_of_array l' 
 			     in
@@ -339,6 +339,13 @@ module Coercion = struct
 	| _ ->
 	    inh_tosort_force loc env isevars j
 
+  let inh_coerce_to_base loc env isevars j =
+    let typ = whd_betadeltaiota env (evars_of isevars) j.uj_type in
+    let ct, typ' = mu env isevars typ in
+      isevars, { uj_val = app_opt ct j.uj_val; 
+		 uj_type = typ' }
+
+
   let inh_coerce_to_fail env isevars c1 v t =
     let v', t' =
       try 
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 24edeba69..552acf137 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -55,8 +55,8 @@ let interp_gen kind isevars env
                ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[]))
                c =
   let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in
-  let c' = Subtac_interp_fixpoint.rewrite_cases env c' in
-    msgnl (str "Pretyping " ++ my_print_constr_expr c);
+  let c' = Subtac_utils.rewrite_cases env c' in
+    trace (str "Pretyping " ++ my_print_constr_expr c);
   let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in
     evar_nf isevars c'
     
@@ -339,13 +339,13 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
       let evm = Evd.evars_of isevars in
       let _, _, typ = arrec.(i) in
       let id = namerec.(i) in
-      let evars_def, evars_typ, evars = Eterm.eterm_term evm def (Some typ) in 	
       (* Generalize by the recursive prototypes  *)
       let def = 
 	Termops.it_mkNamedLambda_or_LetIn def (Environ.named_context rec_sign)
       and typ = 
 	Termops.it_mkNamedProd_or_LetIn typ (Environ.named_context rec_sign) 
       in
+      let evars_def, evars_typ, evars = Eterm.eterm_term evm def (Some typ) in 	
       (*let evars_typ = match evars_typ with Some t -> t | None -> assert(false) in*)
       (*let fi = id_of_string (string_of_id id ^ "_evars") in*)
       (*let ce = 
diff --git a/contrib/subtac/subtac_interp_fixpoint.ml b/contrib/subtac/subtac_interp_fixpoint.ml
index 599dbe39e..858fad1a8 100644
--- a/contrib/subtac/subtac_interp_fixpoint.ml
+++ b/contrib/subtac/subtac_interp_fixpoint.ml
@@ -110,7 +110,7 @@ let rewrite_fixpoint env l (f, decl) =
 	    let body =
 	      (* cast or we will loose some info at pretyping time as body
 		 is a function *)
-	      CCast (dummy_loc, body,  DEFAULTcast, typ) 
+	      CCast (dummy_loc, body,  CastConv DEFAULTcast, typ) 
 	    in
 	    let body' = (* body abstracted by rec call *)
 	      mkLambdaC ([(dummy_loc, Name id)], internal_type, body)
@@ -151,69 +151,3 @@ let rewrite_fixpoint env l (f, decl) =
 			 Ppconstr.pr_constr_expr body')
 	  in (id, (succ n, ro), bl', typ, body'), decl
 
-let list_mapi f = 
-  let rec aux i = function 
-      hd :: tl -> f i hd :: aux (succ i) tl 
-    | [] -> []
-  in aux 0
-
-let rewrite_cases_aux (loc, po, tml, eqns) =
-  let tml = list_mapi (fun i (c, (n, opt)) -> c, 
-		       ((match n with
-			    Name id -> (match c with
-					  | RVar (_, id') when id = id' ->
-					      Name (id_of_string (string_of_id id ^ "'"))
-					  | _ -> n)
-			  | Anonymous -> Name (id_of_string ("x" ^ string_of_int i))),
-			opt)) tml 
-  in
-  let mkHole = RHole (dummy_loc, InternalHole) in
-  let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eqind_ref)),
-		       [mkHole; c; n])
-  in
-  let eqs_types = 
-    List.map
-      (fun (c, (n, _)) ->
-	 let id = match n with Name id -> id | _ -> assert false in
-	 let heqid = id_of_string ("Heq" ^ string_of_id id) in
-	   Name heqid, mkeq c (RVar (dummy_loc, id)))
-      tml
-  in
-  let po = 
-    List.fold_right
-      (fun (n,t) acc ->
-	 RProd (dummy_loc, Anonymous, t, acc))
-      eqs_types (match po with 
-		     Some e -> e
-		   | None -> mkHole)
-  in
-  let eqns =   
-    List.map (fun (loc, idl, cpl, c) ->
-		let c' = 
-		  List.fold_left 
-		    (fun acc (n, t) ->
-		       RLambda (dummy_loc, n, mkHole, acc))
-		    c eqs_types
-		in (loc, idl, cpl, c'))
-      eqns
-  in
-  let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force refl_equal_ref),
-			      [mkHole; c])
-  in
-  let refls = List.map (fun (c, _) -> mk_refl_equal c) tml in
-  let case = RCases (loc,Some po,tml,eqns) in
-  let app = RApp (dummy_loc, case, refls) in
-    app
-
-let rec rewrite_cases c = 
-  match c with 
-      RCases _ -> let c' = map_rawconstr rewrite_cases c in
-	(match c' with 
-	   | RCases (x, y, z, w) -> rewrite_cases_aux (x,y,z,w)
-	   | _ -> assert(false))
-    | _ -> map_rawconstr rewrite_cases c
-	  
-let rewrite_cases env c =
-  let c' = rewrite_cases c in
-  let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in
-    c'
diff --git a/contrib/subtac/subtac_interp_fixpoint.mli b/contrib/subtac/subtac_interp_fixpoint.mli
index 128511c13..fafbb2da5 100644
--- a/contrib/subtac/subtac_interp_fixpoint.mli
+++ b/contrib/subtac/subtac_interp_fixpoint.mli
@@ -26,10 +26,3 @@ val rewrite_fixpoint :
    Topconstr.local_binder list * Topconstr.constr_expr *
    Topconstr.constr_expr) *
   'c
-val list_mapi : (int -> 'a -> 'b) -> 'a list -> 'b list
-val rewrite_cases_aux :
-  Util.loc * Rawterm.rawconstr option * 
-  Rawterm.tomatch_tuple * Rawterm.cases_clauses
-  -> Rawterm.rawconstr
-
-val rewrite_cases : Environ.env -> Rawterm.rawconstr -> Rawterm.rawconstr
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index f73a6e393..1d37900f1 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -39,7 +39,7 @@ open Subtac_errors
 open Context
 open Eterm
 
-module Pretyping = Pretyping.Pretyping_F(Subtac_coercion.Coercion)
+module Pretyping = Subtac_pretyping_F.SubtacPretyping_F(Subtac_coercion.Coercion)
 
 open Pretyping
 
@@ -128,6 +128,7 @@ let subtac_process env isevars id l c tycon =
 	    mk_tycon coqt
   in    
   let c = coqintern !isevars env_binders c in
+  let c = Subtac_utils.rewrite_cases env c in
   let _ = trace (str "Internalized term: " ++ my_print_rawconstr env c) in
   let coqc, ctyp = interp env_binders isevars c tycon in
   let _ = trace (str "Interpreted term: " ++ my_print_constr env_binders coqc ++ spc () ++
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
new file mode 100644
index 000000000..823ff41af
--- /dev/null
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -0,0 +1,639 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Sign
+open Evd
+open Term
+open Termops
+open Reductionops
+open Environ
+open Type_errors
+open Typeops
+open Libnames
+open Nameops
+open Classops
+open List
+open Recordops 
+open Evarutil
+open Pretype_errors
+open Rawterm
+open Evarconv
+open Pattern
+open Dyn
+open Pretyping
+
+(************************************************************************)
+(* This concerns Cases *)
+open Declarations
+open Inductive
+open Inductiveops
+
+module SubtacPretyping_F (Coercion : Coercion.S) = struct
+
+  module Cases = Cases.Cases_F(Coercion)
+
+  (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
+  let allow_anonymous_refs = ref false
+
+  let evd_comb0 f isevars =
+    let (evd',x) = f !isevars in
+      isevars := evd';
+      x
+
+  let evd_comb1 f isevars x =
+    let (evd',y) = f !isevars x in
+      isevars := evd';
+      y
+
+  let evd_comb2 f isevars x y =
+    let (evd',z) = f !isevars x y in
+      isevars := evd';
+      z
+
+  let evd_comb3 f isevars x y z =
+    let (evd',t) = f !isevars x y z in
+      isevars := evd';
+      t
+	
+  let mt_evd = Evd.empty
+    
+  let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)
+      
+  (* Utilisé pour inférer le prédicat des Cases *)
+  (* Semble exagérement fort *)
+  (* Faudra préférer une unification entre les types de toutes les clauses *)
+  (* et autoriser des ? à rester dans le résultat de l'unification *)
+  
+  let evar_type_fixpoint loc env isevars lna lar vdefj =
+    let lt = Array.length vdefj in 
+      if Array.length lar = lt then 
+	for i = 0 to lt-1 do 
+          if not (e_cumul env isevars (vdefj.(i)).uj_type
+		    (lift lt lar.(i))) then
+            error_ill_typed_rec_body_loc loc env (evars_of !isevars)
+              i lna vdefj lar
+	done
+
+  let check_branches_message loc env isevars c (explft,lft) = 
+    for i = 0 to Array.length explft - 1 do
+      if not (e_cumul env isevars lft.(i) explft.(i)) then 
+	let sigma = evars_of !isevars in
+	  error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i)
+    done
+
+  (* coerce to tycon if any *)
+  let inh_conv_coerce_to_tycon loc env isevars j = function
+    | None -> j
+    | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) isevars j t
+
+  let push_rels vars env = List.fold_right push_rel vars env
+
+  (*
+    let evar_type_case isevars env ct pt lft p c =
+    let (mind,bty,rslty) = type_case_branches env (evars_of isevars) ct pt p c
+    in check_branches_message isevars env (c,ct) (bty,lft); (mind,rslty)
+  *)
+
+  let strip_meta id = (* For Grammar v7 compatibility *)
+    let s = string_of_id id in
+      if s.[0]='$' then id_of_string (String.sub s 1 (String.length s - 1))
+      else id
+
+  let pretype_id loc env (lvar,unbndltacvars) id =
+    let id = strip_meta id in (* May happen in tactics defined by Grammar *)
+      try
+	let (n,typ) = lookup_rel_id id (rel_context env) in
+	  { uj_val  = mkRel n; uj_type = type_app (lift n) typ }
+      with Not_found ->
+	try
+	  List.assoc id lvar
+	with Not_found ->
+	  try
+	    let (_,_,typ) = lookup_named id env in
+	      { uj_val  = mkVar id; uj_type = typ }
+	  with Not_found ->
+	    try (* To build a nicer ltac error message *)
+	      match List.assoc id unbndltacvars with
+		| None -> user_err_loc (loc,"",
+					str "variable " ++ pr_id id ++ str " should be bound to a term")
+		| Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
+	    with Not_found ->
+	      error_var_not_found_loc loc id
+
+  (* make a dependent predicate from an undependent one *)
+
+  let make_dep_of_undep env (IndType (indf,realargs)) pj =
+    let n = List.length realargs in
+    let rec decomp n p =
+      if n=0 then p else
+	match kind_of_term p with
+	  | Lambda (_,_,c) -> decomp (n-1) c
+	  | _ -> decomp (n-1) (applist (lift 1 p, [mkRel 1])) 
+    in
+    let sign,s = decompose_prod_n n pj.uj_type in
+    let ind = build_dependent_inductive env indf in
+    let s' = mkProd (Anonymous, ind, s) in
+    let ccl = lift 1 (decomp n pj.uj_val) in
+    let ccl' = mkLambda (Anonymous, ind, ccl) in
+      {uj_val=lam_it ccl' sign; uj_type=prod_it s' sign} 
+
+  (*************************************************************************)
+  (* Main pretyping function                                               *)
+
+  let pretype_ref isevars env ref = 
+    let c = constr_of_global ref in
+      make_judge c (Retyping.get_type_of env Evd.empty c)
+
+  let pretype_sort = function
+    | RProp c -> judge_of_prop_contents c
+    | RType _ -> judge_of_new_Type ()
+
+  (* [pretype tycon env isevars lvar lmeta cstr] attempts to type [cstr] *)
+  (* in environment [env], with existential variables [(evars_of isevars)] and *)
+  (* the type constraint tycon *)
+  let rec pretype (tycon : type_constraint) env isevars lvar = function
+    | RRef (loc,ref) ->
+	inh_conv_coerce_to_tycon loc env isevars
+	  (pretype_ref isevars env ref)
+	  tycon
+
+    | RVar (loc, id) ->
+	inh_conv_coerce_to_tycon loc env isevars
+	  (pretype_id loc env lvar id)
+	  tycon
+
+    | REvar (loc, ev, instopt) ->
+	(* Ne faudrait-il pas s'assurer que hyps est bien un
+	   sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
+	let hyps = evar_context (Evd.find (evars_of !isevars) ev) in
+	let args = match instopt with
+          | None -> instance_from_named_context hyps
+          | Some inst -> failwith "Evar subtitutions not implemented" in
+	let c = mkEvar (ev, args) in
+	let j = (Retyping.get_judgment_of env (evars_of !isevars) c) in
+	  inh_conv_coerce_to_tycon loc env isevars j tycon
+
+    | RPatVar (loc,(someta,n)) -> 
+	anomaly "Found a pattern variable in a rawterm to type"
+	  
+    | RHole (loc,k) ->
+	let ty =
+          match tycon with 
+            | Some (None, ty) -> ty
+            | None | Some _ ->
+		e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ()) in
+	  { uj_val = e_new_evar isevars env ~src:(loc,k) ty; uj_type = ty }
+
+    | RRec (loc,fixkind,names,bl,lar,vdef) ->
+	let rec type_bl env ctxt = function
+            [] -> ctxt
+          | (na,None,ty)::bl ->
+              let ty' = pretype_type empty_valcon env isevars lvar ty in
+              let dcl = (na,None,ty'.utj_val) in
+		type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl
+          | (na,Some bd,ty)::bl ->
+              let ty' = pretype_type empty_valcon env isevars lvar ty in
+              let bd' = pretype (mk_tycon ty'.utj_val) env isevars lvar ty in
+              let dcl = (na,Some bd'.uj_val,ty'.utj_val) in
+		type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl in
+	let ctxtv = Array.map (type_bl env empty_rel_context) bl in
+	let larj =
+          array_map2
+            (fun e ar ->
+               pretype_type empty_valcon (push_rel_context e env) isevars lvar ar)
+            ctxtv lar in
+	let lara = Array.map (fun a -> a.utj_val) larj in
+	let ftys = array_map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in
+	let nbfix = Array.length lar in
+	let names = Array.map (fun id -> Name id) names in
+	  (* Note: bodies are not used by push_rec_types, so [||] is safe *)
+	let newenv = push_rec_types (names,ftys,[||]) env in
+	let vdefj =
+	  array_map2_i 
+	    (fun i ctxt def ->
+               (* we lift nbfix times the type in tycon, because of
+		* the nbfix variables pushed to newenv *)
+               let (ctxt,ty) =
+		 decompose_prod_n_assum (rel_context_length ctxt)
+                   (lift nbfix ftys.(i)) in
+               let nenv = push_rel_context ctxt newenv in
+               let j = pretype (mk_tycon ty) nenv isevars lvar def in
+		 { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
+		   uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
+            ctxtv vdef in
+	evar_type_fixpoint loc env isevars names ftys vdefj;
+	let fixj = match fixkind with
+	  | RFix (vn,i) ->
+	      let guard_indexes = Array.mapi 
+		(fun i (n,_) -> match n with 
+		   | Some n -> n 
+		   | None -> 
+		       (* Recursive argument was not given by the user : We
+			  check that there is only one inductive argument *)
+		       let ctx = ctxtv.(i) in 
+		       let isIndApp t = 
+			 isInd (fst (decompose_app (strip_head_cast t))) in
+			 (* This could be more precise (e.g. do some delta) *)
+		       let lb = List.rev_map (fun (_,_,t) -> isIndApp t) ctx in
+		       try (list_unique_index true lb) - 1
+		       with Not_found -> 
+			 Util.user_err_loc
+			   (loc,"pretype",
+			    Pp.str "cannot guess decreasing argument of fix"))
+		vn 
+	      in
+	      let fix = ((guard_indexes, i),(names,ftys,Array.map j_val vdefj)) in
+	      (try check_fix env fix with e -> Stdpp.raise_with_loc loc e);
+	      make_judge (mkFix fix) ftys.(i)
+	  | RCoFix i -> 
+	      let cofix = (i,(names,ftys,Array.map j_val vdefj)) in
+	      (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
+	      make_judge (mkCoFix cofix) ftys.(i) in
+	inh_conv_coerce_to_tycon loc env isevars fixj tycon
+
+    | RSort (loc,s) ->
+	inh_conv_coerce_to_tycon loc env isevars (pretype_sort s) tycon
+
+    | RApp (loc,f,args) -> 
+	let length = List.length args in	 
+	let ftycon = 
+	  match tycon with
+	      None -> None
+	    | Some (None, ty) -> mk_abstr_tycon length ty
+	    | Some (Some (init, cur), ty) ->
+		Some (Some (length + init, length + cur), ty)
+	in
+	let fj = pretype ftycon env isevars lvar f in
+ 	let floc = loc_of_rawconstr f in
+	let rec apply_rec env n resj tycon = function
+	  | [] -> resj
+	  | c::rest ->
+	      let argloc = loc_of_rawconstr c in
+	      let resj = evd_comb1 (Coercion.inh_app_fun env) isevars resj in
+              let resty = whd_betadeltaiota env (evars_of !isevars) resj.uj_type in
+      		match kind_of_term resty with
+		  | Prod (na,c1,c2) ->
+		      let hj = pretype (mk_tycon c1) env isevars lvar c in
+		      let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
+		      let typ' = nf_isevar !isevars typ in
+		      let tycon = 
+			option_map 
+			  (fun (abs, ty) ->
+			     match abs with
+				 None ->
+				   isevars := Coercion.inh_conv_coerces_to loc env !isevars typ'
+				     (abs, ty);
+				   (abs, ty)
+			       | Some (init, cur) ->
+				   isevars := Coercion.inh_conv_coerces_to loc env !isevars typ' 
+				     (abs, ty);
+				   (Some (init, pred cur), ty))
+			  tycon
+		      in 
+			apply_rec env (n+1) 
+			  { uj_val = nf_isevar !isevars value;
+			    uj_type = nf_isevar !isevars typ' }
+			  (option_map (fun (abs, c) -> abs, nf_isevar !isevars c) tycon) rest
+
+		  | _ ->
+		      let hj = pretype empty_tycon env isevars lvar c in
+			error_cant_apply_not_functional_loc 
+			  (join_loc floc argloc) env (evars_of !isevars)
+	      		  resj [hj]
+	in
+	let ftycon = option_map (lift_abstr_tycon_type (-1)) ftycon in
+	let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj ftycon args) in
+	let resj =
+	  match kind_of_term resj.uj_val with
+	  | App (f,args) when isInd f ->
+	      let sigma = evars_of !isevars in
+	      let t = Retyping.type_of_inductive_knowing_parameters env sigma (destInd f) args in
+	      let s = snd (splay_arity env sigma t) in
+	      on_judgment_type (set_inductive_level env s) resj
+		(* Rem: no need to send sigma: no head evar, it's an arity *)
+	  | _ -> resj in
+	inh_conv_coerce_to_tycon loc env isevars resj tycon
+
+    | RLambda(loc,name,c1,c2)      ->
+	let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon in
+	let dom_valcon = valcon_of_tycon dom in
+	let j = pretype_type dom_valcon env isevars lvar c1 in
+	let var = (name,None,j.utj_val) in
+	let j' = pretype rng (push_rel var env) isevars lvar c2 in 
+	  judge_of_abstraction env name j j'
+
+    | RProd(loc,name,c1,c2)        ->
+	let j = pretype_type empty_valcon env isevars lvar c1 in
+	let var = (name,j.utj_val) in
+	let env' = push_rel_assum var env in
+	let j' = pretype_type empty_valcon env' isevars lvar c2 in
+	let resj =
+	  try judge_of_product env name j j'
+	  with TypeError _ as e -> Stdpp.raise_with_loc loc e in
+	  inh_conv_coerce_to_tycon loc env isevars resj tycon
+	    
+    | RLetIn(loc,name,c1,c2)      ->
+	let j = pretype empty_tycon env isevars lvar c1 in
+	let t = refresh_universes j.uj_type in
+	let var = (name,Some j.uj_val,t) in
+        let tycon = lift_tycon 1 tycon in
+	let j' = pretype tycon (push_rel var env) isevars lvar c2 in
+	  { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
+	    uj_type = subst1 j.uj_val j'.uj_type }
+
+    | RLetTuple (loc,nal,(na,po),c,d) ->
+	let cj = pretype empty_tycon env isevars lvar c in
+	let (IndType (indf,realargs)) = 
+	  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
+	let cstrs = get_constructors env indf in
+	  if Array.length cstrs <> 1 then
+            user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor");
+	  let cs = cstrs.(0) in
+	    if List.length nal <> cs.cs_nargs then
+              user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables");
+	    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 =
+	      let arsgn,_ = get_arity env indf in
+		if not !allow_anonymous_refs then
+		  List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn
+		else arsgn
+	    in
+	    let psign = (na,None,build_dependent_inductive env indf)::arsgn in
+	    let nar = List.length arsgn in
+	      (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
+		     let psign = make_arity_signature env true indf in (* with names *)
+		     let p = it_mkLambda_or_LetIn ccl psign in
+		     let inst = 
+		       (Array.to_list cs.cs_concl_realargs)
+		       @[build_dependent_constructor cs] in
+		     let lp = lift cs.cs_nargs p in
+		     let fty = hnf_lam_applist env (evars_of !isevars) lp inst in
+		     let fj = pretype (mk_tycon fty) env_f isevars lvar d in
+		     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
+		     let v =
+		       let mis,_ = dest_ind_family indf in
+		       let ci = make_default_case_info env LetStyle mis in
+			 mkCase (ci, p, cj.uj_val,[|f|]) in 
+		       { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
+
+		 | None -> 
+		     let tycon = lift_tycon cs.cs_nargs tycon in
+		     let fj = pretype tycon env_f isevars lvar d in
+		     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
+		     let ccl = nf_evar (evars_of !isevars) fj.uj_type in
+		     let ccl =
+		       if noccur_between 1 cs.cs_nargs ccl then
+			 lift (- cs.cs_nargs) ccl 
+		       else
+			 error_cant_find_case_type_loc loc env (evars_of !isevars) 
+			   cj.uj_val in
+		     let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
+		     let v =
+		       let mis,_ = dest_ind_family indf in
+		       let ci = make_default_case_info env LetStyle mis in
+			 mkCase (ci, p, cj.uj_val,[|f|] ) 
+		     in
+		       { uj_val = v; uj_type = ccl })
+
+    | RIf (loc,c,(na,po),b1,b2) ->
+	let cj = pretype empty_tycon env isevars lvar c in
+	let (IndType (indf,realargs)) = 
+	  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
+	let cstrs = get_constructors env indf in 
+	  if Array.length cstrs <> 2 then
+            user_err_loc (loc,"",
+			  str "If is only for inductive types with two constructors");
+
+	  let arsgn = 
+	    let arsgn,_ = get_arity env indf in
+	      if not !allow_anonymous_refs then
+		(* Make dependencies from arity signature impossible *)
+		List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn 
+	      else arsgn
+	  in
+	  let nar = List.length arsgn in
+	  let psign = (na,None,build_dependent_inductive env indf)::arsgn in
+	  let pred,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
+		let pred = it_mkLambda_or_LetIn ccl psign in
+		let typ = lift (- nar) (beta_applist (pred,[cj.uj_val])) in
+		let jtyp = inh_conv_coerce_to_tycon loc env isevars {uj_val = pred;
+								     uj_type = typ} tycon 
+		in
+		  jtyp.uj_val, jtyp.uj_type
+	    | None -> 
+		let p = match tycon with
+		  | Some (None, ty) -> ty
+		  | None | Some _ ->
+                      e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ())
+		in
+		  it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
+	  let pred = nf_evar (evars_of !isevars) pred in
+	  let p = nf_evar (evars_of !isevars) p in
+	 (*   msgnl (str "Pred is: " ++ Termops.print_constr_env env pred);*)
+	  let f cs b =
+	    let n = rel_context_length cs.cs_args in
+	    let pi = lift n pred in (* liftn n 2 pred ? *)
+	    let pi = beta_applist (pi, [build_dependent_constructor cs]) in
+	    let csgn = 
+	      if not !allow_anonymous_refs then
+		List.map (fun (_,b,t) -> (Anonymous,b,t)) cs.cs_args 
+	      else 
+		List.map 
+		  (fun (n, b, t) ->
+		     match n with
+                         Name _ -> (n, b, t)
+                       | Anonymous -> (Name (id_of_string "H"), b, t))
+		cs.cs_args
+	    in
+	    let env_c = push_rels csgn env in 
+(* 	      msgnl (str "Pi is: " ++ Termops.print_constr_env env_c pi); *)
+	    let bj = pretype (mk_tycon pi) env_c isevars lvar b in
+	      it_mkLambda_or_LetIn bj.uj_val cs.cs_args in
+	  let b1 = f cstrs.(0) b1 in
+	  let b2 = f cstrs.(1) b2 in
+	  let v =
+	    let mis,_ = dest_ind_family indf in
+	    let ci = make_default_case_info env IfStyle mis in
+	      mkCase (ci, pred, cj.uj_val, [|b1;b2|])
+	  in
+	    { uj_val = v; uj_type = p }
+
+    | RCases (loc,po,tml,eqns) ->
+	Cases.compile_cases loc
+	  ((fun vtyc env -> pretype vtyc env isevars lvar),isevars)
+	  tycon env (* loc *) (po,tml,eqns)
+
+    | RCast(loc,c,k,t) ->
+	let cj =
+	  match k with
+	      CastCoerce ->
+		let cj = pretype empty_tycon env isevars lvar c in
+		  evd_comb1 (Coercion.inh_coerce_to_base loc env) isevars cj
+	    | CastConv k ->
+		let tj = pretype_type empty_valcon env isevars lvar t in
+		let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in
+		  (* User Casts are for helping pretyping, experimentally not to be kept*)
+		  (* ... except for Correctness *)
+		let v = mkCast (cj.uj_val, k, tj.utj_val) in
+		  { uj_val = v; uj_type = tj.utj_val }
+	in
+	  inh_conv_coerce_to_tycon loc env isevars cj tycon
+
+    | RDynamic (loc,d) ->
+	if (tag d) = "constr" then
+	  let c = constr_out d in
+	  let j = (Retyping.get_judgment_of env (evars_of !isevars) c) in
+	    j
+	      (*inh_conv_coerce_to_tycon loc env isevars j tycon*)
+	else
+	  user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic"))
+
+  (* [pretype_type valcon env isevars lvar c] coerces [c] into a type *)
+  and pretype_type valcon env isevars lvar = function
+    | RHole loc ->
+	(match valcon with
+	   | Some v ->
+               let s =
+		 let sigma = evars_of !isevars in
+		 let t = Retyping.get_type_of env sigma v in
+		   match kind_of_term (whd_betadeltaiota env sigma t) with
+                     | Sort s -> s
+                     | Evar v when is_Type (existential_type sigma v) -> 
+			 evd_comb1 (define_evar_as_sort) isevars v
+                     | _ -> anomaly "Found a type constraint which is not a type"
+               in
+		 { utj_val = v;
+		   utj_type = s }
+	   | None ->
+	       let s = new_Type_sort () in
+		 { utj_val = e_new_evar isevars env ~src:loc (mkSort s);
+		   utj_type = s})
+    | c ->
+	let j = pretype empty_tycon env isevars lvar c in
+	let loc = loc_of_rawconstr c in
+	let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) isevars j in
+	  match valcon with
+	    | None -> tj
+	    | Some v ->
+		if e_cumul env isevars v tj.utj_val then tj
+		else
+		  error_unexpected_type_loc
+                    (loc_of_rawconstr c) env (evars_of !isevars) tj.utj_val v
+
+  let pretype_gen isevars env lvar kind c =
+    let c' = match kind with
+      | OfType exptyp ->
+	  let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
+	    (pretype tycon env isevars lvar c).uj_val
+      | IsType ->
+	  (pretype_type empty_valcon env isevars lvar c).utj_val in
+      nf_evar (evars_of !isevars) c'
+
+  (* [check_evars] fails if some unresolved evar remains *)
+  (* it assumes that the defined existentials have already been substituted
+     (should be done in unsafe_infer and unsafe_infer_type) *)
+
+  let check_evars env initial_sigma isevars c =
+    let sigma = evars_of !isevars in
+    let rec proc_rec c =
+      match kind_of_term c with
+	| Evar (ev,args) ->
+            assert (Evd.mem sigma ev);
+	    if not (Evd.mem initial_sigma ev) then
+              let (loc,k) = evar_source ev !isevars in
+		error_unsolvable_implicit loc env sigma k
+	| _ -> iter_constr proc_rec c
+    in
+      proc_rec c(*;
+		  let (_,pbs) = get_conv_pbs !isevars (fun _ -> true) in
+		  if pbs <> [] then begin
+		  pperrnl
+		  (str"TYPING OF "++Termops.print_constr_env env c++fnl()++
+		  prlist_with_sep fnl
+		  (fun  (pb,c1,c2) ->
+		  Termops.print_constr c1 ++
+		  (if pb=Reduction.CUMUL then str " <="++ spc()
+		  else str" =="++spc()) ++
+		  Termops.print_constr c2)
+		  pbs ++ fnl())
+		  end*)
+
+  (* TODO: comment faire remonter l'information si le typage a resolu des
+     variables du sigma original. il faudrait que la fonction de typage
+     retourne aussi le nouveau sigma...
+  *)
+
+  let understand_judgment sigma env c =
+    let isevars = ref (create_evar_defs sigma) in
+    let j = pretype empty_tycon env isevars ([],[]) c in
+    let j = j_nf_evar (evars_of !isevars) j in
+      check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
+      j
+
+  let understand_judgment_tcc isevars env c =
+    let j = pretype empty_tycon env isevars ([],[]) c in
+    let sigma = evars_of !isevars in
+    let j = j_nf_evar sigma j in
+      j
+
+  (* Raw calls to the unsafe inference machine: boolean says if we must
+     fail on unresolved evars; the unsafe_judgment list allows us to
+     extend env with some bindings *)
+
+  let ise_pretype_gen fail_evar sigma env lvar kind c =
+    let isevars = ref (Evd.create_evar_defs sigma) in
+    let c = pretype_gen isevars env lvar kind c in
+      if fail_evar then check_evars env sigma isevars c;
+      !isevars, c
+
+  (** Entry points of the high-level type synthesis algorithm *)
+
+  let understand_gen kind sigma env c =
+    snd (ise_pretype_gen true sigma env ([],[]) kind c)
+
+  let understand sigma env ?expected_type:exptyp c =
+    snd (ise_pretype_gen true sigma env ([],[]) (OfType exptyp) c)
+
+  let understand_type sigma env c =
+    snd (ise_pretype_gen true sigma env ([],[]) IsType c)
+
+  let understand_ltac sigma env lvar kind c =
+    ise_pretype_gen false sigma env lvar kind c
+      
+  let understand_tcc_evars isevars env kind c =
+    pretype_gen isevars env ([],[]) kind c
+
+  let understand_tcc sigma env ?expected_type:exptyp c =
+    let ev, t = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in
+      Evd.evars_of ev, t
+end
+
+module Default : S = SubtacPretyping_F(Coercion.Default)
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 6c165dada..966aa80a9 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -57,7 +57,7 @@ let natind = lazy (init_constant ["Init"; "Datatypes"] "nat")
 let intind = lazy (init_constant ["ZArith"; "binint"] "Z")
 let existSind = lazy (init_constant ["Init"; "Specif"] "sigS")
   
-let existS = lazy (build_sigma_set ())
+let existS = lazy (build_sigma_type ())
 
 let prod = lazy (build_prod ())
 
@@ -244,3 +244,79 @@ let destruct_ex ext ex =
   in aux ex ext
 
 
+let list_mapi f = 
+  let rec aux i = function 
+      hd :: tl -> f i hd :: aux (succ i) tl 
+    | [] -> []
+  in aux 0
+
+open Rawterm
+
+let rewrite_cases_aux (loc, po, tml, eqns) =
+  let tml' = list_mapi (fun i (c, (n, opt)) -> c, 
+		       ((match n with
+			    Name id -> (match c with
+					  | RVar (_, id') when id = id' ->
+					      id, (id_of_string (string_of_id id ^ "Heq_id"))
+					  | RVar (_, id') ->
+					      id', id
+					  | _ -> id_of_string (string_of_id id ^ "Heq_id"), id)
+			   | Anonymous -> 
+			       let str = "Heq_id" ^ string_of_int i in
+				 id_of_string str, id_of_string (str ^ "'")),
+			opt)) tml 
+  in
+  let mkHole = RHole (dummy_loc, InternalHole) in
+  let mkCoerceCast c = RCast (dummy_loc, c, CastCoerce, mkHole) in
+  let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eqind_ref)),
+		       [mkHole; c; n])
+  in
+  let eqs_types = 
+    List.map
+      (fun (c, ((id, id'), _)) ->
+	 let heqid = id_of_string ("Heq" ^ string_of_id id) in
+	   Name heqid, mkeq (RVar (dummy_loc, id')) c)
+      tml'
+  in
+  let po = 
+    List.fold_right
+      (fun (n,t) acc ->
+	 RProd (dummy_loc, Anonymous, t, acc))
+      eqs_types (match po with 
+		     Some e -> e
+		   | None -> mkHole)
+  in
+  let eqns =   
+    List.map (fun (loc, idl, cpl, c) ->
+		let c' = 
+		  List.fold_left 
+		    (fun acc (n, t) ->
+		       RLambda (dummy_loc, n, mkHole, acc))
+		    c eqs_types
+		in (loc, idl, cpl, c'))
+      eqns
+  in
+  let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force refl_equal_ref),
+			      [mkHole; c])
+  in
+  let refls = List.map (fun (c, ((id, _), _)) -> mk_refl_equal (mkCoerceCast c)) tml' in
+  let tml'' = List.map (fun (c, ((id, id'), opt)) -> c, (Name id', opt)) tml' in
+  let case = RCases (loc,Some po,tml'',eqns) in
+  let app = RApp (dummy_loc, case, refls) in
+(*   let letapp = List.fold_left (fun acc (c, ((id, id'), opt)) -> RLetIn (dummy_loc, Name id, c, acc)) *)
+(* 		 app tml' *)
+(*   in *)
+    app
+
+let rec rewrite_cases c = 
+  match c with 
+      RCases _ -> let c' = map_rawconstr rewrite_cases c in
+	(match c' with 
+	   | RCases (x, y, z, w) -> rewrite_cases_aux (x,y,z,w)
+	   | _ -> assert(false))
+    | _ -> map_rawconstr rewrite_cases c
+	  
+let rewrite_cases env c =
+  let c' = rewrite_cases c in
+  let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in
+    c'
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 92a995c89..5ef3af18e 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -83,3 +83,5 @@ val and_tac : (identifier * 'a * constr * Proof_type.tactic) list ->
   ((constr -> (identifier * 'a * constr * constr) list) -> Tacexpr.declaration_hook) -> unit
 
 val destruct_ex : constr -> constr -> constr list
+
+val rewrite_cases : Environ.env -> Rawterm.rawconstr -> Rawterm.rawconstr
diff --git a/contrib/subtac/test/ListsTest.v b/contrib/subtac/test/ListsTest.v
index e5f42defb..a29cd0396 100644
--- a/contrib/subtac/test/ListsTest.v
+++ b/contrib/subtac/test/ListsTest.v
@@ -1,38 +1,28 @@
 Require Import Coq.subtac.Utils.
 Require Import List.
-Require Import Arith.
+
 Variable A : Set.
 
-Notation "` t" := (proj1_sig t) (at level 100) : core_scope.
-Extraction Inline proj1_sig.
-Notation "'forall' { x : A | P } , Q" :=
-  (forall x:{x:A|P}, Q)
-  (at level 200, x ident, right associativity).
-Require Import Omega.
-Program Definition myhd : 
-  forall { l : list A | length l <> 0 }, A :=
-  
+Program Definition myhd : forall { l : list A | length l <> 0 }, A :=  
   fun l =>
     match l with
     | nil => _
     | hd :: tl => hd
     end.
-
 Proof.
   destruct l ; simpl ; intro H ; rewrite <- H in n ; intuition.
 Defined.
 
-Extraction myhd.
 
-Program Definition mytail : 
-  forall { l : list A | length l <> 0 }, list A :=
+Extraction myhd.
+Extraction Inline proj1_sig.
 
+Program Definition mytail : forall { l : list A | length l <> 0 }, list A :=
   fun l => 
-    match `l with
+    match l with
     | nil => _
     | hd :: tl => tl
     end.
-
 Proof.
 destruct l ; simpl ; intro H ; rewrite <- H in n ; intuition.
 Defined.
@@ -48,35 +38,39 @@ Defined.
 
 Extraction test_hd.
 
-Program Definition test_tail : list A := mytail nil.
+(*Program Definition test_tail : list A := mytail nil.*)
+
+
+
+
 
 Program Fixpoint append (l : list A) (l' : list A) { struct l } :
  { r : list A | length r = length l + length l' } :=
  match l with
- nil => l'
+ | nil => l'
  | hd :: tl => hd :: (append tl l')
  end.
-rewrite Heql ; auto.
 simpl.
-rewrite (subset_simpl (append tl0 l')).
-unfold tl0 ; unfold hd0.
-rewrite Heql.
+subst ; auto.
+simpl ; rewrite (subset_simpl (append tl0 l')).
+simpl ; subst.
 simpl ; auto.
 Defined.
 
 Extraction append.
 
-Lemma append_app' : forall l : list A, (`append nil l) = l.
+
+Program Lemma append_app' : forall l : list A, l = append nil l.
 Proof.
 simpl ; auto.
 Qed.
 
-Lemma append_app : forall l : list A, (`append l nil) = l.
+Program Lemma append_app : forall l : list A, l = append l nil.
 Proof.
 intros.
 induction l ; simpl ; auto.
 simpl in IHl.
-rewrite IHl.
+rewrite <- IHl.
 reflexivity.
 Qed.
 
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 7a634a71a..5b9b40442 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -45,7 +45,7 @@ type aconstr =
   | ASort of rawsort
   | AHole of Evd.hole_kind
   | APatVar of patvar
-  | ACast of aconstr * cast_kind * aconstr
+  | ACast of aconstr * cast_type * aconstr
   
 let name_app f e = function
   | Name id -> let (id, e) = f id e in (e, Name id)
@@ -94,7 +94,7 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
   | AIf (c,(na,po),b1,b2) ->
       let e,na = name_app g e na in
       RIf (loc,f e c,(na,option_map (f e) po),f e b1,f e b2)
-  | ACast (c,k,t) -> RCast (loc,f e c,k,f e t)
+  | ACast (c,k,t) -> RCast (loc,f e c, k,f e t)
   | ASort x -> RSort (loc,x)
   | AHole x  -> RHole (loc,x)
   | APatVar n -> RPatVar (loc,(false,n))
@@ -524,7 +524,7 @@ type constr_expr =
   | CPatVar of loc * (bool * patvar)
   | CEvar of loc * existential_key
   | CSort of loc * rawsort
-  | CCast of loc * constr_expr * cast_kind * constr_expr
+  | CCast of loc * constr_expr * cast_type * constr_expr
   | CNotation of loc * notation * constr_expr list
   | CPrim of loc * prim_token
   | CDelimiters of loc * string * constr_expr
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index d5b718d34..9173d3116 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -41,7 +41,7 @@ type aconstr =
   | ASort of rawsort
   | AHole of Evd.hole_kind
   | APatVar of patvar
-  | ACast of aconstr * cast_kind * aconstr
+  | ACast of aconstr * cast_type * aconstr
 
 val rawconstr_of_aconstr_with_binders : loc -> 
   (identifier -> 'a -> identifier * 'a) ->
@@ -107,7 +107,7 @@ type constr_expr =
   | CPatVar of loc * (bool * patvar)
   | CEvar of loc * existential_key
   | CSort of loc * rawsort
-  | CCast of loc * constr_expr * cast_kind * constr_expr
+  | CCast of loc * constr_expr * cast_type * constr_expr
   | CNotation of loc * notation * constr_expr list
   | CPrim of loc * prim_token
   | CDelimiters of loc * string * constr_expr
@@ -143,7 +143,7 @@ val names_of_cases_indtype : constr_expr -> identifier list
 val mkIdentC : identifier -> constr_expr
 val mkRefC : reference -> constr_expr
 val mkAppC : constr_expr * constr_expr list -> constr_expr
-val mkCastC : constr_expr * cast_kind * constr_expr -> constr_expr
+val mkCastC : constr_expr * cast_type * constr_expr -> constr_expr
 val mkLambdaC : name located list * constr_expr * constr_expr -> constr_expr
 val mkLetInC : name located * constr_expr * constr_expr -> constr_expr
 val mkProdC : name located list * constr_expr * constr_expr -> constr_expr
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 64d96ae4b..82e111425 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -28,7 +28,7 @@ let _ = List.iter (fun s -> Lexer.add_token("",s)) constr_kw
 
 let mk_cast = function
     (c,(_,None)) -> c
-  | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, DEFAULTcast,ty)
+  | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv DEFAULTcast, ty)
 
 let mk_lam = function
     ([],c) -> c
@@ -155,8 +155,8 @@ GEXTEND Gram
     [ "200" RIGHTA
       [ c = binder_constr -> c ]
     | "100" RIGHTA
-      [ c1 = operconstr; ":"; c2 = binder_constr -> CCast(loc,c1,DEFAULTcast,c2)
-      | c1 = operconstr; ":"; c2 = SELF -> CCast(loc,c1,DEFAULTcast,c2) ]
+      [ c1 = operconstr; ":"; c2 = binder_constr -> CCast(loc,c1, CastConv DEFAULTcast,c2)
+      | c1 = operconstr; ":"; c2 = SELF -> CCast(loc,c1,CastConv DEFAULTcast,c2) ]
     | "99" RIGHTA [ ]
     | "90" RIGHTA
       [ c1 = operconstr; "->"; c2 = binder_constr -> CArrow(loc,c1,c2)
@@ -320,7 +320,7 @@ GEXTEND Gram
       | "("; id=name; ":="; c=lconstr; ")" ->
           LocalRawDef (id,c)
       | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> 
-          LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c,DEFAULTcast,t))
+          LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv DEFAULTcast,t))
     ] ]
   ;
   binder:
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 5d392846d..a1a703099 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -117,6 +117,6 @@ GEXTEND Gram
     ;
   constr_body:
     [ [ ":="; c = lconstr -> c
-      | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c,Term.DEFAULTcast,t) ] ]
+      | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c, Rawterm.CastConv Term.DEFAULTcast,t) ] ]
   ;
 END
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 56be1ff5a..bdedaf176 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -181,7 +181,7 @@ let rec interp_xml_constr = function
       let ln,lc,lt = list_split3 (List.map interp_xml_CoFixFunction xl) in
       RRec (loc, RCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt)
   | XmlTag (loc,"CAST",al,[x1;x2]) ->
-      RCast (loc, interp_xml_term x1, DEFAULTcast, interp_xml_type x2)
+      RCast (loc, interp_xml_term x1, CastConv DEFAULTcast, interp_xml_type x2)
   | XmlTag (loc,"SORT",al,[]) ->
       RSort (loc, get_xml_sort al)
   | XmlTag (loc,s,_,_) -> user_err_loc (loc,"", str "Unexpected tag " ++ str s)
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 7a77d6eab..b3cff232b 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1482,7 +1482,7 @@ let set_arity_signature dep n arsign tomatchl pred x =
   in
   decomp_block [] pred (tomatchl,arsign)
 
-let prepare_predicate_from_tycon loc dep env isevars tomatchs c =
+let prepare_predicate_from_tycon loc dep env isevars tomatchs sign c =
   let cook (n, l, env, signs) = function
     | c,IsInd (_,IndType(indf,realargs)) ->
 	let indf' = lift_inductive_family n indf in
@@ -1594,7 +1594,7 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
       (match tycon with
        | Some (None, t) ->
 	   let names,pred = 
-	     prepare_predicate_from_tycon loc false env isevars tomatchs t 
+	     prepare_predicate_from_tycon loc false env isevars tomatchs sign t 
 	   in Some (build_initial_predicate false names pred)
        | _ -> None)
 
@@ -1607,7 +1607,8 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
       let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in
       let _ = 
 	option_map (fun tycon -> 
-		      isevars := Coercion.inh_conv_coerces_to loc env !isevars predcclj.uj_val tycon)
+		      isevars := Coercion.inh_conv_coerces_to loc env !isevars predcclj.uj_val 
+		      (lift_tycon_type (List.length arsign) tycon))
 	  tycon
       in
       let predccl = (j_nf_isevar !isevars predcclj).uj_val in      
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 1b128e43a..8a55a46d2 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -35,6 +35,12 @@ module type S = sig
      type a sort; it fails if no coercion is applicable *)
   val inh_coerce_to_sort : loc ->
     env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_type_judgment
+
+  (* [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it
+     inserts a coercion into [j], if needed, in such a way it gets as
+     type its base type (the notion depends on the coercion system) *)
+  val inh_coerce_to_base : loc ->
+    env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment
     
   (* [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type 
      [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
@@ -143,6 +149,8 @@ module Default = struct
 	| _ ->
 	    inh_tosort_force loc env isevars j
 
+  let inh_coerce_to_base loc env isevars j = (isevars, j)
+
   let inh_coerce_to_fail env isevars c1 v t =
     let v', t' =
       try 
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 667f20730..5476a4820 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -33,13 +33,19 @@ module type S = sig
      type a sort; it fails if no coercion is applicable *)
   val inh_coerce_to_sort : loc ->
     env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_type_judgment
+
+  (* [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it
+     inserts a coercion into [j], if needed, in such a way it gets as
+     type its base type (the notion depends on the coercion system) *)
+  val inh_coerce_to_base : loc ->
+    env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment
     
   (* [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type 
      [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
      [j.uj_type] are convertible; it fails if no coercion is applicable *)
   val inh_conv_coerce_to : loc -> 
     env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment
-
+    
   (* [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
      is coercible to an object of type [t'] adding evar constraints if needed;
      it fails if no coercion exists *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index ec6edcbdf..1fcc6d8b7 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -374,7 +374,7 @@ let rec detype isgoal avoid env t =
 	  RVar (dl, id))
     | Sort s -> RSort (dl,detype_sort s)
     | Cast (c1,k,c2) ->
-	RCast(dl,detype isgoal avoid env c1, k,
+	RCast(dl,detype isgoal avoid env c1, CastConv k,
               detype isgoal avoid env c2)
     | Prod (na,ty,c) -> detype_binder isgoal BProd avoid env na ty c
     | Lambda (na,ty,c) -> detype_binder isgoal BLambda avoid env na ty c
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index d1d30980b..be24d22b5 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -363,17 +363,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	inh_conv_coerce_to_tycon loc env isevars (pretype_sort s) tycon
 
     | RApp (loc,f,args) -> 
-	let length = List.length args in	 
-	let ftycon = 
-	  match tycon with
-	      None -> None
-	    | Some (None, ty) -> mk_abstr_tycon length ty
-	    | Some (Some (init, cur), ty) ->
-		Some (Some (length + init, length + cur), ty)
-	in
 	let fj = pretype empty_tycon env isevars lvar f in
  	let floc = loc_of_rawconstr f in
-	let rec apply_rec env n resj tycon = function
+	let rec apply_rec env n resj = function
 	  | [] -> resj
 	  | c::rest ->
 	      let argloc = loc_of_rawconstr c in
@@ -384,33 +376,17 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		      let hj = pretype (mk_tycon c1) env isevars lvar c in
 		      let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
 		      let typ' = nf_isevar !isevars typ in
-		      let tycon = 
-			option_map 
-			  (fun (abs, ty) ->
-			     match abs with
-				 None ->
-				   isevars := Coercion.inh_conv_coerces_to loc env !isevars typ'
-				     (abs, ty);
-				   (abs, ty)
-			       | Some (init, cur) ->
-				   isevars := Coercion.inh_conv_coerces_to loc env !isevars typ' 
-				     (abs, ty);
-				   (Some (init, pred cur), ty))
-			  tycon
-		      in 
 			apply_rec env (n+1) 
 			  { uj_val = nf_isevar !isevars value;
-			    uj_type = nf_isevar !isevars typ' }
-			  (option_map (fun (abs, c) -> abs, nf_isevar !isevars c) tycon) rest
-
+			    uj_type = typ' }
+			  rest
 		  | _ ->
 		      let hj = pretype empty_tycon env isevars lvar c in
 			error_cant_apply_not_functional_loc 
 			  (join_loc floc argloc) env (evars_of !isevars)
 	      		  resj [hj]
 	in
-	let ftycon = option_map (lift_abstr_tycon_type (-1)) ftycon in
-	let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj ftycon args) in
+	let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj args) in
 	let resj =
 	  match kind_of_term resj.uj_val with
 	  | App (f,args) when isInd f ->
@@ -590,12 +566,19 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  tycon env (* loc *) (po,tml,eqns)
 
     | RCast(loc,c,k,t) ->
-	let tj = pretype_type empty_valcon env isevars lvar t in
-	let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in
-	  (* User Casts are for helping pretyping, experimentally not to be kept*)
-	  (* ... except for Correctness *)
-	let v = mkCast (cj.uj_val, k, tj.utj_val) in
-	let cj = { uj_val = v; uj_type = tj.utj_val } in
+	let cj =
+	  match k with
+	      CastCoerce ->
+		let cj = pretype empty_tycon env isevars lvar c in
+		  evd_comb1 (Coercion.inh_coerce_to_base loc env) isevars cj
+	    | CastConv k ->
+		let tj = pretype_type empty_valcon env isevars lvar t in
+		let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in
+		  (* User Casts are for helping pretyping, experimentally not to be kept*)
+		  (* ... except for Correctness *)
+		let v = mkCast (cj.uj_val, k, tj.utj_val) in
+		  { uj_val = v; uj_type = tj.utj_val }
+	in
 	  inh_conv_coerce_to_tycon loc env isevars cj tycon
 
     | RDynamic (loc,d) ->
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index d536adcb0..480ee13b2 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -47,6 +47,10 @@ type 'a bindings =
 
 type 'a with_bindings = 'a * 'a bindings
 
+type cast_type =
+  | CastConv of cast_kind
+  | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *)
+
 type rawconstr = 
   | RRef of (loc * global_reference)
   | RVar of (loc * identifier)
@@ -64,7 +68,7 @@ type rawconstr =
       rawconstr array * rawconstr array
   | RSort of loc * rawsort
   | RHole of (loc * hole_kind)
-  | RCast of loc * rawconstr * cast_kind * rawconstr
+  | RCast of loc * rawconstr * cast_type * rawconstr
   | RDynamic of loc * Dyn.t
 
 and rawdecl = name * rawconstr option * rawconstr
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index d85ca0158..d64ba03a7 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -44,6 +44,10 @@ type 'a bindings =
 
 type 'a with_bindings = 'a * 'a bindings
 
+type cast_type =
+  | CastConv of cast_kind
+  | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *)
+
 type rawconstr = 
   | RRef of (loc * global_reference)
   | RVar of (loc * identifier)
@@ -61,7 +65,7 @@ type rawconstr =
       rawconstr array * rawconstr array
   | RSort of loc * rawsort
   | RHole of (loc * Evd.hole_kind)
-  | RCast of loc * rawconstr * cast_kind * rawconstr
+  | RCast of loc * rawconstr * cast_type * rawconstr
   | RDynamic of loc * Dyn.t
 
 and rawdecl = name * rawconstr option * rawconstr
diff --git a/toplevel/command.ml b/toplevel/command.ml
index bfead59aa..0f7f449ce 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -112,7 +112,7 @@ let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) =
     | Some comtyp ->
 	(* We use a cast to avoid troubles with evars in comtyp *)
 	(* that can only be resolved knowing com *)
-	let b = abstract_constr_expr (mkCastC (com,DEFAULTcast,comtyp)) bl in
+	let b = abstract_constr_expr (mkCastC (com, Rawterm.CastConv DEFAULTcast,comtyp)) bl in
 	let (body,typ) = destSubCast (interp_constr sigma env b) in
 	{ const_entry_body = body;
 	  const_entry_type = Some typ;
diff --git a/toplevel/record.ml b/toplevel/record.ml
index f4f0c9150..9c2d9732a 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -36,7 +36,7 @@ let interp_decl sigma env = function
   | Vernacexpr.DefExpr((_,id),c,t) ->
       let c = match t with
 	| None -> c
-	| Some t -> mkCastC (c,DEFAULTcast,t)
+	| Some t -> mkCastC (c, Rawterm.CastConv DEFAULTcast,t)
       in
       let j = interp_constr_judgment Evd.empty env c in
       (id,Some j.uj_val, j.uj_type)