Add a parameter to QuestionMark evar kind to say it can be turned into an obligations (even an opaque one).

Change cast_type to include the converted-to type or nothing in case of a Coerce cast, required much minor changes.
Various little subtac changes.


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

40 files changed, 227 insertions, 161 deletions

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 3fb6641879..dc1dc2cfb2 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -209,7 +209,7 @@ let rec is_rec names =
   let rec lookup names = function 
     | RVar(_,id) -> check_id id names
     | RRef _ | REvar _ | RPatVar _ | RSort _ |  RHole _ | RDynamic _ -> false
-    | RCast(_,b,_,_) -> lookup names b
+    | RCast(_,b,_) -> lookup names b
     | RRec _ -> error "RRec not handled"
     | RIf(_,b,_,lhs,rhs) -> 
 	(lookup names b) || (lookup names lhs) || (lookup names rhs)
@@ -611,8 +611,10 @@ let rec add_args id new_args b =
   | CPatVar _ -> b
   | CEvar _ -> b
   | CSort _ -> b
-  | CCast(loc,b1,ck,b2)  -> 
-      CCast(loc,add_args id new_args b1,ck,add_args id new_args b2)
+  | CCast(loc,b1,CastConv(ck,b2))  -> 
+      CCast(loc,add_args id new_args b1,CastConv(ck,add_args id new_args b2))
+  | CCast(loc,b1,CastCoerce) ->
+      CCast(loc,add_args id new_args b1,CastCoerce)
   | CNotation _ -> anomaly "add_args : CNotation"
   | CPrim _ -> b
   | CDelimiters _ -> anomaly "add_args : CDelimiters"
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index aca84f0627..b34a1097a3 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -351,7 +351,7 @@ let rec find_type_of nb b =
 	  then raise (Invalid_argument "find_type_of : not a valid inductive");
 	  ind_type	   
 	end
-    | RCast(_,b,_,_) -> find_type_of nb b 
+    | RCast(_,b,_) -> find_type_of nb b 
     | RApp _ -> assert false (* we have decomposed any application via raw_decompose_app *)
     | _ -> raise (Invalid_argument "not a ref")
     
@@ -575,7 +575,7 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 		let f_res = build_entry_lc env funnames args_res.to_avoid f in
 		combine_results combine_app f_res  args_res
 	    | RDynamic _ ->error "Not handled RDynamic" 
-	    | RCast(_,b,_,_) -> 
+	    | RCast(_,b,_) -> 
 		(* for an applied cast we just trash the cast part 
 		   and restart the work. 
 
@@ -685,7 +685,7 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 
 	end
     | RRec _ -> error "Not handled RRec"
-    | RCast(_,b,_,_) -> 
+    | RCast(_,b,_) -> 
 	build_entry_lc env funnames  avoid b
     | RDynamic _ -> error "Not handled RDynamic"
 and build_entry_lc_from_case env funname make_discr
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index 6af8d2c36c..f9e188dacf 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -18,7 +18,7 @@ let mkRLetIn(n,t,b) = RLetIn(dummy_loc,n,t,b)
 let mkRCases(rto,l,brl) = RCases(dummy_loc,rto,l,brl)
 let mkRSort s = RSort(dummy_loc,s)
 let mkRHole () = RHole(dummy_loc,Evd.BinderType Anonymous)
-let mkRCast(b,t) = RCast(dummy_loc,b,CastCoerce,t)
+let mkRCast(b,t) = RCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t))
 
 (*
   Some basic functions to decompose rawconstrs
@@ -177,8 +177,10 @@ let change_vars =
       | RRec _ -> error "Local (co)fixes are not supported"
       | RSort _ -> rt 
       | RHole _ -> rt 
-      | RCast(loc,b,k,t) -> 
-	  RCast(loc,change_vars mapping b,k,change_vars mapping t)
+      | RCast(loc,b,CastConv (k,t)) -> 
+	  RCast(loc,change_vars mapping b, CastConv (k,change_vars mapping t))
+      | RCast(loc,b,CastCoerce) -> 
+	  RCast(loc,change_vars mapping b,CastCoerce)
       | RDynamic _ -> error "Not handled RDynamic"
   and change_vars_br mapping ((loc,idl,patl,res) as br) = 
     let new_mapping = List.fold_right Idmap.remove idl mapping in 
@@ -356,8 +358,10 @@ let rec alpha_rt excluded rt =
     | RRec _ -> error "Not handled RRec"
     | RSort _ -> rt 
     | RHole _ -> rt 
-    | RCast (loc,b,k,t) -> 
-	RCast(loc,alpha_rt excluded b,k,alpha_rt excluded t)
+    | RCast (loc,b,CastConv (k,t)) -> 
+	RCast(loc,alpha_rt excluded b,CastConv(k,alpha_rt excluded t))
+    | RCast (loc,b,CastCoerce) -> 
+	RCast(loc,alpha_rt excluded b,CastCoerce)
     | RDynamic _ -> error "Not handled RDynamic"
     | RApp(loc,f,args) -> 
 	RApp(loc,
@@ -407,7 +411,8 @@ let is_free_in id =
     | RRec _ -> raise (UserError("",str "Not handled RRec"))
     | RSort _ -> false
     | RHole _ -> false
-    | RCast (_,b,_,t) -> is_free_in b || is_free_in t
+    | RCast (_,b,CastConv (_,t)) -> is_free_in b || is_free_in t
+    | RCast (_,b,CastCoerce) -> is_free_in b
     | RDynamic _ -> raise (UserError("",str "Not handled RDynamic"))
   and is_free_in_br (_,ids,_,rt) =
     (not (List.mem id ids)) && is_free_in rt
@@ -501,8 +506,10 @@ let replace_var_by_term x_id term =
       | RRec _ -> raise (UserError("",str "Not handled RRec"))
       | RSort _ -> rt 
       | RHole _ -> rt 
-      | RCast(loc,b,k,t) -> 
-	  RCast(loc,replace_var_by_pattern b,k,replace_var_by_pattern t)
+      | RCast(loc,b,CastConv(k,t)) -> 
+	  RCast(loc,replace_var_by_pattern b,CastConv(k,replace_var_by_pattern t))
+      | RCast(loc,b,CastCoerce) -> 
+	  RCast(loc,replace_var_by_pattern b,CastCoerce)
       | RDynamic _ -> raise (UserError("",str "Not handled RDynamic"))
   and replace_var_by_pattern_br ((loc,idl,patl,res) as br) = 
     if List.exists (fun id -> id_ord id x_id == 0) idl 
@@ -586,7 +593,8 @@ let ids_of_rawterm c =
       | RLambda (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
       | RProd (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
       | RLetIn (loc,na,b,c) -> idof na :: ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
-      | RCast (loc,c,k,t) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc
+      | RCast (loc,c,CastConv(k,t)) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc
+      | RCast (loc,c,CastCoerce) -> ids_of_rawterm [] c @ acc
       | RIf (loc,c,(na,po),b1,b2) -> ids_of_rawterm [] c @ ids_of_rawterm [] b1 @ ids_of_rawterm [] b2 @ acc
       | RLetTuple (_,nal,(na,po),b,c) -> 
           List.map idof nal @ ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
@@ -651,8 +659,10 @@ let zeta_normalize =
       | RRec _ -> raise (UserError("",str "Not handled RRec"))
       | RSort _ -> rt 
       | RHole _ -> rt 
-      | RCast(loc,b,k,t) -> 
-	  RCast(loc,zeta_normalize_term b,k,zeta_normalize_term t)
+      | RCast(loc,b,CastConv(k,t)) -> 
+	  RCast(loc,zeta_normalize_term b,CastConv(k,zeta_normalize_term t))
+      | RCast(loc,b,CastCoerce) -> 
+	  RCast(loc,zeta_normalize_term b,CastCoerce)
       | RDynamic _ -> raise (UserError("",str "Not handled RDynamic"))
   and zeta_normalize_br (loc,idl,patl,res) = 
     (loc,idl,patl,zeta_normalize_term res)
@@ -692,7 +702,8 @@ let expand_as =
 	      expand_as map br1, expand_as map br2)
       | RRec _ ->  error "Not handled RRec"
       | RDynamic _ -> error "Not handled RDynamic"
-      | RCast(loc,b,kind,t) -> RCast(loc,expand_as map b,kind,expand_as map t)
+      | RCast(loc,b,CastConv(kind,t)) -> RCast(loc,expand_as map b,CastConv(kind,expand_as map t))
+      | RCast(loc,b,CastCoerce) -> RCast(loc,expand_as map b,CastCoerce)
       | RCases(loc,po,el,brl) ->
 	  RCases(loc, option_map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
 		List.map (expand_as_br map) brl)
diff --git a/contrib/subtac/FunctionalExtensionality.v b/contrib/subtac/FunctionalExtensionality.v
index 07a19ab376..4610f3467a 100644
--- a/contrib/subtac/FunctionalExtensionality.v
+++ b/contrib/subtac/FunctionalExtensionality.v
@@ -1,3 +1,11 @@
+Lemma equal_f : forall A B : Type, forall (f g : A -> B), 
+  f = g -> forall x, f x = g x.
+Proof.
+  intros.
+  rewrite H.
+  auto.
+Qed.
+
 Axiom fun_extensionality : forall A B (f g : A -> B), 
   (forall x, f x = g x) -> f = g.
 
diff --git a/contrib/subtac/SubtacTactics.v b/contrib/subtac/SubtacTactics.v
index e678cf5d93..e1c48769c4 100644
--- a/contrib/subtac/SubtacTactics.v
+++ b/contrib/subtac/SubtacTactics.v
@@ -24,14 +24,19 @@ Ltac induction_with_subterms c c' H :=
 
 Ltac destruct_one_pair :=
  match goal with
- | [H : (ex _) |- _] => destruct H
- | [H : (ex2 _) |- _] => destruct H
- | [H : (sig _) |- _] => destruct H
- | [H : (_ /\ _) |- _] => destruct H
- | [H : prod _ _ |- _] => destruct H
-end.
+   | [H : (ex2 _) |- _] => destruct H
+   | [H : (_ /\ _) |- _] => destruct H
+   | [H : prod _ _ |- _] => destruct H
+ end.
 
-Ltac destruct_exists := repeat (destruct_one_pair) .
+Ltac destruct_one_ex :=
+  let tac H := let ph := fresh "H" in destruct H as [H ph] in
+    match goal with
+      | [H : (ex _) |- _] => tac H
+      | [H : (sig ?P) |- _ ] => tac H
+    end.
+
+Ltac destruct_exists := repeat (destruct_one_pair || destruct_one_ex).
 
 Ltac on_call f tac :=
   match goal with
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index 6250794526..bf4876a03c 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -2,58 +2,37 @@ Require Export Coq.subtac.SubtacTactics.
 
 Set Implicit Arguments.
 
-Notation "'fun' { x : A | P } => Q" :=
-  (fun x:{x:A|P} => Q)
-  (at level 200, x ident, right associativity).
-
 Notation " {{ x }} " := (tt : { y : unit | x }).
 
-Notation "( x & ? )" := (@exist _ _ x _) : core_scope.
+Notation "{ ( x , y )  :  A  |  P }" := 
+  (sig (fun t:A => let (x,y) := t in P))
+  (x ident, y ident) : type_scope.
 
 Notation " ! " := (False_rect _ _).
 
-Require Import Coq.Bool.Sumbool.	
-Notation "'dec'" := (sumbool_of_bool) (at level 0). 
-
-Definition ex_pi1 (A : Prop) (P : A -> Prop) (t : ex P) : A.
-intros.
-induction t.
-exact x.
-Defined.
+Notation "` t" := (proj1_sig t) (at level 100) : core_scope.
+Notation "( x & ? )" := (@exist _ _ x _) : core_scope.
 
-Lemma ex_pi2  : forall (A : Prop) (P : A -> Prop) (t : ex P),
- P (ex_pi1 t).
-intros A P.
-dependent inversion t.
-simpl.
-exact p.
-Defined.
+(** Coerces objects before comparing them *)
+Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70).
 
+(** Quantifying over subsets *)
+Notation "'fun' { x : A | P } => Q" :=
+  (fun x:{x:A|P} => Q)
+  (at level 200, x ident, right associativity).
 
-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).
 
-Lemma subset_simpl : forall (A : Set) (P : A -> Prop) 
-	(t : sig P), P (` t).
-Proof.
-intros.
-induction t.
- simpl ; auto.
-Qed.
-
-Lemma equal_f : forall A B : Type, forall (f g : A -> B), 
-  f = g -> forall x, f x = g x.
-Proof.
-  intros.
-  rewrite H.
-  auto.
-Qed.
+Require Import Coq.Bool.Sumbool.	
+Notation "'dec'" := (sumbool_of_bool) (at level 0). 
 
+(** Default simplification tactic. *)
 Ltac subtac_simpl := simpl ; intros ; destruct_exists ; simpl in * ; try subst ; 
-  try (solve [ red ; intros ; discriminate ]) ; auto with arith.  
+  try (solve [ red ; intros ; discriminate ]) ; auto with *.  
 
+(** Extraction directives *)
 Extraction Inline proj1_sig.
 Extract Inductive unit => "unit" [ "()" ].
 Extract Inductive bool => "bool" [ "true" "false" ].
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index e0711cade9..1989e7dcf0 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -65,7 +65,8 @@ let subst_evar_constr evs n t =
 	     and we must not apply to defined ones (i.e. LetIn's)
 	  *)
 	let args = 
-	  let (l, r) = list_split_at chop (List.rev (Array.to_list args)) in
+	  let n = match chop with None -> 0 | Some c -> c in 
+	  let (l, r) = list_split_at n (List.rev (Array.to_list args)) in
 	    List.rev r
 	in
 	let args =
@@ -144,14 +145,16 @@ let rec chop_product n t =
       | Prod (_, _, b) ->  if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None
       | _ -> None
 
-let eterm_obligations name nclen evm fs t tycon = 
+let eterm_obligations name nclen isevars evm fs t tycon = 
   (* 'Serialize' the evars, we assume that the types of the existentials
      refer to previous existentials in the list only *)
   let evl = List.rev (to_list evm) in
   let evn = 
     let i = ref (-1) in
       List.rev_map (fun (id, ev) -> incr i; 
-		  (id, (!i, id_of_string (string_of_id name ^ "_obligation_" ^ string_of_int (succ !i))), ev)) evl
+		      (id, (!i, id_of_string
+			      (string_of_id name ^ "_obligation_" ^ string_of_int (succ !i))),
+		       ev)) evl
   in
   let evts = 
     (* Remove existential variables in types and build the corresponding products *)
@@ -171,7 +174,10 @@ let eterm_obligations name nclen evm fs t tycon =
 		 t, trunc_named_context fs hyps, fs
 	     | None -> evtyp, hyps, 0
 	 in
-	 let y' = (id, ((n, nstr), hyps, chop, evtyp, deps)) in
+	 let loc, k = evar_source id isevars in
+	 let opacity = match k with QuestionMark o -> o | _ -> true in
+	 let opaque = if not opacity || chop <> fs then None else Some chop in
+	 let y' = (id, ((n, nstr), hyps, opaque, evtyp, deps)) in
 	   y' :: l) 
       evn []
   in 
@@ -179,7 +185,7 @@ let eterm_obligations name nclen evm fs t tycon =
     subst_evar_constr evts 0 t 
   in
   let evars = 
-    List.map (fun (_, ((_, name), _, chop, typ, deps)) -> name, typ, chop = fs, deps) evts
+    List.map (fun (_, ((_, name), _, opaque, typ, deps)) -> name, typ, not (opaque = None), deps) evts
   in
     (try
        trace (str "Term given to eterm" ++ spc () ++
diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli
index a67020c52d..71fd766e35 100644
--- a/contrib/subtac/eterm.mli
+++ b/contrib/subtac/eterm.mli
@@ -18,9 +18,10 @@ val mkMetas : int -> constr list
 
 (* val eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) list *)
 
-val eterm_obligations : identifier -> int -> evar_map -> int -> constr -> types option -> (* id, named context length, evars, number of
-											     function prototypes to try to clear from evars contexts *)
+(* id, named context length, evars, number of
+   function prototypes to try to clear from evars contexts, object and optional type *)
+val eterm_obligations : identifier -> int -> evar_defs -> evar_map -> int -> constr -> types option -> 
   (identifier * types * bool * Intset.t) array * constr
-    (* Obl. name, type as product, chopping of products flag, and dependencies as indexes into the array *)
+    (* Obl. name, type as product, opacity (true = opaque) and dependencies as indexes into the array *)
 
 val etermtac : open_constr -> tactic
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index b697e93320..fc2da8f587 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -145,10 +145,28 @@ let print_subgoals () = Options.if_verbose (fun () -> msg (Printer.pr_open_subgo
 let start_proof_and_print env isevars idopt k t hook =
   start_proof_com env isevars idopt k t hook;
   print_subgoals ()
-  (*if !pcoq <> None then (out_some !pcoq).start_proof ()*)
+(*     if !pcoq <> None then (out_some !pcoq).start_proof () *)
 
 let _ = Detyping.set_detype_anonymous (fun loc n -> RVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n)))
 
+
+let assumption_message id =
+  Options.if_verbose message ((string_of_id id) ^ " is assumed")
+
+let declare_assumption env isevars idl is_coe k bl c =
+  if not (Pfedit.refining ()) then 
+    let evm, c, typ = 
+      Subtac_pretyping.subtac_process env isevars (snd (List.hd idl)) [] (Command.generalize_constr_expr c bl) None 
+    in
+      List.iter (Command.declare_one_assumption is_coe k c) idl
+  else
+    errorlabstrm "Command.Assumption"
+	(str "Cannot declare an assumption while in proof editing mode.")
+
+let vernac_assumption env isevars kind l =
+  List.iter (fun (is_coe,(idl,c)) -> declare_assumption env isevars idl is_coe kind [] c) l
+
+
 let subtac (loc, command) =
   check_required_library ["Coq";"Init";"Datatypes"];
   check_required_library ["Coq";"Init";"Specif"];
@@ -159,7 +177,7 @@ let subtac (loc, command) =
   let env = Global.env () in
   let isevars = ref (create_evar_defs Evd.empty) in
   try
-    match command with
+  match command with
 	VernacDefinition (defkind, (locid, id), expr, hook) -> 
 	    (match expr with
 		 ProveBody (bl, c) -> Subtac_pretyping.subtac_proof env isevars id bl c None
@@ -190,6 +208,8 @@ let subtac (loc, command) =
 	  start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook
 
 
+      | VernacAssumption (stre,l) -> 
+	  vernac_assumption env isevars stre l
 
       (*| VernacEndProof e -> 
 	  subtac_end_proof e*)
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index b7243374b2..72fd421893 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1762,7 +1762,7 @@ let constrs_of_pats typing_fun tycon env isevars eqns tomatchs sign neqs arity =
 	       | l -> RApp (dummy_loc, bref, l)
 	 in
 	 let branch = match ineqs with
-	     Some _ -> RApp (dummy_loc, branch, [ RHole (dummy_loc, Evd.QuestionMark) ])
+	     Some _ -> RApp (dummy_loc, branch, [ RHole (dummy_loc, Evd.QuestionMark true) ])
 	   | None -> branch
 	 in
 	   (* 	 let branch =  *)
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 94f1bdec0a..09ed69fb4d 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -286,7 +286,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
 	  mkApp (constr_of_reference (Lazy.force fix_sub_ref), 
 		 [| argtyp ;
 		    wf_rel ;
-		    make_existential dummy_loc intern_before_env isevars wf_proof ;
+		    make_existential dummy_loc ~opaque:false intern_before_env isevars wf_proof ;
 		    prop ;
 		    intern_body_lam |])
       | Some f ->
@@ -309,7 +309,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
 (*   in *)
   let evm = non_instanciated_map env isevars in
     (*   let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm)  with _ -> () in *)
-  let evars, evars_def = Eterm.eterm_obligations recname nc_len evm 0 fullcoqc (Some fullctyp) in
+  let evars, evars_def = Eterm.eterm_obligations recname nc_len !isevars evm 0 fullcoqc (Some fullctyp) in
     (*     (try trace (str "Generated obligations : "); *)
 (*        Array.iter *)
     (* 	 (fun (n, t, _) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t)) *)
@@ -392,7 +392,7 @@ let build_mutrec l boxed =
       and typ = 
 	Termops.it_mkNamedProd_or_LetIn typ rec_sign
       in
-      let evars, def = Eterm.eterm_obligations id nc_len evm recdefs def (Some typ) in
+      let evars, def = Eterm.eterm_obligations id nc_len isevars evm recdefs def (Some typ) in
 	collect_evars (succ i) ((id, def, typ, evars) :: acc)
     else acc
   in 
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index 647c47b6ad..e83ee66585 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -151,5 +151,5 @@ let subtac_proof env isevars id l c tycon =
   let nc = named_context env in
   let nc_len = named_context_length nc in
   let evm, coqc, coqt = subtac_process env isevars id l c tycon in
-  let evars, def = Eterm.eterm_obligations id nc_len evm 0 coqc (Some coqt) in
+  let evars, def = Eterm.eterm_obligations id nc_len !isevars evm 0 coqc (Some coqt) in
     add_definition id def coqt evars
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 990ee115f6..c2132f61b5 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -495,13 +495,13 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  ((fun vtyc env -> pretype vtyc env isevars lvar),isevars)
 	  tycon env (* loc *) (po,tml,eqns)
 
-    | RCast(loc,c,k,t) ->
+    | RCast(loc,c,k) ->
 	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 ->
+	    | CastConv (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*)
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 4dc157397a..2e362a2107 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -152,8 +152,8 @@ let app_opt c e =
 let print_args env args = 
   Array.fold_right (fun a acc -> my_print_constr env a ++ spc () ++ acc) args (str "")
 
-let make_existential loc env isevars c =
-  let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark) c in
+let make_existential loc ?(opaque = true) env isevars c =
+  let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c in
   let (key, args) = destEvar evar in
     (try trace (str "Constructed evar " ++ int key ++ str " applied to args: " ++
 		  print_args env args ++ str " for type: "++ 
@@ -169,7 +169,7 @@ let make_existential_expr loc env c =
 let string_of_hole_kind = function
   | ImplicitArg _ -> "ImplicitArg"
   | BinderType _ -> "BinderType"
-  | QuestionMark -> "QuestionMark"
+  | QuestionMark _ -> "QuestionMark"
   | CasesType -> "CasesType"
   | InternalHole -> "InternalHole"
   | TomatchTypeParameter _ -> "TomatchTypeParameter"
@@ -182,7 +182,7 @@ let non_instanciated_map env evd =
 	   debug 2 (str "evar " ++ int key ++ str " has kind " ++ 
 		      str (string_of_hole_kind k));
 	   match k with 
-	       QuestionMark -> Evd.add evm key evi
+	       QuestionMark _ -> Evd.add evm key evi
 	     | _ ->
 	       debug 2 (str " and is an implicit");
 	       Pretype_errors.error_unsolvable_implicit loc env evm k)
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 00f01d6e1c..37ee1ac23a 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -82,7 +82,7 @@ val wf_relations : (constr, constr lazy_t) Hashtbl.t
 type binders = local_binder list
 val app_opt : ('a -> 'a) option -> 'a -> 'a
 val print_args : env -> constr array -> std_ppcmds
-val make_existential : loc -> env -> evar_defs ref -> types -> constr
+val make_existential : loc -> ?opaque:bool -> env -> evar_defs ref -> types -> constr
 val make_existential_expr : loc -> 'a -> 'b -> constr_expr
 val string_of_hole_kind : hole_kind -> string
 val non_instanciated_map : env -> evar_defs ref -> evar_map
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 96548df711..4fbf57e07a 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -204,9 +204,11 @@ let rec check_same_type ty1 ty2 =
   | CHole _, CHole _ -> ()
   | CPatVar(_,i1), CPatVar(_,i2) when i1=i2 -> ()
   | CSort(_,s1), CSort(_,s2) when s1=s2 -> ()
-  | CCast(_,a1,_,b1), CCast(_,a2,_,b2) ->
+  | CCast(_,a1,CastConv (_,b1)), CCast(_,a2, CastConv(_,b2)) ->
       check_same_type a1 a2;
       check_same_type b1 b2
+  | CCast(_,a1,CastCoerce), CCast(_,a2, CastCoerce) ->
+      check_same_type a1 a2
   | CNotation(_,n1,e1), CNotation(_,n2,e2) when n1=n2 ->
       List.iter2 check_same_type e1 e2
   | CPrim(_,i1), CPrim(_,i2) when i1=i2 -> ()
@@ -296,8 +298,8 @@ let rec same_raw c d =
   | RSort(_,s1), RSort(_,s2) -> if s1<>s2 then failwith "RSort"
   | RHole _, _ -> ()
   | _, RHole _ -> ()
-  | RCast(_,c1,_,_),r2 -> same_raw c1 r2
-  | r1, RCast(_,c2,_,_) -> same_raw r1 c2
+  | RCast(_,c1,_),r2 -> same_raw c1 r2
+  | r1, RCast(_,c2,_) -> same_raw r1 c2
   | RDynamic(_,d1), RDynamic(_,d2) -> if d1<>d2 then failwith"RDynamic"
   | _ -> failwith "same_raw"
      
@@ -757,8 +759,10 @@ let rec extern inctx scopes vars r =
 
   | RHole (loc,e) -> CHole loc
 
-  | RCast (loc,c,k,t) ->
-      CCast (loc,sub_extern true scopes vars c,k,extern_typ scopes vars t)
+  | RCast (loc,c, CastConv (k,t)) ->
+      CCast (loc,sub_extern true scopes vars c, CastConv (k,extern_typ scopes vars t))
+  | RCast (loc,c, CastCoerce) ->
+      CCast (loc,sub_extern true scopes vars c, CastCoerce)
 
   | RDynamic (loc,d) -> CDynamic (loc,d)
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 244f8228a9..5a41f35086 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -915,7 +915,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
         let p' = option_map (intern_type env'') po in
         RIf (loc, c', (na', p'), intern env b1, intern env b2)
     | CHole loc -> 
-	RHole (loc, Evd.QuestionMark)
+	RHole (loc, Evd.QuestionMark true)
     | CPatVar (loc, n) when allow_patvar ->
 	RPatVar (loc, n)
     | CPatVar (loc, _) ->
@@ -924,8 +924,10 @@ let internalise sigma globalenv env allow_patvar lvar c =
 	REvar (loc, n, None)
     | CSort (loc, s) ->
 	RSort(loc,s)
-    | CCast (loc, c1, k, c2) ->
-	RCast (loc,intern env c1,k,intern_type env c2)
+    | CCast (loc, c1, CastConv (k, c2)) ->
+	RCast (loc,intern env c1, CastConv (k, intern_type env c2))
+    | CCast (loc, c1, CastCoerce) ->
+	RCast (loc,intern env c1, CastCoerce)
 
     | CDynamic (loc,d) -> RDynamic (loc,d)
 
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 39ba6d6fd5..5a8eafff7b 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -73,7 +73,8 @@ let rec unloc = function
               bl,
             Array.map unloc tyl,
             Array.map unloc bv)
-  | RCast (_,c,k,t) -> RCast (dummy_loc,unloc c,k,unloc t)
+  | RCast (_,c, CastConv (k,t)) -> RCast (dummy_loc,unloc c, CastConv (k,unloc t))
+  | RCast (_,c, CastCoerce) -> RCast (dummy_loc,unloc c, CastCoerce)
   | RSort (_,x) -> RSort (dummy_loc,x)
   | RHole (_,x)  -> RHole (dummy_loc,x)
   | RRef (_,x) -> RRef (dummy_loc,x)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index da3f73149f..514c0811c7 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_type * aconstr
+  | ACast of aconstr * aconstr cast_type
 
 (**********************************************************************)
 (* Re-interpret a notation as a rawconstr, taking care of binders     *)
@@ -102,7 +102,10 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
   | AIf (c,(na,po),b1,b2) ->
       let e,na = name_fold_map 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) -> RCast (loc,f e c, 
+			  match k with 
+			    | CastConv (k,t) -> CastConv (k,f e t)
+			    | CastCoerce -> CastCoerce)
   | ASort x -> RSort (loc,x)
   | AHole x  -> RHole (loc,x)
   | APatVar n -> RPatVar (loc,(false,n))
@@ -196,7 +199,9 @@ let aconstr_and_vars_of_rawconstr a =
   | RIf (loc,c,(na,po),b1,b2) ->
       add_name found na;
       AIf (aux c,(na,option_map aux po),aux b1,aux b2)
-  | RCast (_,c,k,t) -> ACast (aux c,k,aux t)
+  | RCast (_,c,k) -> ACast (aux c, 
+			    match k with CastConv (k,t) -> CastConv (k,aux t) 
+			      | CastCoerce -> CastCoerce)
   | RSort (_,s) -> ASort s
   | RHole (_,w) -> AHole w
   | RRef (_,r) -> ARef r
@@ -342,15 +347,21 @@ let rec subst_aconstr subst bound raw =
       let ref',t = subst_global subst ref in 
 	if ref' == ref then raw else
 	  AHole (Evd.InternalHole)
-  | AHole (Evd.BinderType _ | Evd.QuestionMark | Evd.CasesType |
-      Evd.InternalHole | Evd.TomatchTypeParameter _) -> raw
-
-  | ACast (r1,k,r2) -> 
-      let r1' = subst_aconstr subst bound r1 
-      and r2' = subst_aconstr subst bound r2 in
-	if r1' == r1 && r2' == r2 then raw else
-	  ACast (r1',k,r2')
-
+  | AHole (Evd.BinderType _ | Evd.QuestionMark _ | Evd.CasesType 
+    | Evd.InternalHole | Evd.TomatchTypeParameter _) -> raw
+
+  | ACast (r1,k) -> 
+      match k with
+	  CastConv (k, r2) ->
+	    let r1' = subst_aconstr subst bound r1 
+	    and r2' = subst_aconstr subst bound r2 in
+	      if r1' == r1 && r2' == r2 then raw else
+		ACast (r1',CastConv (k,r2'))
+	| CastCoerce ->
+	    let r1' = subst_aconstr subst bound r1 in
+	      if r1' == r1 then raw else
+		ACast (r1',CastCoerce)
+		  
 
 let encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l)
 
@@ -454,8 +465,10 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
       let (alp,sigma) =
 	List.fold_left2 (match_names metas) (alp,sigma) nal1 nal2 in
       match_ alp metas sigma c1 c2
-  | RCast(_,c1,_,t1), ACast(c2,_,t2) ->
+  | RCast(_,c1, CastConv(_,t1)), ACast(c2, CastConv (_,t2)) ->
       match_ alp metas (match_ alp metas sigma c1 c2) t1 t2
+  | RCast(_,c1, CastCoerce), ACast(c2, CastCoerce) ->
+      match_ alp metas sigma c1 c2
   | RSort (_,s1), ASort s2 when s1 = s2 -> sigma
   | RPatVar _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
   | a, AHole _ -> sigma
@@ -554,7 +567,7 @@ type constr_expr =
   | CPatVar of loc * (bool * patvar)
   | CEvar of loc * existential_key
   | CSort of loc * rawsort
-  | CCast of loc * constr_expr * cast_type * constr_expr
+  | CCast of loc * constr_expr * constr_expr cast_type
   | CNotation of loc * notation * constr_expr list
   | CPrim of loc * prim_token
   | CDelimiters of loc * string * constr_expr
@@ -616,7 +629,7 @@ let constr_loc = function
   | CPatVar (loc,_) -> loc
   | CEvar (loc,_) -> loc
   | CSort (loc,_) -> loc
-  | CCast (loc,_,_,_) -> loc
+  | CCast (loc,_,_) -> loc
   | CNotation (loc,_,_) -> loc
   | CPrim (loc,_) -> loc
   | CDelimiters (loc,_,_) -> loc
@@ -694,7 +707,8 @@ let fold_constr_expr_with_binders g f n acc = function
   | CApp (loc,(_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
   | CProdN (_,l,b) | CLambdaN (_,l,b) -> fold_constr_expr_binders g f n acc b l
   | CLetIn (_,na,a,b) -> fold_constr_expr_binders g f n acc b [[na],a]
-  | CCast (loc,a,_,b) -> f n (f n acc a) b
+  | CCast (loc,a,CastConv(_,b)) -> f n (f n acc a) b
+  | CCast (loc,a,CastCoerce) -> f n acc a
   | CNotation (_,_,l) -> List.fold_left (f n) acc l
   | CDelimiters (loc,_,a) -> f n acc a
   | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _  | CRef _ ->
@@ -731,7 +745,7 @@ let occur_var_constr_expr id c = Idset.mem id (free_vars_of_constr_expr c)
 let mkIdentC id  = CRef (Ident (dummy_loc, id))
 let mkRefC r     = CRef r
 let mkAppC (f,l) = CApp (dummy_loc, (None,f), List.map (fun x -> (x,None)) l)
-let mkCastC (a,k,b)  = CCast (dummy_loc,a,k,b)
+let mkCastC (a,k)  = CCast (dummy_loc,a,k)
 let mkLambdaC (idl,a,b) = CLambdaN (dummy_loc,[idl,a],b)
 let mkLetInC (id,a,b)   = CLetIn (dummy_loc,id,a,b)
 let mkProdC (idl,a,b)   = CProdN (dummy_loc,[idl,a],b)
@@ -804,7 +818,8 @@ let map_constr_expr_with_binders g f e = function
   | CLambdaN (loc,bl,b) ->
       let (e,bl) = map_binders f g e bl in CLambdaN (loc,bl,f e b)
   | CLetIn (loc,na,a,b) -> CLetIn (loc,na,f e a,f (name_fold g (snd na) e) b)
-  | CCast (loc,a,k,b) -> CCast (loc,f e a,k,f e b)
+  | CCast (loc,a,CastConv (k,b)) -> CCast (loc,f e a,CastConv(k, f e b))
+  | CCast (loc,a,CastCoerce) -> CCast (loc,f e a,CastCoerce)
   | CNotation (loc,n,l) -> CNotation (loc,n,List.map (f e) l)
   | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
   | CHole _ | CEvar _ | CPatVar _ | CSort _ 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 7d1a7a8096..75dbb7cf2b 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_type * aconstr
+  | ACast of aconstr * aconstr cast_type
 
 (**********************************************************************)
 (* Translate a rawconstr into a notation given the list of variables  *)
@@ -127,7 +127,7 @@ type constr_expr =
   | CPatVar of loc * (bool * patvar)
   | CEvar of loc * existential_key
   | CSort of loc * rawsort
-  | CCast of loc * constr_expr * cast_type * constr_expr
+  | CCast of loc * constr_expr * constr_expr cast_type
   | CNotation of loc * notation * constr_expr list
   | CPrim of loc * prim_token
   | CDelimiters of loc * string * constr_expr
@@ -167,7 +167,7 @@ val ids_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_type * constr_expr -> constr_expr
+val mkCastC : constr_expr * constr_expr cast_type -> 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 e05fe036d2..fb3c7940ba 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, CastConv DEFAULTcast, ty)
+  | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv (DEFAULTcast, ty))
 
 let mk_lam = function
     ([],c) -> c
@@ -138,13 +138,15 @@ GEXTEND Gram
       [ c = binder_constr -> c ]
     | "100" RIGHTA
       [ c1 = operconstr; "<:"; c2 = binder_constr -> 
-                 CCast(loc,c1, CastConv VMcast,c2)
+                 CCast(loc,c1, CastConv (VMcast,c2))
       | c1 = operconstr; "<:"; c2 = SELF -> 
-                 CCast(loc,c1, CastConv VMcast,c2)
+                 CCast(loc,c1, CastConv (VMcast,c2))
       | c1 = operconstr; ":";c2 = binder_constr -> 
-                 CCast(loc,c1, CastConv DEFAULTcast,c2)
+                 CCast(loc,c1, CastConv (DEFAULTcast,c2))
       | c1 = operconstr; ":"; c2 = SELF -> 
-                 CCast(loc,c1, CastConv DEFAULTcast,c2) ]
+                 CCast(loc,c1, CastConv (DEFAULTcast,c2)) 
+      | c1 = operconstr; ":>" ->
+                 CCast(loc,c1, CastCoerce) ]
     | "99" RIGHTA [ ]
     | "90" RIGHTA
       [ c1 = operconstr; "->"; c2 = binder_constr -> CArrow(loc,c1,c2)
@@ -317,7 +319,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, CastConv 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 afa5160116..e13962ce88 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -118,6 +118,6 @@ GEXTEND Gram
     ;
   constr_body:
     [ [ ":="; c = lconstr -> c
-      | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c, Rawterm.CastConv Term.DEFAULTcast,t) ] ]
+      | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c, Rawterm.CastConv (Term.DEFAULTcast,t)) ] ]
   ;
 END
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 4c9056f09b..34d7997456 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -204,7 +204,7 @@ GEXTEND Gram
   def_body:
     [ [ bl = LIST0 binder_let; ":="; red = reduce; c = lconstr ->
       (match c with
-          CCast(_,c,k,t) -> DefineBody (bl, red, c, Some t)
+          CCast(_,c, Rawterm.CastConv (k,t)) -> DefineBody (bl, red, c, Some t)
         | _ -> DefineBody (bl, red, c, None))
       | bl = LIST0 binder_let; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
           DefineBody (bl, red, c, Some t)
@@ -306,7 +306,7 @@ GEXTEND Gram
              t = lconstr; ":="; b = lconstr -> (oc,DefExpr (id,b,Some t))
       | id = name; ":="; b = lconstr ->
          match b with
-             CCast(_,b,_,t) -> (false,DefExpr(id,b,Some t))
+             CCast(_,b, Rawterm.CastConv (_, t)) -> (false,DefExpr(id,b,Some t))
            | _ -> (false,DefExpr(id,b,None)) ] ]
   ;
   assum_list:
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index a1181939f7..dea45ac11c 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -183,7 +183,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, CastConv 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/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 901866523f..f0a44311bc 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -215,7 +215,7 @@ let pr_binder_among_many pr_c = function
       pr_binder true pr_c (nal,t)
   | LocalRawDef (na,c) ->
       let c,topt = match c with
-        | CCast(_,c,_,t) -> c, t
+        | CCast(_,c, CastConv (_,t)) -> c, t
         | _ -> c, CHole dummy_loc in
       hov 1 (surround
         (pr_lname na ++ pr_opt_type pr_c topt ++
@@ -566,10 +566,13 @@ let rec pr sep inherited a =
   | CEvar (_,n) -> str (Evd.string_of_existential n), latom
   | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom
   | CSort (_,s) -> pr_rawsort s, latom
-  | CCast (_,a,k,b) ->
-      let s = match k with CastConv  VMcast -> "<:" | _ -> ":" in
+  | CCast (_,a,CastConv (k,b)) ->
+      let s = match k with VMcast -> "<:" | DEFAULTcast -> ":" in
       hv 0 (pr mt (lcast,L) a ++ cut () ++ str s ++ pr mt (-lcast,E) b),
       lcast
+  | CCast (_,a,CastCoerce) ->
+      hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":>"),
+      lcast
   | CNotation (_,"( _ )",[t]) ->
       pr (fun()->str"(") (max_int,L) t ++ str")", latom
   | CNotation (_,s,env) -> pr_notation (pr mt) s env
@@ -590,7 +593,7 @@ let pr = pr mt
 
 let rec strip_context n iscast t =
   if n = 0 then
-    [], if iscast then match t with CCast (_,c,_,_) -> c | _ -> t else t
+    [], if iscast then match t with CCast (_,c,_) -> c | _ -> t else t
   else match t with
     | CLambdaN (loc,(nal,t)::bll,c) ->
 	let n' = List.length nal in
@@ -613,7 +616,7 @@ let rec strip_context n iscast t =
     | CArrow (loc,t,c) ->
 	let bl', c = strip_context (n-1) iscast c in
 	LocalRawAssum ([loc,Anonymous],t) :: bl', c 
-    | CCast (_,c,_,_) -> strip_context n false c
+    | CCast (_,c,_) -> strip_context n false c
     | CLetIn (_,na,b,c) -> 
 	let bl', c = strip_context (n-1) iscast c in
 	LocalRawDef (na,b) :: bl', c
diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4
index 768bc45c14..21c851dfbe 100644
--- a/parsing/q_constr.ml4
+++ b/parsing/q_constr.ml4
@@ -73,7 +73,7 @@ EXTEND
     | "0"
       [ s = sort -> <:expr< Rawterm.RSort ($dloc$,s) >>
       | id = ident -> <:expr< Rawterm.RVar ($dloc$,$id$) >>
-      | "_" -> <:expr< Rawterm.RHole ($dloc$,QuestionMark) >>
+      | "_" -> <:expr< Rawterm.RHole ($dloc$, QuestionMark False) >>
       | "?"; id = ident -> <:expr< Rawterm.RPatVar($dloc$,(False,$id$)) >>
       | "{"; c1 = constr; "}"; "+"; "{"; c2 = constr; "}" ->
           apply_ref <:expr< coq_sumbool_ref >> [c1;c2]
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index a0071d5b6d..412275c108 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -380,8 +380,7 @@ let rec detype (isgoal:bool) avoid env t =
 	  RVar (dl, id))
     | Sort s -> RSort (dl,detype_sort s)
     | Cast (c1,k,c2) ->
-	RCast(dl,detype isgoal avoid env c1, CastConv k,
-              detype isgoal avoid env c2)
+	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
     | LetIn (na,b,_,c) -> detype_binder isgoal BLetIn avoid env na b c
@@ -633,14 +632,18 @@ let rec subst_rawconstr subst raw =
       let ref',_ = subst_global subst ref in 
 	if ref' == ref then raw else
 	  RHole (loc,InternalHole)
-  | RHole (loc, (BinderType _ | QuestionMark | CasesType |
+  | RHole (loc, (BinderType _ | QuestionMark _ | CasesType |
       InternalHole | TomatchTypeParameter _)) -> raw
 
-  | RCast (loc,r1,k,r2) -> 
-      let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in
-	if r1' == r1 && r2' == r2 then raw else
-	  RCast (loc,r1',k,r2')
-
+  | RCast (loc,r1,k) -> 
+      (match k with 
+	   CastConv (k,r2) ->
+	     let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in
+	       if r1' == r1 && r2' == r2 then raw else
+		 RCast (loc,r1', CastConv (k,r2'))
+	 | CastCoerce -> 
+	     let r1' = subst_rawconstr subst r1 in
+	       if r1' == r1 then raw else RCast (loc,r1',k))
   | RDynamic _ -> raw
 
 (* Utilities to transform kernel cases to simple pattern-matching problem *)
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index a247b5b1ef..b9a443317f 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -366,7 +366,7 @@ let metamap_to_list m =
 type hole_kind =
   | ImplicitArg of global_reference * (int * identifier option)
   | BinderType of name
-  | QuestionMark
+  | QuestionMark of bool
   | CasesType
   | InternalHole
   | TomatchTypeParameter of inductive * int
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index ac1ed145af..8a1f6a53f3 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -132,7 +132,7 @@ val evars_reset_evd  : evar_map ->  evar_defs -> evar_defs
 type hole_kind =
   | ImplicitArg of global_reference * (int * identifier option)
   | BinderType of name
-  | QuestionMark
+  | QuestionMark of bool (* Can it be turned into an obligation ? *)
   | CasesType
   | InternalHole
   | TomatchTypeParameter of inductive * int
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index b0fd76cb76..c3b49b9749 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -233,7 +233,7 @@ let rec pat_of_raw metas vars = function
       PSort s
   | RHole _ ->
       PMeta None
-  | RCast (_,c,_,t) ->
+  | RCast (_,c,_) ->
       Options.if_verbose
         Pp.warning "Cast not taken into account in constr pattern";
       pat_of_raw metas vars c
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index dc3ea869c1..3aefeeb077 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -578,13 +578,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  ((fun vtyc env -> pretype vtyc env isevars lvar),isevars)
 	  tycon env (* loc *) (po,tml,eqns)
 
-    | RCast(loc,c,k,t) ->
+    | RCast (loc,c,k) ->
 	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 ->
+	    | CastConv (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*)
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 683182bc1f..63e40a0521 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -47,8 +47,8 @@ type 'a bindings =
 
 type 'a with_bindings = 'a * 'a bindings
 
-type cast_type =
-  | CastConv of cast_kind
+type 'a cast_type =
+  | CastConv of cast_kind * 'a
   | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *)
 
 type rawconstr = 
@@ -68,7 +68,7 @@ type rawconstr =
       rawconstr array * rawconstr array
   | RSort of loc * rawsort
   | RHole of (loc * hole_kind)
-  | RCast of loc * rawconstr * cast_type * rawconstr
+  | RCast of loc * rawconstr * rawconstr cast_type
   | RDynamic of loc * Dyn.t
 
 and rawdecl = name * rawconstr option * rawconstr
@@ -120,7 +120,7 @@ let map_rawconstr f = function
   | RRec (loc,fk,idl,bl,tyl,bv) ->
       RRec (loc,fk,idl,Array.map (List.map (map_rawdecl f)) bl,
             Array.map f tyl,Array.map f bv)
-  | RCast (loc,c,k,t) -> RCast (loc,f c,k,f t)
+  | RCast (loc,c,k) -> RCast (loc,f c, match k with CastConv (k,t) -> CastConv (k, f t) | x -> x)
   | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) as x -> x
   
 
@@ -190,7 +190,7 @@ let occur_rawconstr id =
                 (na=Name id or not(occur_fix bl)) in
           occur_fix bl)
           idl bl tyl bv)
-    | RCast (loc,c,_,t) -> (occur c) or (occur t)
+    | RCast (loc,c,k) -> (occur c) or (match k with CastConv (_, t) -> occur t | CastCoerce -> false)
     | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> false
 
   and occur_pattern (loc,idl,p,c) = not (List.mem id idl) & (occur c)
@@ -247,7 +247,8 @@ let free_rawvars  =
 	  vars bounded1 vs2 bv.(i)
 	in
 	array_fold_left_i vars_fix vs idl
-    | RCast (loc,c,_,t) -> vars bounded (vars bounded vs c) t
+    | RCast (loc,c,k) -> let v = vars bounded vs c in 
+	(match k with CastConv (_,t) -> vars bounded v t | _ -> v)
     | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> vs
 
   and vars_pattern bounded vs (loc,idl,p,c) = 
@@ -280,7 +281,7 @@ let loc_of_rawconstr = function
   | RRec (loc,_,_,_,_,_) -> loc
   | RSort (loc,_) -> loc
   | RHole (loc,_) -> loc
-  | RCast (loc,_,_,_) -> loc
+  | RCast (loc,_,_) -> loc
   | RDynamic (loc,_) -> loc
 
 (**********************************************************************)
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 2a1fef22cd..c43c290e86 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -51,8 +51,8 @@ type 'a bindings =
 
 type 'a with_bindings = 'a * 'a bindings
 
-type cast_type =
-  | CastConv of cast_kind
+type 'a cast_type =
+  | CastConv of cast_kind * 'a
   | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *)
 
 type rawconstr = 
@@ -72,7 +72,7 @@ type rawconstr =
       rawconstr array * rawconstr array
   | RSort of loc * rawsort
   | RHole of (loc * Evd.hole_kind)
-  | RCast of loc * rawconstr * cast_type * rawconstr
+  | RCast of loc * rawconstr * rawconstr cast_type
   | RDynamic of loc * Dyn.t
 
 and rawdecl = name * rawconstr option * rawconstr
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index f341580eb1..87a472003f 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -346,7 +346,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
 	(fun (loc,(id,_)) -> 
 	   RVar (loc,id)) params in 
     let dum_args= 
-      list_tabulate (fun _ -> RHole (dummy_loc,Evd.QuestionMark))
+      list_tabulate (fun _ -> RHole (dummy_loc,Evd.QuestionMark false))
 	oib.Declarations.mind_nrealargs in
       raw_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in
   let pat_vars,aliases,patt = interp_pattern env pat in
@@ -369,7 +369,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
   let term2 =
     RLetIn(dummy_loc,Anonymous,
 	   RCast(dummy_loc,raw_of_pat npatt,
-		 CastConv DEFAULTcast,app_ind),term1) in
+		 CastConv (DEFAULTcast,app_ind)),term1) in
   let term3=List.fold_right let_in_one_alias aliases term2 in  
   let term4=List.fold_right prod_one_id loc_ids term3 in
   let term5=List.fold_right prod_one_hyp params term4 in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 971e0986ae..75f517023f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1246,7 +1246,7 @@ open Evd
 
 let solvable_by_tactic env evi (ev,args) src = 
   match (!implicit_tactic, src) with
-  | Some tac, (ImplicitArg _ | QuestionMark)
+  | Some tac, (ImplicitArg _ | QuestionMark _)
       when 
 	Environ.named_context_of_val evi.evar_hyps = 
 	Environ.named_context env ->
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 739a7b47f7..ecd0a6d7e3 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -111,7 +111,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, Rawterm.CastConv 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/command.mli b/toplevel/command.mli
index c4ef924474..9540888dd3 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -36,6 +36,9 @@ val declare_definition : identifier -> definition_kind ->
 
 val syntax_definition : identifier -> constr_expr -> bool -> bool -> unit
 
+val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types -> 
+  Names.variable located -> unit
+
 val declare_assumption : identifier located list ->
   coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> unit
 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 305685cc7b..49a1d07f7d 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -329,7 +329,7 @@ let explain_occur_check env ev rhs =
   str" with term" ++ brk(1,1) ++ pt
 
 let explain_hole_kind env = function
-  | QuestionMark -> str "a term for this placeholder"
+  | QuestionMark _ -> str "a term for this placeholder"
   | CasesType ->
       str "the type of this pattern-matching problem"
   | BinderType (Name id) ->
diff --git a/toplevel/record.ml b/toplevel/record.ml
index f3ec4732d7..b339d493b3 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, Rawterm.CastConv 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)
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index eb9fdae30e..b41bcec8b0 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -139,11 +139,11 @@ let rec uri_of_constr c =
   | RLetIn (_,na,b,c) ->
       url_string "let "; url_of_name na; url_string "\\def ";
       uri_of_constr b; url_string " in "; uri_of_constr c
-  | RCast (_,c,_,t) ->
+  | RCast (_,c, CastConv (_,t)) ->
       uri_of_constr c; url_string ":"; uri_of_constr t
   | RRec _ | RIf _ | RLetTuple _ | RCases _ ->
       error "Whelp does not support pattern-matching and (co-)fixpoint"
-  | RVar _ | RRef _ | RHole _ | REvar _ | RSort _ ->
+  | RVar _ | RRef _ | RHole _ | REvar _ | RSort _ | RCast (_,_, CastCoerce) ->
       anomaly "Written w/o parenthesis"
   | RPatVar _ | RDynamic _ -> 
       anomaly "Found constructors not supported in constr") ()