Imported Upstream version 8.0pl3+8.1beta.2upstream/8.0pl3+8.1beta.2

10 files changed, 66 insertions, 84 deletions

diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index ec3c2c9c..638a8d65 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: argextend.ml4 8926 2006-06-08 20:23:17Z herbelin $ *)
+(* $Id: argextend.ml4 8976 2006-06-23 10:03:54Z herbelin $ *)
 
 open Genarg
 open Q_util
@@ -176,41 +176,6 @@ let declare_vernac_argument loc s cl =
 
 open Vernacexpr
 open Pcoq
-
-let rec interp_entry_name loc s =
-  let l = String.length s in
-  if l > 8 & String.sub s 0 3 = "ne_" & String.sub s (l-5) 5 = "_list" then
-    let t, g = interp_entry_name loc (String.sub s 3 (l-8)) in
-    List1ArgType t, <:expr< Gramext.Slist1 $g$ >>
-  else if l > 5 & String.sub s (l-5) 5 = "_list" then
-    let t, g = interp_entry_name loc (String.sub s 0 (l-5)) in
-    List0ArgType t, <:expr< Gramext.Slist0 $g$ >>
-  else if l > 4 & String.sub s (l-4) 4 = "_opt" then
-    let t, g = interp_entry_name loc (String.sub s 0 (l-4)) in
-    OptArgType t, <:expr< Gramext.Sopt $g$ >>
-  else 
-    let t, se =
-      if tactic_genarg_level s <> None then
-        Some (ExtraArgType s), <:expr< Tactic. tactic >>
-      else
-      match Pcoq.entry_type (Pcoq.get_univ "prim") s with
-	| Some _ as x -> x, <:expr< Prim. $lid:s$ >>
-	| None -> 
-      match Pcoq.entry_type (Pcoq.get_univ "constr") s with
-	| Some _ as x -> x, <:expr< Constr. $lid:s$ >>
-	| None -> 
-      match Pcoq.entry_type (Pcoq.get_univ "tactic") s with
-	| Some _ as x -> x, <:expr< Tactic. $lid:s$ >>
-	| None -> None, <:expr< $lid:s$ >> in
-    let t =
-      match t with
-	| Some t -> t
-	| None ->
-(*	    Pp.warning_with Pp_control.err_ft
-            ("Unknown primitive grammar entry: "^s);*)
-	    ExtraArgType s
-    in t, <:expr< Gramext.Snterm (Pcoq.Gram.Entry.obj $se$) >>
-
 open Pcaml
 
 EXTEND
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 9ee312ff..a1c0c9ae 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 8875 2006-05-29 19:59:11Z msozeau $ *)
+(* $Id: g_constr.ml4 9043 2006-07-12 10:06:40Z herbelin $ *)
 
 open Pcoq
 open Constr
@@ -244,6 +244,7 @@ GEXTEND Gram
   fixannot:
     [ [ "{"; IDENT "struct"; id=name; "}" -> (Some id, CStructRec)
       | "{"; IDENT "wf"; id=name; rel=lconstr; "}" -> (Some id, CWfRec rel)
+      | "{"; IDENT "measure"; id=name; rel=lconstr; "}" -> (Some id, CMeasureRec rel)
       | ->  (None, CStructRec)
       ] ]
   ;
@@ -273,24 +274,25 @@ GEXTEND Gram
     [ [ OPT"|"; br=LIST0 eqn SEP "|" -> br ] ]
   ;
   eqn:
-    [ [ pl = LIST1 pattern SEP ","; "=>"; rhs = lconstr -> (loc,pl,rhs) ] ]
+    [ [ pll = LIST0 LIST1 pattern LEVEL "99" SEP "," SEP "|"; 
+        "=>"; rhs = lconstr -> (loc,pll,rhs) ] ]
   ;
   pattern:
     [ "200" RIGHTA [ ]
-    | "100" LEFTA
+    | "100" RIGHTA
       [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CPatOr (loc,p::pl) ]
     | "99" RIGHTA [ ]
     | "10" LEFTA
-      [ p = pattern; lp = LIST1 (pattern LEVEL "0") ->
+      [ p = pattern; lp = LIST1 NEXT ->
         (match p with
           | CPatAtom (_, Some r) -> CPatCstr (loc, r, lp)
           | _ -> Util.user_err_loc 
               (cases_pattern_loc p, "compound_pattern",
                Pp.str "Constructor expected"))
       | p = pattern; "as"; id = ident ->
-	  CPatAlias (loc, p, id)
-      | c = pattern; "%"; key=IDENT -> 
-          CPatDelimiters (loc,key,c) ]
+	  CPatAlias (loc, p, id) ]
+    | "1" LEFTA
+      [ c = pattern; "%"; key=IDENT -> CPatDelimiters (loc,key,c) ]
     | "0"
       [ r = Prim.reference -> CPatAtom (loc,Some r)
       | "_" -> CPatAtom (loc,None)
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index eaa51810..c01c23b6 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: g_ltac.ml4 8878 2006-05-30 16:44:25Z herbelin $ *)
+(* $Id: g_ltac.ml4 9037 2006-07-11 12:43:50Z herbelin $ *)
 
 open Pp
 open Util
@@ -134,7 +134,7 @@ GEXTEND Gram
       | "()" -> TacVoid ] ]
   ;
   match_key:
-    [ [ "match" -> false ] ]
+    [ [ "match" -> false | "lazymatch" -> true ] ]
   ;
   input_fun:
     [ [ "_" -> None 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 7405ae54..a72ced97 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 8929 2006-06-08 22:35:58Z herbelin $ *)
+(* $Id: g_vernac.ml4 9017 2006-07-05 17:27:34Z herbelin $ *)
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
 open Pp
@@ -237,6 +237,7 @@ GEXTEND Gram
   rec_annotation:
     [ [ "{"; IDENT "struct"; id=IDENT; "}" -> (Some (id_of_string id), CStructRec)
       | "{"; IDENT "wf"; id=IDENT; rel=lconstr; "}" -> (Some (id_of_string id), CWfRec rel) 
+      | "{"; IDENT "measure"; id=IDENT; rel=lconstr; "}" -> (Some (id_of_string id), CMeasureRec rel) 
       | ->  (None, CStructRec)
       ] ]
   ;
@@ -651,8 +652,11 @@ GEXTEND Gram
 	  VernacBacktrack (n,m,p)
 
 (* Tactic Debugger *)
-      |	IDENT "Debug"; IDENT "On" -> VernacDebug true
-      |	IDENT "Debug"; IDENT "Off" -> VernacDebug false
+      |	IDENT "Debug"; IDENT "On" -> 
+          VernacSetOption (SecondaryTable ("Ltac","Debug"), BoolValue true)
+
+      |	IDENT "Debug"; IDENT "Off" ->
+          VernacSetOption (SecondaryTable ("Ltac","Debug"), BoolValue false)
 
  ] ];
     END
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 5ad0193b..a89fffa0 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 8875 2006-05-29 19:59:11Z msozeau $ *)
+(* $Id: g_xml.ml4 9016 2006-07-05 17:19:39Z herbelin $ *)
 
 open Pp
 open Util
@@ -228,6 +228,10 @@ and interp_xml_recursionOrder x =
 	  (match l with
 	       [c] -> RWfRec (interp_xml_type c)
 	     | _ -> user_err_loc (loc, "", str "wrong number of arguments (expected one)"))
+      | "Measure" -> 
+	  (match l with
+	       [c] -> RMeasureRec (interp_xml_type c)
+	     | _ -> user_err_loc (loc, "", str "wrong number of arguments (expected one)"))
       | _ ->
           user_err_loc (locs,"",str "invalid recursion order")
 
@@ -252,22 +256,12 @@ and interp_xml_CoFixFunction x =
 
 (* Interpreting tactic argument *)
 
-let rec (interp_xml_tactic_expr : xml -> glob_tactic_expr) = function
-  | XmlTag (loc,"TACARG",[],[x]) ->
-      TacArg (interp_xml_tactic_arg x)
-  | _ -> error "Ill-formed xml tree"
-
-and interp_xml_tactic_arg = function
+let rec interp_xml_tactic_arg = function
   | XmlTag (loc,"TERM",[],[x]) ->
       ConstrMayEval (ConstrTerm (interp_xml_constr x,None))
   | XmlTag (loc,"CALL",al,xl) ->
       let ltacref = ltacref_of_cdata (get_xml_attr "uri" al) in
       TacCall(loc,ArgArg ltacref,List.map interp_xml_tactic_arg xl)
-(*
-  | XmlTag (loc,"TACTIC",[],[x]) ->
-      Tacexp (interp_xml_tactic_expr x)
-  | _ -> error "Ill-formed xml tree"
-*)
   | XmlTag (loc,s,_,_) -> user_err_loc (loc,"", str "Unexpected tag " ++ str s)
 
 let parse_tactic_arg ch =
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index c02dc59b..80eaf7f0 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: lexer.ml4 8924 2006-06-08 17:49:01Z notin $ i*)
+(*i $Id: lexer.ml4 9015 2006-07-05 17:19:22Z herbelin $ i*)
 
 open Pp
 open Token
@@ -146,12 +146,14 @@ let lookup_utf8_tail c cs =
     (* utf-8 what do to with diacritics U0483-U0489 \ U0487 ? *)
     (* utf-8 Cyrillic letters U048A-U4F9 (Warning: 04CF) *)
     | x when 0x048A <= x & x <= 0x04F9 -> Utf8Letter n
-    (* utf-8 Cyrillic supplements letters U0500-U050F *)
+    (* utf-8 Cyrillic supplement letters U0500-U050F *)
     | x when 0x0500 <= x & x <= 0x050F -> Utf8Letter n
     (* utf-8 Hebrew letters U05D0-05EA *)
     | x when 0x05D0 <= x & x <= 0x05EA -> Utf8Letter n
-    (* utf-8 Hebrew letters U0621-064A *)
+    (* utf-8 Arabic letters U0621-064A *)
     | x when 0x0621 <= x & x <= 0x064A -> Utf8Letter n
+    (* utf-8 Arabic supplement letters U0750-076D *)
+    | x when 0x0750 <= x & x <= 0x076D -> Utf8Letter n
     | _ -> error_unsupported_unicode_character n cs
     end
     | 0x1000 ->
@@ -589,9 +591,10 @@ let is_ident_not_keyword s =
     | _ -> false
 
 let is_number s =
-  match s.[0] with
-    | '0'..'9' -> true
-    | _ -> false
+  let rec aux i =
+    String.length s = i or 
+    match s.[i] with '0'..'9' -> aux (i+1) | _ -> false
+  in aux 0
 
 let strip s =
   let len =
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 127a911f..56e434fb 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pcoq.ml4 8926 2006-06-08 20:23:17Z herbelin $ i*)
+(*i $Id: pcoq.ml4 9043 2006-07-12 10:06:40Z herbelin $ i*)
 
 open Pp
 open Util
@@ -484,7 +484,11 @@ let default_levels =
    0,Gramext.RightA]
 
 let default_pattern_levels =
-  [10,Gramext.LeftA;
+  [200,Gramext.RightA;
+   100,Gramext.RightA;
+   99,Gramext.RightA;
+   10,Gramext.LeftA;
+   1,Gramext.LeftA;
    0,Gramext.RightA]
 
 let level_stack = 
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index d55a6c1e..a1ca386e 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ppconstr.ml 8878 2006-05-30 16:44:25Z herbelin $ *)      
+(* $Id: ppconstr.ml 8997 2006-07-03 16:40:20Z herbelin $ *)      
 
 (*i*)
 open Util
@@ -186,12 +186,12 @@ let rec pr_patt sep inh p =
 
 let pr_patt = pr_patt mt
 
-
 let pr_eqn pr (loc,pl,rhs) =
   spc() ++ hov 4
     (pr_with_comments loc
       (str "| " ++
-      hov 0 (prlist_with_sep sep_v (pr_patt ltop) pl ++ str " =>") ++
+      hov 0 (prlist_with_sep pr_bar (prlist_with_sep sep_v (pr_patt ltop)) pl 
+             ++ str " =>") ++
       pr_sep_com spc (pr ltop) rhs))
 
 let begin_of_binder = function
@@ -384,6 +384,8 @@ let pr_fixdecl pr prd dangling_with_for (id,(n,ro),bl,t,c) =
 	    else mt() 
 	| CWfRec c ->
 	    spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}"
+	| CMeasureRec c ->
+	    spc () ++ str "{measure " ++ pr lsimple c ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}"
   in
     pr_recursive_decl pr prd dangling_with_for id bl annot t c
 
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index aea44604..7e3c853d 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ppvernac.ml 8831 2006-05-19 09:29:54Z herbelin $ *)  
+(* $Id: ppvernac.ml 9020 2006-07-05 17:35:23Z herbelin $ *)  
 
 open Pp
 open Names
@@ -414,7 +414,6 @@ let rec pr_vernac = function
 	| ExplainTree l -> str"Explain Proof Tree" ++ spc() ++ prlist_with_sep sep int l 
       in pr_showable s
   | VernacCheckGuard -> str"Guarded"
-  | VernacDebug b -> pr_topcmd b
 
   (* Resetting *)
   | VernacResetName id -> str"Reset" ++ spc() ++ pr_lident id
@@ -572,6 +571,9 @@ let rec pr_vernac = function
 		      | CWfRec c -> 
 			  spc() ++ str "{wf " ++ pr_name name ++ spc() ++ 
 			    pr_lconstr_expr c ++ str"}"
+		      | CMeasureRec c -> 
+			  spc() ++ str "{measure " ++ pr_name name ++ spc() ++ 
+			    pr_lconstr_expr c ++ str"}"
 	    in
             pr_id id ++ pr_binders_arg bl ++ annot ++ spc()
             ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4
index 07b23972..61a552f3 100644
--- a/parsing/q_util.ml4
+++ b/parsing/q_util.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: q_util.ml4 7732 2005-12-26 13:51:24Z herbelin $ *)
+(* $Id: q_util.ml4 8982 2006-06-23 13:17:49Z herbelin $ *)
 
 (* This file defines standard combinators to build ml expressions *)
 
@@ -84,21 +84,27 @@ let rec interp_entry_name loc s =
     OptArgType t, <:expr< Gramext.Sopt $g$ >>
   else
     let s = if s = "hyp" then "var" else s in
-    let t, se =
+    let t, se, lev =
+      match tactic_genarg_level s with
+	| Some n -> Some (ExtraArgType s), <:expr< Tactic. tactic_expr >>, Some n
+	| None ->
       match Pcoq.entry_type (Pcoq.get_univ "prim") s with
-	| Some _ as x -> x, <:expr< Prim. $lid:s$ >>
+	| Some _ as x -> x, <:expr< Prim. $lid:s$ >>, None
 	| None -> 
       match Pcoq.entry_type (Pcoq.get_univ "constr") s with
-	| Some _ as x -> x, <:expr< Constr. $lid:s$ >>
+	| Some _ as x -> x, <:expr< Constr. $lid:s$ >>, None
 	| None -> 
       match Pcoq.entry_type (Pcoq.get_univ "tactic") s with
-	| Some _ as x -> x, <:expr< Tactic. $lid:s$ >>
-	| None -> None, <:expr< $lid:s$ >> in
+	| Some _ as x -> x, <:expr< Tactic. $lid:s$ >>, None
+	| None -> None, <:expr< $lid:s$ >>, None in
     let t =
       match t with
 	| Some t -> t
-	| None ->
-(*	    Pp.warning_with Pp_control.err_ft
-            ("Unknown primitive grammar entry: "^s);*)
-	    ExtraArgType s
-    in t, <:expr< Gramext.Snterm (Pcoq.Gram.Entry.obj $se$) >>
+	| None -> ExtraArgType s in
+    let entry = match lev with
+      | Some n ->
+	  let s = string_of_int n in
+	  <:expr< Gramext.Snterml (Pcoq.Gram.Entry.obj $se$, $str:s$) >>
+      | None -> 
+	  <:expr< Gramext.Snterm (Pcoq.Gram.Entry.obj $se$) >>
+    in t, entry