Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg

6 files changed, 33 insertions, 24 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 9163f3c1..1cde66e2 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: g_constr.ml4 9562 2007-01-31 09:00:36Z msozeau $ *)
+(* $Id: g_constr.ml4 9976 2007-07-12 11:58:30Z msozeau $ *)
 
 open Pcoq
 open Constr
@@ -21,14 +21,14 @@ open Util
 
 let constr_kw =
   [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; 
-    "end"; "as"; "let"; "if"; "then"; "else"; "return";
+    "end"; "as"; "let"; "dest"; "if"; "then"; "else"; "return";
     "Prop"; "Set"; "Type"; ".("; "_"; ".." ]
 
 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
@@ -156,13 +156,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)
@@ -210,6 +212,10 @@ GEXTEND Gram
 	  ":="; c1 = operconstr LEVEL "200"; "in";
           c2 = operconstr LEVEL "200" ->
           CLetTuple (loc,List.map snd lb,po,c1,c2)
+      | "dest"; c1 = operconstr LEVEL "200"; "as"; p=pattern;
+          "in"; c2 = operconstr LEVEL "200" ->
+         CCases (loc, None, [(c1, (None, None))],
+                 [loc, [[p]], c2])
       | "if"; c=operconstr LEVEL "200"; po = return_type;
 	"then"; b1=operconstr LEVEL "200";
         "else"; b2=operconstr LEVEL "200" ->
@@ -328,7 +334,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 2f515a81..0a48748f 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: g_proofs.ml4 9154 2006-09-20 17:18:18Z corbinea $ *)
+(* $Id: g_proofs.ml4 9976 2007-07-12 11:58:30Z msozeau $ *)
 
 open Pcoq
 open Pp
@@ -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 9a98df80..6a9388b2 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: g_vernac.ml4 9562 2007-01-31 09:00:36Z msozeau $ *)
+(* $Id: g_vernac.ml4 9977 2007-07-12 12:18:46Z msozeau $ *)
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
 open Pp
@@ -202,7 +202,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)
@@ -264,8 +264,8 @@ GEXTEND Gram
   ;
   rec_annotation:
     [ [ "{"; IDENT "struct"; id=IDENT; "}" -> (Some (id_of_string id), CStructRec)
-      | "{"; IDENT "wf"; rel=constr; id=IDENT; "}" -> (Some (id_of_string id), CWfRec rel) 
-      | "{"; IDENT "measure"; rel=constr; id=IDENT; "}" -> (Some (id_of_string id), CMeasureRec rel) 
+      | "{"; IDENT "wf"; rel=constr; id=OPT IDENT; "}" -> (option_map id_of_string id, CWfRec rel) 
+      | "{"; IDENT "measure"; rel=constr; id=OPT IDENT; "}" -> (option_map id_of_string id, CMeasureRec rel) 
       | ->  (None, CStructRec)
       ] ]
   ;
@@ -304,7 +304,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 c13532cc..2f31c0b6 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: g_xml.ml4 9200 2006-10-03 14:11:08Z herbelin $ *)
+(* $Id: g_xml.ml4 9976 2007-07-12 11:58:30Z msozeau $ *)
 
 open Pp
 open Util
@@ -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 349d5df8..275e179e 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ppconstr.ml 9304 2006-10-28 09:58:16Z herbelin $ *)      
+(* $Id: ppconstr.ml 9976 2007-07-12 11:58:30Z msozeau $ *)      
 
 (*i*)
 open Util
@@ -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 768bc45c..21c851df 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]