Imported Upstream version 8.0pl2upstream/8.0pl2

23 files changed, 122 insertions, 78 deletions

diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 5fa781ad..e6d9f99d 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: argextend.ml4,v 1.9.2.2 2004/07/16 19:30:37 herbelin Exp $ *)
+(* $Id: argextend.ml4,v 1.9.2.4 2005/01/15 14:56:53 herbelin Exp $ *)
 
 open Genarg
 open Q_util
@@ -33,6 +33,7 @@ let rec make_rawwit loc = function
   | QuantHypArgType -> <:expr< Genarg.rawwit_quant_hyp >>
   | TacticArgType -> <:expr< Genarg.rawwit_tactic >>
   | RedExprArgType -> <:expr< Genarg.rawwit_red_expr >>
+  | OpenConstrArgType -> <:expr< Genarg.rawwit_open_constr >>
   | CastedOpenConstrArgType -> <:expr< Genarg.rawwit_casted_open_constr >>
   | ConstrWithBindingsArgType -> <:expr< Genarg.rawwit_constr_with_bindings >>
   | BindingsArgType -> <:expr< Genarg.rawwit_bindings >>
@@ -59,6 +60,7 @@ let rec make_globwit loc = function
   | ConstrMayEvalArgType -> <:expr< Genarg.globwit_constr_may_eval >>
   | TacticArgType -> <:expr< Genarg.globwit_tactic >>
   | RedExprArgType -> <:expr< Genarg.globwit_red_expr >>
+  | OpenConstrArgType -> <:expr< Genarg.globwit_open_constr >>
   | CastedOpenConstrArgType -> <:expr< Genarg.globwit_casted_open_constr >>
   | ConstrWithBindingsArgType -> <:expr< Genarg.globwit_constr_with_bindings >>
   | BindingsArgType -> <:expr< Genarg.globwit_bindings >>
@@ -85,6 +87,7 @@ let rec make_wit loc = function
   | ConstrMayEvalArgType -> <:expr< Genarg.wit_constr_may_eval >>
   | TacticArgType -> <:expr< Genarg.wit_tactic >>
   | RedExprArgType -> <:expr< Genarg.wit_red_expr >>
+  | OpenConstrArgType -> <:expr< Genarg.wit_open_constr >>
   | CastedOpenConstrArgType -> <:expr< Genarg.wit_casted_open_constr >>
   | ConstrWithBindingsArgType -> <:expr< Genarg.wit_constr_with_bindings >>
   | BindingsArgType -> <:expr< Genarg.wit_bindings >>
@@ -267,11 +270,14 @@ EXTEND
          declare_vernac_argument false loc s l ] ]
   ;
   argtype:
-    [ [ e = LIDENT -> fst (interp_entry_name loc e) 
-      | e1 = LIDENT; "*"; e2 = LIDENT ->
-          let e1 = fst (interp_entry_name loc e1) in
-          let e2 = fst (interp_entry_name loc e2) in
-          PairArgType (e1, e2) ] ]
+    [ "2" RIGHTA
+      [ e1 = argtype; "*"; e2 = NEXT -> PairArgType (e1, e2) ]
+    | "1"
+      [ e = argtype; LIDENT "list" -> List0ArgType e
+      | e = argtype; LIDENT "option" -> OptArgType e ]
+    | "0"
+      [ e = LIDENT -> fst (interp_entry_name loc e) 
+      | "("; e = argtype; ")" -> e ] ]
   ;
   argrule:
     [ [ "["; l = LIST0 genarg; "]"; "->"; "["; e = Pcaml.expr; "]" -> (l,e) ] ]
@@ -286,4 +292,3 @@ EXTEND
     ] ]
   ;
   END
-
diff --git a/parsing/coqast.mli b/parsing/coqast.mli
index 546725c0..0b1138f2 100644
--- a/parsing/coqast.mli
+++ b/parsing/coqast.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: coqast.mli,v 1.10.6.1 2004/07/16 19:30:37 herbelin Exp $ i*)
+(*i $Id: coqast.mli,v 1.10.6.2 2005/01/21 16:42:36 herbelin Exp $ i*)
 
 (*i*)
 open Util
@@ -43,9 +43,9 @@ val hcons_ast:
 
 val subst_ast: Names.substitution -> t -> t
 
-(*
+(*i
 val map_tactic_expr : (t -> t) -> (tactic_expr -> tactic_expr) -> tactic_expr -> tactic_expr
 val fold_tactic_expr :
   ('a -> t -> 'a) -> ('a -> tactic_expr -> 'a) -> 'a -> tactic_expr -> 'a
 val iter_tactic_expr : (tactic_expr -> unit) -> tactic_expr -> unit
-*)
+i*)
diff --git a/parsing/doc.tex b/parsing/doc.tex
new file mode 100644
index 00000000..68ab601c
--- /dev/null
+++ b/parsing/doc.tex
@@ -0,0 +1,9 @@
+
+\newpage
+\section*{The Coq parsers and printers}
+
+\ocwsection \label{parsing}
+This chapter describes the implementation of the \Coq\ parsers and printers.
+
+\bigskip
+\begin{center}\epsfig{file=parsing.dep.ps}\end{center}
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 9886bbf1..7a151c1a 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -6,10 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: egrammar.ml,v 1.48.2.1 2004/07/16 19:30:37 herbelin Exp $ *)
+(* $Id: egrammar.ml,v 1.48.2.3 2004/11/26 19:37:59 herbelin Exp $ *)
 
 open Pp
 open Util
+open Ppextend
 open Extend
 open Pcoq
 open Topconstr
@@ -20,10 +21,11 @@ open Nameops
 
 (* State of the grammar extensions *)
 
+type notation_grammar = 
+    int * Gramext.g_assoc option * notation * prod_item list * int list option
+
 type all_grammar_command =
-  | Notation of
-      (int * Gramext.g_assoc option * notation * prod_item list *
-      int list option)
+  | Notation of (precedence * tolerability list) * notation_grammar
   | Grammar of grammar_command
   | TacticGrammar of
       (string * (string * grammar_production list) * 
@@ -415,7 +417,7 @@ let add_tactic_entries gl =
 
 let extend_grammar gram =
   (match gram with
-  | Notation a -> extend_constr_notation a
+  | Notation (_,a) -> extend_constr_notation a
   | Grammar g -> extend_grammar_rules g
   | TacticGrammar l -> add_tactic_entries l);
   grammar_state := gram :: !grammar_state
@@ -428,6 +430,12 @@ let reset_extend_grammars_v8 () =
   List.iter (fun (s,gl) -> extend_tactic_grammar s gl) te;
   List.iter (fun (s,gl) -> extend_vernac_command_grammar s gl) tv
 
+let recover_notation_grammar ntn prec =
+  let l = map_succeed (function
+    | Notation (prec',(_,_,ntn',_,_ as x)) when prec = prec' & ntn = ntn' -> x
+    | _ -> failwith "") !grammar_state in
+  assert (List.length l = 1);
+  List.hd l
 
 (* Summary functions: the state of the lexer is included in that of the parser.
    Because the grammar affects the set of keywords when adding or removing
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index c601c5fc..0009b4b6 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,v 1.14.2.2 2004/07/16 19:30:37 herbelin Exp $ i*)
+(*i $Id: egrammar.mli,v 1.14.2.5 2004/11/27 09:25:44 herbelin Exp $ i*)
 
 (*i*)
 open Util
@@ -14,14 +14,16 @@ open Topconstr
 open Ast
 open Coqast
 open Vernacexpr
+open Ppextend
 open Extend
 open Rawterm
 (*i*)
 
+type notation_grammar = 
+    int * Gramext.g_assoc option * notation * prod_item list * int list option
+
 type all_grammar_command =
-  | Notation of
-      (int * Gramext.g_assoc option * notation * prod_item list *
-      int list option)
+  | Notation of (precedence * tolerability list) * notation_grammar
   | Grammar of grammar_command
   | TacticGrammar of
       (string * (string * grammar_production list) * 
@@ -52,3 +54,6 @@ val subst_all_grammar_command :
 
 val interp_entry_name : string -> string -> 
   entry_type * Token.t Gramext.g_symbol
+
+val recover_notation_grammar :
+  notation -> (precedence * tolerability list) -> notation_grammar
diff --git a/parsing/esyntax.mli b/parsing/esyntax.mli
index e05e1ca4..88d1a0e2 100644
--- a/parsing/esyntax.mli
+++ b/parsing/esyntax.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: esyntax.mli,v 1.10.2.1 2004/07/16 19:30:37 herbelin Exp $ i*)
+(*i $Id: esyntax.mli,v 1.10.2.2 2005/01/21 16:42:36 herbelin Exp $ i*)
 
 (*i*)
 open Pp
@@ -48,16 +48,14 @@ module Ppprim :
 val declare_primitive_printer : 
   string -> scope_name -> primitive_printer -> unit
 
-(*
+(*i
 val declare_infix_symbol : Libnames.section_path -> string -> unit
-*)
+i*)
 
 (* Generic printing functions *) 
-(*
+(*i
 val token_printer: std_printer -> std_printer
-*)
-(*
 val print_syntax_entry : 
   string -> unparsing_subfunction -> Ast.env -> Ast.astpat syntax_entry -> std_ppcmds
-*)
+i*)
 val genprint : std_printer -> unparsing_subfunction
diff --git a/parsing/extend.mli b/parsing/extend.mli
index 761d0e04..c5417649 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extend.mli,v 1.19.2.1 2004/07/16 19:30:37 herbelin Exp $ i*)
+(*i $Id: extend.mli,v 1.19.2.2 2005/01/21 16:42:37 herbelin Exp $ i*)
 
 (*i*)
 open Pp
@@ -112,10 +112,11 @@ type 'pat unparsing_hunk =
   | UNP_FNL
   | UNP_SYMBOLIC of string option * string * 'pat unparsing_hunk
 
-(*val subst_unparsing_hunk : 
+(*i
+val subst_unparsing_hunk : 
   Names.substitution -> (Names.substitution -> 'pat -> 'pat) -> 
   'pat unparsing_hunk -> 'pat unparsing_hunk
-*)
+i*)
 
 (* Checks if the precedence of the parent printer (None means the
    highest precedence), and the child's one, follow the given
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 7b0f7da2..80dc69f1 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,v 1.52.2.1 2004/07/16 19:30:38 herbelin Exp $ *)
+(* $Id: g_constr.ml4,v 1.52.2.2 2004/11/17 12:48:35 herbelin Exp $ *)
 
 open Pcoq
 open Constr
@@ -23,7 +23,7 @@ let constr_kw =
     ":"; "("; ")"; "["; "]"; "{"; "}"; ","; ";"; "->"; "="; ":="; "!";
     "::"; "<:"; ":<"; "=>"; "<"; ">"; "|"; "?"; "/";
     "<->"; "\\/"; "/\\"; "`"; "``"; "&"; "*"; "+"; "@"; "^"; "#"; "-";
-    "~"; "'"; "<<"; ">>"; "<>"
+    "~"; "'"; "<<"; ">>"; "<>"; ".."
   ]
 let _ =
   if !Options.v7 then
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index 18dc5683..adc26532 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: g_constrnew.ml4,v 1.41.2.1 2004/07/16 19:30:38 herbelin Exp $ *)
+(* $Id: g_constrnew.ml4,v 1.41.2.2 2004/11/17 12:48:35 herbelin Exp $ *)
 
 open Pcoq
 open Constr
@@ -22,7 +22,7 @@ open Util
 let constr_kw =
   [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; 
     "end"; "as"; "let"; "if"; "then"; "else"; "return";
-    "Prop"; "Set"; "Type"; ".("; "_" ]
+    "Prop"; "Set"; "Type"; ".("; "_"; ".." ]
 
 let _ = 
   if not !Options.v7 then
diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml
index e43142ba..46ef81f3 100644
--- a/parsing/g_natsyntax.ml
+++ b/parsing/g_natsyntax.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: g_natsyntax.ml,v 1.19.2.1 2004/07/16 19:30:39 herbelin Exp $ *)
+(* $Id: g_natsyntax.ml,v 1.19.2.2 2004/09/08 13:47:51 herbelin Exp $ *)
 
 (* This file to allow writing (3) for (S (S (S O))) 
    and still write (S y) for (S y) *)
@@ -125,7 +125,7 @@ let nat_of_int dloc n =
   match n with
   | POS n ->
       if less_than (of_string "5000") n & Options.is_verbose () then begin
-	warning ("You may experiment stack overflow and segmentation fault\
+	warning ("You may experience stack overflow and segmentation fault\
                   \nwhile parsing numbers in nat greater than 5000");
 	flush_all ()
       end;
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 2e067215..a1559572 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: g_tactic.ml4,v 1.83.2.2 2004/07/16 19:30:39 herbelin Exp $ *)
+(* $Id: g_tactic.ml4,v 1.83.2.4 2005/01/15 14:56:53 herbelin Exp $ *)
 
 open Pp
 open Ast
@@ -42,7 +42,7 @@ let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2)
 if !Options.v7 then
 GEXTEND Gram
   GLOBAL: simple_tactic constrarg bindings constr_with_bindings 
-  quantified_hypothesis red_expr int_or_var castedopenconstr
+  quantified_hypothesis red_expr int_or_var castedopenconstr open_constr
   simple_intropattern;
 
   int_or_var:
@@ -96,8 +96,11 @@ GEXTEND Gram
       | IDENT "Check"; c = constr -> ConstrTypeOf c
       | c = constr -> ConstrTerm c ] ]
   ;
+  open_constr:
+    [ [ c = constr -> ((),c) ] ]
+   ;
   castedopenconstr:
-    [ [ c = constr -> c ] ]
+    [ [ c = constr -> ((),c) ] ]
   ;
   induction_arg:
     [ [ n = natural -> ElimOnAnonHyp n
@@ -180,7 +183,7 @@ GEXTEND Gram
       | IDENT "Unfold"; ul = LIST1 unfold_occ -> Unfold ul
       | IDENT "Fold"; cl = LIST1 constr -> Fold cl
       | IDENT "Pattern"; pl = LIST1 pattern_occ -> Pattern pl
-      | s = IDENT; c = constr -> ExtraRedExpr (s,c) ] ]
+      | s = IDENT -> ExtraRedExpr s ] ]
   ;
   hypident:
     [ [ id = id_or_meta -> id,[],(InHyp,ref None)
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 2070b40e..643be98d 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: g_tacticnew.ml4,v 1.35.2.2 2004/07/16 19:30:39 herbelin Exp $ *)
+(* $Id: g_tacticnew.ml4,v 1.35.2.6 2005/01/15 14:56:53 herbelin Exp $ *)
 
 open Pp
 open Ast
@@ -78,7 +78,7 @@ open Tactic
 let mk_fix_tac (loc,id,bl,ann,ty) =
   let n =
     match bl,ann with
-        [([_],_)], None -> 0
+        [([_],_)], None -> 1
       | _, Some x ->
           let ids = List.map snd (List.flatten (List.map fst bl)) in
           (try list_index (snd x) ids
@@ -109,7 +109,8 @@ let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2)
 if not !Options.v7 then
 GEXTEND Gram
   GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
-  bindings red_expr int_or_var castedopenconstr simple_intropattern;
+  bindings red_expr int_or_var open_constr castedopenconstr 
+  simple_intropattern;
 
   int_or_var:
     [ [ n = integer  -> Genarg.ArgArg n
@@ -128,8 +129,11 @@ GEXTEND Gram
       |	id = METAIDENT -> MetaId (loc,id)
       ] ]
   ;
+  open_constr:
+    [ [ c = constr -> ((),c) ] ]
+   ;
   castedopenconstr:
-    [ [ c = constr -> c ] ]
+    [ [ c = constr -> ((),c) ] ]
   ;
   induction_arg:
     [ [ n = natural -> ElimOnAnonHyp n
@@ -212,7 +216,7 @@ GEXTEND Gram
       | IDENT "unfold"; ul = LIST1 unfold_occ -> Unfold ul
       | IDENT "fold"; cl = LIST1 constr -> Fold cl
       | IDENT "pattern"; pl = LIST1 pattern_occ -> Pattern pl
-      | s = IDENT; c = constr -> ExtraRedExpr (s,c) ] ]
+      | s = IDENT; OPT [ (* compat V8.0pl1 *) constr ] -> ExtraRedExpr s ] ]
   ;
   hypident:
     [ [ id = id_or_meta -> id,(InHyp,ref None)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index e2eecf55..87183e18 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,v 1.93.2.2 2004/07/16 20:51:12 herbelin Exp $ *)
+(* $Id: g_vernac.ml4,v 1.93.2.3 2004/10/12 10:11:28 herbelin Exp $ *)
 
 open Names
 open Topconstr
@@ -189,8 +189,8 @@ GEXTEND Gram
   ;
   gallina:
     (* Definition, Theorem, Variable, Axiom, ... *)
-    [ [ thm = thm_token; id = identref; ":"; c = constr ->
-         VernacStartTheoremProof (thm, id, ([], c), false, (fun _ _ -> ()))
+    [ [ thm = thm_token; id = identref; bl = binders_list; ":"; c = constr ->
+         VernacStartTheoremProof (thm, id, (bl, c), false, (fun _ _ -> ()))
       | (f,d) = def_token; id = identref; b = def_body -> 
           VernacDefinition (d, id, b, f)
       | stre = assumption_token; bl = ne_params_list -> 
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 8a99a51e..976cc259 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: g_vernacnew.ml4,v 1.63.2.1 2004/07/16 19:30:39 herbelin Exp $ *)
+(* $Id: g_vernacnew.ml4,v 1.63.2.2 2004/10/12 10:10:29 herbelin Exp $ *)
 
 open Pp
 open Util
@@ -93,9 +93,8 @@ GEXTEND Gram
 
   gallina:
       (* Definition, Theorem, Variable, Axiom, ... *)
-    [ [ thm = thm_token; id = identref; (* bl = LIST0 binder; *) ":";
+    [ [ thm = thm_token; id = identref; bl = LIST0 binder_let; ":";
         c = lconstr ->
-          let bl = [] in
           VernacStartTheoremProof (thm, id, (bl, c), false, (fun _ _ -> ()))
       | (f,d) = def_token; id = identref; b = def_body -> 
           VernacDefinition (d, id, b, f)
diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml
index 27eead96..2d8d2ddd 100644
--- a/parsing/g_zsyntax.ml
+++ b/parsing/g_zsyntax.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: g_zsyntax.ml,v 1.16.2.1 2004/07/16 19:30:39 herbelin Exp $ *)
+(* $Id: g_zsyntax.ml,v 1.16.2.2 2004/11/10 13:00:44 herbelin Exp $ *)
 
 open Coqast
 open Pcoq
@@ -197,11 +197,14 @@ let rec pat_pos_of_bignat dloc x name =
     | (q,true) ->
         PatCstr (dloc,path_of_xH,[],name)
 
+let error_non_positive dloc = 
+  user_err_loc (dloc, "interp_positive",
+    str "No non-positive numbers in type \"positive\"!")
+
 let pat_interp_positive dloc = function
-  | POS n -> pat_pos_of_bignat dloc n
-  | NEG n ->
-      user_err_loc (dloc, "interp_positive",
-        str "No negative number in type \"positive\"!")
+  | NEG n -> error_non_positive dloc
+  | POS n ->
+     if is_nonzero n then pat_pos_of_bignat dloc n else error_non_positive dloc
 
 (**********************************************************************)
 (* Printing positive via scopes                                       *)
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index cda482af..b5ab2387 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,v 1.80.2.1 2004/07/16 19:30:40 herbelin Exp $ i*)
+(*i $Id: pcoq.ml4,v 1.80.2.3 2005/01/15 14:56:53 herbelin Exp $ i*)
 
 open Pp
 open Util
@@ -371,6 +371,8 @@ module Tactic =
 
     (* Entries that can be refered via the string -> Gram.Entry.e table *)
     (* Typically for tactic user extensions *)
+    let open_constr = 
+      make_gen_entry utactic rawwit_open_constr "open_constr"
     let castedopenconstr = 
       make_gen_entry utactic rawwit_casted_open_constr "castedopenconstr"
     let constr_with_bindings =
@@ -774,7 +776,9 @@ let is_self from e =
 
 let is_binder_level from e =
   match from, e with
-      ETConstr(200,()), ETConstr(NumLevel 200,_) -> not !Options.v7
+      ETConstr(200,()),
+      ETConstr(NumLevel 200,(BorderProd(false,_)|InternalProd)) ->
+        not !Options.v7
     | _ -> false
 
 let rec symbol_of_production assoc from forpat typ =
@@ -799,5 +803,3 @@ let rec symbol_of_production assoc from forpat typ =
       | (eobj,Some None,_) -> Gramext.Snext
       | (eobj,Some (Some (lev,cur)),_) -> 
           Gramext.Snterml (Gram.Entry.obj eobj,constr_prod_level assoc cur lev)
-
-
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 5c6c8354..361137f4 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,v 1.63.2.1 2004/07/16 19:30:40 herbelin Exp $ i*)
+(*i $Id: pcoq.mli,v 1.63.2.2 2005/01/15 14:56:53 herbelin Exp $ i*)
 
 open Util
 open Names
@@ -156,7 +156,8 @@ module Module :
 module Tactic :
   sig
     open Rawterm
-    val castedopenconstr : constr_expr Gram.Entry.e
+    val open_constr : open_constr_expr Gram.Entry.e
+    val castedopenconstr : open_constr_expr Gram.Entry.e
     val constr_with_bindings : constr_expr with_bindings Gram.Entry.e
     val bindings : constr_expr bindings Gram.Entry.e
     val constrarg : (constr_expr,reference) may_eval Gram.Entry.e
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 6a5242e8..ddf008cb 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ppconstr.ml,v 1.32.2.1 2004/07/16 19:30:40 herbelin Exp $ *)
+(* $Id: ppconstr.ml,v 1.32.2.2 2004/12/29 10:17:11 herbelin Exp $ *)
 
 (*i*)
 open Ast
@@ -370,8 +370,7 @@ let pr_red_expr (pr_constr,pr_ref) = function
   | Fold l -> hov 1 (str "Fold" ++ prlist (pr_arg pr_constr) l)
   | Pattern l -> hov 1 (str "Pattern " ++ prlist (pr_occurrences pr_constr) l)
   | Red true -> error "Shouldn't be accessible from user"
-  | ExtraRedExpr (s,c) ->
-      hov 1 (str s ++ pr_arg pr_constr c)
+  | ExtraRedExpr s -> str s
 
 let rec pr_may_eval pr pr2 = function
   | ConstrEval (r,c) ->
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index d238b371..039cd745 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ppconstr.mli,v 1.7.2.1 2004/07/16 19:30:40 herbelin Exp $ *)
+(*i $Id: ppconstr.mli,v 1.7.2.2 2005/01/21 17:19:37 herbelin Exp $ i*)
 
 open Pp
 open Environ
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 95e134ae..1d7a9428 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pptactic.ml,v 1.54.2.2 2004/07/16 19:30:40 herbelin Exp $ *)
+(* $Id: pptactic.ml,v 1.54.2.3 2005/01/15 14:56:53 herbelin Exp $ *)
 
 open Pp
 open Names
@@ -272,8 +272,9 @@ let rec pr_raw_generic prc prlc prtac prref x =
       pr_arg (pr_red_expr 
         (prc,prref)) (out_gen rawwit_red_expr x)
   | TacticArgType -> pr_arg prtac (out_gen rawwit_tactic x)
+  | OpenConstrArgType -> pr_arg prc (snd (out_gen rawwit_open_constr x))
   | CastedOpenConstrArgType ->
-      pr_arg prc (out_gen rawwit_casted_open_constr x)
+      pr_arg prc (snd (out_gen rawwit_casted_open_constr x))
   | ConstrWithBindingsArgType -> 
       pr_arg (pr_with_bindings prc prlc) (out_gen rawwit_constr_with_bindings x)
   | BindingsArgType -> 
@@ -320,8 +321,9 @@ let rec pr_glob_generic prc prlc prtac x =
       pr_arg (pr_red_expr 
         (prc,pr_or_var (pr_and_short_name pr_evaluable_reference))) (out_gen globwit_red_expr x)
   | TacticArgType -> pr_arg prtac (out_gen globwit_tactic x)
+  | OpenConstrArgType -> pr_arg prc (snd (out_gen globwit_open_constr x))
   | CastedOpenConstrArgType ->
-      pr_arg prc (out_gen globwit_casted_open_constr x)
+      pr_arg prc (snd (out_gen globwit_casted_open_constr x))
   | ConstrWithBindingsArgType -> 
       pr_arg (pr_with_bindings prc prlc) (out_gen globwit_constr_with_bindings x)
   | BindingsArgType -> 
@@ -367,6 +369,7 @@ let rec pr_generic prc prlc prtac x =
   | RedExprArgType ->
       pr_arg (pr_red_expr (prc,pr_evaluable_reference)) (out_gen wit_red_expr x)
   | TacticArgType -> pr_arg prtac (out_gen wit_tactic x)
+  | OpenConstrArgType -> pr_arg prc (snd (out_gen wit_open_constr x))
   | CastedOpenConstrArgType ->
       pr_arg prc (snd (out_gen wit_casted_open_constr x))
   | ConstrWithBindingsArgType -> 
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index a80ec6fb..b9cf7401 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pptactic.mli,v 1.9.2.1 2004/07/16 19:30:40 herbelin Exp $ *)
+(*i $Id: pptactic.mli,v 1.9.2.2 2005/01/21 17:19:37 herbelin Exp $ i*)
 
 open Pp
 open Genarg
diff --git a/parsing/printer.mli b/parsing/printer.mli
index b4cd87b0..c44be124 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: printer.mli,v 1.26.2.1 2004/07/16 19:30:41 herbelin Exp $ i*)
+(*i $Id: printer.mli,v 1.26.2.2 2005/01/21 16:42:37 herbelin Exp $ i*)
 
 (*i*)
 open Pp
@@ -22,9 +22,9 @@ open Termops
 (*i*)
 
 (* These are the entry points for printing terms, context, tac, ... *)
-(*
+(*i
 val gentacpr  : Tacexpr.raw_tactic_expr -> std_ppcmds
-*)
+i*)
 
 val prterm_env      : env -> constr -> std_ppcmds
 val prterm_env_at_top : env -> constr -> std_ppcmds
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index aa0fce9d..a278e3d5 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,v 1.47.2.2 2004/07/16 20:51:12 herbelin Exp $ *)
+(* $Id: q_coqast.ml4,v 1.47.2.5 2005/01/15 14:56:54 herbelin Exp $ *)
 
 open Util
 open Names
@@ -21,8 +21,12 @@ let purge_str s =
 
 let anti loc x =
   let e =
-    let loc = unloc loc in
-    let loc = make_loc (1, snd loc - fst loc) in <:expr< $lid:purge_str x$ >>
+    let loc = 
+      ifdef OCAML_308 then
+        loc
+      else
+        (1, snd loc - fst loc)
+    in <:expr< $lid:purge_str x$ >>
   in
   <:expr< $anti:e$ >>
 
@@ -244,9 +248,8 @@ let mlexpr_of_red_expr = function
   | Rawterm.Pattern l ->
       let f = mlexpr_of_list mlexpr_of_occ_constr in
       <:expr< Rawterm.Pattern $f l$ >>
-  | Rawterm.ExtraRedExpr (s,c) ->
-      let l = mlexpr_of_constr c in
-      <:expr< Rawterm.ExtraRedExpr $mlexpr_of_string s$ $l$ >>
+  | Rawterm.ExtraRedExpr s ->
+      <:expr< Rawterm.ExtraRedExpr $mlexpr_of_string s$ >>
 
 let rec mlexpr_of_argtype loc = function
   | Genarg.BoolArgType -> <:expr< Genarg.BoolArgType >>
@@ -259,6 +262,7 @@ let rec mlexpr_of_argtype loc = function
   | Genarg.HypArgType -> <:expr< Genarg.HypArgType >>
   | Genarg.StringArgType -> <:expr< Genarg.StringArgType >>
   | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >>
+  | Genarg.OpenConstrArgType -> <:expr< Genarg.OpenConstrArgType >>
   | Genarg.CastedOpenConstrArgType -> <:expr< Genarg.CastedOpenConstrArgType >>
   | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >>
   | Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >>