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

12 files changed, 73 insertions, 36 deletions

diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 12c0ea1d..2731fc90 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -6,13 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: argextend.ml4 9265 2006-10-24 08:35:38Z herbelin $ *)
+(* $Id: argextend.ml4 10185 2007-10-06 18:05:13Z herbelin $ *)
 
 open Genarg
 open Q_util
 open Q_coqast
 
-let join_loc (deb1,_) (_,fin2) = (deb1,fin2)
+let join_loc = Util.join_loc
 let loc = Util.dummy_loc
 let default_loc = <:expr< Util.dummy_loc >>
 
@@ -226,7 +226,7 @@ EXTEND
         let t, g = interp_entry_name loc e sep in (g, Some (s,t))
       | s = STRING ->
 	  if String.length s > 0 && Util.is_letter s.[0] then
-	    Pcoq.lexer.Token.using ("", s);
+	    Compat.using Pcoq.lexer ("", s);
         (<:expr< (Gramext.Stoken (Lexer.terminal $str:s$)) >>, None)
     ] ]
   ;
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index 5dda69ba..4216899b 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: egrammar.mli 9147 2006-09-15 21:49:56Z herbelin $ i*)
+(*i $Id: egrammar.mli 10185 2007-10-06 18:05:13Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -45,7 +45,7 @@ val extend_grammar : all_grammar_command -> unit
 type grammar_tactic_production =
   | TacTerm of string
   | TacNonTerm of
-      loc * (Token.t Gramext.g_symbol * Genarg.argument_type) * string option
+      loc * (Compat.token Gramext.g_symbol * Genarg.argument_type) * string option
 
 val extend_tactic_grammar :
   string -> grammar_tactic_production list list -> unit
@@ -61,7 +61,7 @@ val get_extend_vernac_grammars :
 (*
 val reset_extend_grammars_v8 : unit -> unit
 *)
-val interp_entry_name : int -> string -> entry_type * Token.t Gramext.g_symbol
+val interp_entry_name : int -> string -> entry_type * Compat.token Gramext.g_symbol
 
 val recover_notation_grammar :
   notation -> (precedence * tolerability list) -> notation_grammar
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 6a9388b2..cdd484e7 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 9977 2007-07-12 12:18:46Z msozeau $ *)
+(* $Id: g_vernac.ml4 10067 2007-08-09 17:13:16Z msozeau $ *)
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
 open Pp
@@ -143,7 +143,9 @@ GEXTEND Gram
           VernacFixpoint (recs,Options.boxed_definitions())
       | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
           VernacCoFixpoint (corecs,false)
-      | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l ] ]
+      | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l
+      | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from"; 
+	l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) ] ]
   ;
   gallina_ext:
     [ [ b = record_token; oc = opt_coercion; name = identref;
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 2f31c0b6..ce284454 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 9976 2007-07-12 11:58:30Z msozeau $ *)
+(* $Id: g_xml.ml4 10090 2007-08-24 10:53:53Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index f7adfdd8..bf3cb084 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 9333 2006-11-02 13:59:14Z barras $ i*)
+(*i $Id: pcoq.ml4 10185 2007-10-06 18:05:13Z herbelin $ i*)
 
 open Pp
 open Util
@@ -29,6 +29,29 @@ open Ppextend
    we unfreeze the state of the lexer. This restores the behaviour of the
    lexer. B.B. *)
 
+IFDEF CAMLP5 THEN 
+
+let lexer = {
+  Token.tok_func = Lexer.func;
+  Token.tok_using = Lexer.add_token;
+  Token.tok_removing = (fun _ -> ());
+  Token.tok_match = Token.default_match;
+  (* Token.parse = Lexer.tparse; *)
+  Token.tok_comm = None;
+  Token.tok_text = Lexer.token_text }
+
+module L =
+  struct
+    type te = string * string
+    let lexer = lexer
+  end
+
+(* The parser of Coq *)
+
+module G = Grammar.GMake(L)
+
+ELSE 
+
 let lexer = {
   Token.func = Lexer.func;
   Token.using = Lexer.add_token;
@@ -45,6 +68,8 @@ module L =
 
 module G = Grammar.Make(L)
 
+END
+
 let grammar_delete e rls =
   List.iter
     (fun (_,_,lev) ->
@@ -95,7 +120,7 @@ type ext_kind =
   | ByGrammar of
       grammar_object G.Entry.e * Gramext.position option *
       (string option * Gramext.g_assoc option *
-       (Token.t Gramext.g_symbol list * Gramext.g_action) list) list
+       (Compat.token Gramext.g_symbol list * Gramext.g_action) list) list
   | ByGEXTEND of (unit -> unit) * (unit -> unit)
 
 let camlp4_state = ref []
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 1fe8c122..681a6b2c 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pcoq.mli 9333 2006-11-02 13:59:14Z barras $ i*)
+(*i $Id: pcoq.mli 10185 2007-10-06 18:05:13Z herbelin $ i*)
 
 open Util
 open Names
@@ -20,9 +20,9 @@ open Libnames
 
 (* The lexer and parser of Coq. *)
 
-val lexer : Token.lexer
+val lexer : Compat.lexer
 
-module Gram : Grammar.S with type te = Token.t
+module Gram : Grammar.S with type te = Compat.token
 
 (* The superclass of all grammar entries *)
 type grammar_object
@@ -42,7 +42,7 @@ val get_constr_entry :
 val grammar_extend :
   grammar_object Gram.Entry.e -> Gramext.position option ->
     (string option * Gramext.g_assoc option *
-     (Token.t Gramext.g_symbol list * Gramext.g_action) list) list
+     (Compat.token Gramext.g_symbol list * Gramext.g_action) list) list
     -> unit
 
 val remove_grammars : int -> unit
@@ -210,7 +210,7 @@ module Vernac_ :
 (* Binding entry names to campl4 entries *)
 
 val symbol_of_production : Gramext.g_assoc option -> constr_entry ->
-  bool -> constr_production_entry -> Token.t Gramext.g_symbol
+  bool -> constr_production_entry -> Compat.token Gramext.g_symbol
 
 (* Registering/resetting the level of an entry *)
 
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 275e179e..92c6715e 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ppconstr.ml 9976 2007-07-12 11:58:30Z msozeau $ *)      
+(* $Id: ppconstr.ml 10087 2007-08-24 10:39:30Z herbelin $ *)      
 
 (*i*)
 open Util
@@ -95,9 +95,9 @@ let pr_patnotation = pr_notation_gen decode_patlist_value
 let pr_delimiters key strm =
   strm ++ str ("%"^key)
 
-let pr_located pr ((b,e),x) =
-  if Options.do_translate() && (b,e)<>dummy_loc then
-    let (b,e) = unloc (b,e) in
+let pr_located pr (loc,x) =
+  if Options.do_translate() && loc<>dummy_loc then
+    let (b,e) = unloc loc in
     comment b ++ pr x ++ comment e
   else pr x
 
@@ -142,7 +142,7 @@ let pr_opt_type_spc pr = function
   | CHole _ -> mt ()
   | t ->  str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
 
-let pr_lident (b,_ as loc,id) =
+let pr_lident (loc,id) =
   if loc <> dummy_loc then
     let (b,_) = unloc loc in
     pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id)
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index f9b8c425..77f0d5cb 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ppvernac.ml 9562 2007-01-31 09:00:36Z msozeau $ *)  
+(* $Id: ppvernac.ml 10087 2007-08-24 10:39:30Z herbelin $ *)  
 
 open Pp
 open Names
@@ -28,7 +28,7 @@ open Tacinterp
 
 let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr
 
-let pr_lident (b,_ as loc,id) =
+let pr_lident (loc,id) =
   if loc <> dummy_loc then
     let (b,_) = unloc loc in
     pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id)
@@ -39,7 +39,7 @@ let string_of_fqid fqid =
 
 let pr_fqid fqid = str (string_of_fqid fqid)
 
-let pr_lfqid (_,_ as loc,fqid) =
+let pr_lfqid (loc,fqid) =
   if loc <> dummy_loc then
    let (b,_) = unloc loc in
     pr_located pr_fqid (make_loc (b,b+String.length(string_of_fqid fqid)),fqid)
@@ -602,6 +602,11 @@ let rec pr_vernac = function
   | VernacScheme l ->
       hov 2 (str"Scheme" ++ spc() ++
              prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onescheme l)
+  | VernacCombinedScheme (id, l) ->
+      hov 2 (str"Combined Scheme" ++ spc() ++
+	       pr_lident id ++ spc() ++ str"from" ++ spc() ++
+	       prlist_with_sep (fun _ -> fnl() ++ str", ") pr_lident l)
+	
 
   (* Gallina extensions *)
   | VernacRecord (b,(oc,name),ps,s,c,fs) ->
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 23787f4c..9f828c96 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: q_coqast.ml4 9551 2007-01-29 15:13:35Z bgregoir $ *)
+(* $Id: q_coqast.ml4 10185 2007-10-06 18:05:13Z herbelin $ *)
 
 open Util
 open Names
@@ -19,13 +19,18 @@ let purge_str s =
   if String.length s == 0 || s.[0] <> '$' then s
   else String.sub s 1 (String.length s - 1)
 
+IFDEF OCAML308 THEN DEFINE NOP END
+IFDEF OCAML309 THEN DEFINE NOP END
+IFDEF CAMLP5 THEN DEFINE NOP END
+
 let anti loc x =
   let e =
     let loc =
-      ifdef OCAML_308 then
+      IFDEF NOP THEN 
         loc
-      else
-        (1, snd loc - fst loc)
+      ELSE 
+	(1, snd loc - fst loc)
+      END 
     in <:expr< $lid:purge_str x$ >>
   in
   <:expr< $anti:e$ >>
diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4
index 2ef56907..552c144a 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 9333 2006-11-02 13:59:14Z barras $ *)
+(* $Id: q_util.ml4 10087 2007-08-24 10:39:30Z herbelin $ *)
 
 (* This file defines standard combinators to build ml expressions *)
 
@@ -37,18 +37,18 @@ let mlexpr_of_list f l =
   List.fold_right
     (fun e1 e2 ->
       let e1 = f e1 in
-       let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e2)) in
+       let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
        <:expr< [$e1$ :: $e2$] >>)
     l (let loc = dummy_loc in <:expr< [] >>)
 
 let mlexpr_of_pair m1 m2 (a1,a2) =
   let e1 = m1 a1 and e2 = m2 a2 in
-  let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e2)) in
+  let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
   <:expr< ($e1$, $e2$) >>
 
 let mlexpr_of_triple m1 m2 m3 (a1,a2,a3)=
   let e1 = m1 a1 and e2 = m2 a2 and e3 = m3 a3 in
-  let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e3)) in
+  let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e3) in
   <:expr< ($e1$, $e2$, $e3$) >>
 
 (* We don't give location for tactic quotation! *)
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 73d41465..2dfe489e 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -6,14 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacextend.ml4 9265 2006-10-24 08:35:38Z herbelin $ *)
+(* $Id: tacextend.ml4 10089 2007-08-24 10:49:43Z herbelin $ *)
 
+open Util
 open Genarg
 open Q_util
 open Q_coqast
 open Argextend
 
-let join_loc (deb1,_) (_,fin2) = (deb1,fin2)
 let loc = Util.dummy_loc
 let default_loc = <:expr< Util.dummy_loc >>
 
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index 7cf542fe..4847f385 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -6,14 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: vernacextend.ml4 9265 2006-10-24 08:35:38Z herbelin $ *)
+(* $Id: vernacextend.ml4 10089 2007-08-24 10:49:43Z herbelin $ *)
 
+open Util
 open Genarg
 open Q_util
 open Q_coqast
 open Argextend
 
-let join_loc (deb1,_) (_,fin2) = (deb1,fin2)
 let loc = Util.dummy_loc
 let default_loc = <:expr< Util.dummy_loc >>