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

6 files changed, 21 insertions, 16 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index e05fe036d..fb3c7940b 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 afa516011..e13962ce8 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 4c9056f09..34d799745 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 a1181939f..dea45ac11 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 901866523..f0a44311b 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 768bc45c1..21c851dfb 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]