Imported Upstream version 8.2pl2+dfsgupstream/8.2.pl2+dfsg

5 files changed, 28 insertions, 19 deletions

diff --git a/parsing/g_decl_mode.ml4 b/parsing/g_decl_mode.ml4
index 61c3474d..35fc064b 100644
--- a/parsing/g_decl_mode.ml4
+++ b/parsing/g_decl_mode.ml4
@@ -9,7 +9,7 @@
 (*i camlp4deps: "parsing/grammar.cma" i*)
 (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
 
-(* $Id: g_decl_mode.ml4 10739 2008-04-01 14:45:20Z herbelin $ *)
+(* $Id: g_decl_mode.ml4 12414 2009-10-25 18:50:41Z corbinea $ *)
 
 
 open Decl_expr
@@ -220,7 +220,7 @@ GLOBAL: proof_instr;
   intro_step:
     [[ IDENT "suppose" ; h=assume_clause -> Psuppose h
      | IDENT "suppose" ; IDENT "it"; IDENT "is" ; c=pattern LEVEL "0" ;
-       po=OPT[ IDENT "with"; p=LIST1 hyp -> p ] ; 
+       po=OPT[ "with"; p=LIST1 hyp SEP ","-> p  ] ; 
        ho=OPT[ IDENT "and" ; h=suppose_clause -> h ] -> 
 	 Pcase (none_is_empty po,c,none_is_empty ho)
      | "let" ; v=let_vars -> Plet v	 
diff --git a/parsing/g_intsyntax.ml b/parsing/g_intsyntax.ml
index a589ccf1..64fa0b49 100644
--- a/parsing/g_intsyntax.ml
+++ b/parsing/g_intsyntax.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: g_intsyntax.ml 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: g_intsyntax.ml 12509 2009-11-12 15:52:50Z letouzey $ i*)
 
 (* digit-based syntax for int31, bigN bigZ and bigQ *)
 
@@ -92,13 +92,15 @@ let bigZ_neg = ConstructRef ((bigZ_id "t_",0),2)
 
 (*bigQ stuff*)
 let bigQ_module = ["Coq"; "Numbers"; "Rational"; "BigQ"; "BigQ"]
-let qmake_module = ["Coq"; "Numbers"; "Rational"; "BigQ"; "QMake_base"]
+let qmake_module = ["Coq"; "Numbers"; "Rational"; "BigQ"; "QMake"]
 let bigQ_path = make_path (bigQ_module@["BigQ"]) "t"
 (* big ugly hack bis *)
-let bigQ_id = make_kn qmake_module
+let bigQ_id id = (Obj.magic ((Names.MPdot ((Names.MPfile (make_dir bigQ_module)), 
+                             Names.mk_label "BigQ")),
+              [], Names.id_of_string id) : Names.kernel_name)
 let bigQ_scope = "bigQ_scope"
 
-let bigQ_z =  ConstructRef ((bigQ_id "q_type",0),1)
+let bigQ_z =  ConstructRef ((bigQ_id "t_",0),1)
 
 
 (*** Definition of the Non_closed exception, used in the pretty printing ***)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index b2d67e1c..f727dfea 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -9,7 +9,7 @@
 (*i camlp4deps: "parsing/grammar.cma" i*)
 (*i camlp4use: "pa_extend.cmo" i*)
 
-(* $Id: g_vernac.ml4 12187 2009-06-13 19:36:59Z msozeau $ *)
+(* $Id: g_vernac.ml4 13197 2010-06-25 22:36:17Z letouzey $ *)
 
 
 open Pp
@@ -663,6 +663,8 @@ GEXTEND Gram
   check_command: (* TODO: rapprocher Eval et Check *)
     [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = lconstr ->
           fun g -> VernacCheckMayEval (Some r, g, c)
+      | IDENT "Compute"; c = lconstr ->
+	  fun g -> VernacCheckMayEval (Some Rawterm.CbvVm, g, c)
       | IDENT "Check"; c = lconstr ->
 	  fun g -> VernacCheckMayEval (None, g, c) ] ]
   ;
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 2633386f..52b5ede7 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 11786 2009-01-14 13:07:34Z herbelin $ i*)
+(*i $Id: lexer.ml4 12891 2010-03-30 11:40:02Z herbelin $ i*)
 
 
 (*i camlp4use: "pr_o.cmo" i*) 
@@ -91,6 +91,14 @@ let error_utf8 cs =
   Stream.junk cs; (* consume the char to avoid read it and fail again *)
   err (bp, bp+1) Illegal_character
 
+let utf8_char_size cs = function
+  (* Utf8 leading byte *)
+  | '\x00'..'\x7F' -> 1
+  | '\xC0'..'\xDF' -> 2
+  | '\xE0'..'\xEF' -> 3
+  | '\xF0'..'\xF7' -> 4
+  | _ (* '\x80'..\xBF'|'\xF8'..'\xFF' *) -> error_utf8 cs
+
 let njunk n = Util.repeat n Stream.junk
 
 let check_utf8_trailing_byte cs c =
@@ -355,14 +363,8 @@ and progress_utf8 last nj n c tt cs =
   with Not_found ->
     last
 
-and progress_from_byte last nj tt cs = function
-  (* Utf8 leading byte *)
-  | '\x00'..'\x7F' as c -> progress_utf8 last nj 1 c tt cs
-  | '\xC0'..'\xDF' as c -> progress_utf8 last nj 2 c tt cs
-  | '\xE0'..'\xEF' as c -> progress_utf8 last nj 3 c tt cs
-  | '\xF0'..'\xF7' as c -> progress_utf8 last nj 4 c tt cs
-  | _ (* '\x80'..\xBF'|'\xF8'..'\xFF' *) ->
-      error_utf8 cs
+and progress_from_byte last nj tt cs c =
+  progress_utf8 last nj (utf8_char_size cs c) c tt cs
 
 (* Must be a special token *)
 let process_chars bp c cs =
@@ -370,7 +372,10 @@ let process_chars bp c cs =
   let ep = Stream.count cs in
   match t with
     | Some t -> (("", t), (bp, ep))
-    | None -> err (bp, ep) Undefined_token
+    | None ->
+	let ep' = bp + utf8_char_size cs c in
+	njunk (ep' - ep) cs;
+	err (bp, ep') Undefined_token
 
 let parse_after_dollar bp =
   parser
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 3b433498..f52ebc76 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pptactic.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
+(* $Id: pptactic.ml 12581 2009-12-13 15:02:33Z herbelin $ *)
 
 open Pp
 open Names
@@ -378,7 +378,7 @@ let pr_as_ipat = function
 
 let pr_as_name = function
   | Anonymous -> mt ()
-  | Name id -> str "as " ++ pr_lident (dummy_loc,id)
+  | Name id -> str " as " ++ pr_lident (dummy_loc,id)
 
 let pr_pose_as_style prc na c =
   spc() ++ prc c ++ pr_as_name na