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

1 files changed, 8 insertions, 7 deletions

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
 
 (**********************************************************************)