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

7 files changed, 27 insertions, 23 deletions

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