Imported Upstream version 8.0pl3upstream/8.0pl3

12 files changed, 55 insertions, 35 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 7a151c1a..09889d40 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: egrammar.ml,v 1.48.2.3 2004/11/26 19:37:59 herbelin Exp $ *)
+(* $Id: egrammar.ml,v 1.48.2.4 2005/12/23 22:16:46 herbelin Exp $ *)
 
 open Pp
 open Util
@@ -30,12 +30,13 @@ type all_grammar_command =
   | TacticGrammar of
       (string * (string * grammar_production list) * 
       (Names.dir_path * Tacexpr.raw_tactic_expr))
-      list
+      list * (string * Genarg.argument_type list *
+              (string * Pptactic.grammar_terminals)) list
 
 let subst_all_grammar_command subst = function
   | Notation _ -> anomaly "Notation not in GRAMMAR summary"
   | Grammar gc -> Grammar (subst_grammar_command subst gc)
-  | TacticGrammar g -> TacticGrammar g (* TODO ... *)
+  | TacticGrammar (g,p) -> TacticGrammar (g,p) (* TODO ... *)
 
 let (grammar_state : all_grammar_command list ref) = ref []
 
@@ -419,7 +420,7 @@ let extend_grammar gram =
   (match gram with
   | Notation (_,a) -> extend_constr_notation a
   | Grammar g -> extend_grammar_rules g
-  | TacticGrammar l -> add_tactic_entries l);
+  | TacticGrammar (l,_) -> add_tactic_entries l);
   grammar_state := gram :: !grammar_state
 
 let reset_extend_grammars_v8 () =
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index 0009b4b6..ade91453 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.5 2004/11/27 09:25:44 herbelin Exp $ i*)
+(*i $Id: egrammar.mli,v 1.14.2.6 2005/12/23 22:16:46 herbelin Exp $ i*)
 
 (*i*)
 open Util
@@ -28,7 +28,8 @@ type all_grammar_command =
   | TacticGrammar of
       (string * (string * grammar_production list) * 
       (Names.dir_path * Tacexpr.raw_tactic_expr))
-      list
+      list * (string * Genarg.argument_type list *
+              (string * Pptactic.grammar_terminals)) list
 
 val extend_grammar : all_grammar_command -> unit
 
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index adc26532..fe579e98 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.2 2004/11/17 12:48:35 herbelin Exp $ *)
+(* $Id: g_constrnew.ml4,v 1.41.2.4 2005/09/21 14:47:33 herbelin Exp $ *)
 
 open Pcoq
 open Constr
@@ -285,7 +285,9 @@ GEXTEND Gram
     [ [ pl = LIST1 pattern SEP ","; "=>"; rhs = lconstr -> (loc,pl,rhs) ] ]
   ;
   pattern:
-    [ "10" LEFTA
+    [ "200" RIGHTA [ ]
+    | "99" RIGHTA [ ]
+    | "10" LEFTA
       [ p = pattern ; lp = LIST1 (pattern LEVEL "0") ->
         (match p with
           | CPatAtom (_, Some r) -> CPatCstr (loc, r, lp)
diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4
index 9c8d1675..7492ac8c 100644
--- a/parsing/g_ltacnew.ml4
+++ b/parsing/g_ltacnew.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: g_ltacnew.ml4,v 1.22.2.2 2004/07/16 19:30:38 herbelin Exp $ *)
+(* $Id: g_ltacnew.ml4,v 1.22.2.3 2005/06/21 15:31:12 herbelin Exp $ *)
 
 open Pp
 open Util
@@ -43,7 +43,7 @@ let tactic_expr = Gram.Entry.create "tactic:tactic_expr"
 
 if not !Options.v7 then
 GEXTEND Gram
-  GLOBAL: tactic Vernac_.command tactic_expr tactic_arg;
+  GLOBAL: tactic Vernac_.command tactic_expr tactic_arg constr_may_eval;
 
   tactic_expr:
     [ "5" LEFTA
@@ -108,14 +108,20 @@ GEXTEND Gram
       | c = Constr.constr -> ConstrMayEval (ConstrTerm c) ] ]
   ;
   may_eval_arg:
+    [ [ c = constr_eval -> ConstrMayEval c
+      | IDENT "fresh"; s = OPT STRING -> TacFreshId s ] ]
+  ;
+  constr_eval:
     [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
-	  ConstrMayEval (ConstrEval (rtc,c))
+	  ConstrEval (rtc,c)
       | IDENT "context"; id = identref; "["; c = Constr.lconstr; "]" ->
-	  ConstrMayEval (ConstrContext (id,c))
+	  ConstrContext (id,c)
       | IDENT "type"; IDENT "of"; c = Constr.constr ->
-	  ConstrMayEval (ConstrTypeOf c)
-      | IDENT "fresh"; s = OPT STRING ->
-	  TacFreshId s ] ]
+	  ConstrTypeOf c ] ]
+  ;
+  constr_may_eval: (* For extensions *)
+    [ [ c = constr_eval -> c
+      | c = Constr.constr -> ConstrTerm c ] ]
   ;
   tactic_atom:
     [ [ id = METAIDENT -> MetaIdArg (loc,id)
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index a1559572..fd64defc 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.4 2005/01/15 14:56:53 herbelin Exp $ *)
+(* $Id: g_tactic.ml4,v 1.83.2.5 2005/05/15 12:47:04 herbelin Exp $ *)
 
 open Pp
 open Ast
@@ -306,14 +306,14 @@ GEXTEND Gram
 
       (* Automation tactic *)
       | IDENT "Trivial"; db = hintbases -> TacTrivial db
-      | IDENT "Auto"; n = OPT natural; db = hintbases -> TacAuto (n, db)
+      | IDENT "Auto"; n = OPT int_or_var; db = hintbases -> TacAuto (n, db)
 
       | IDENT "AutoTDB"; n = OPT natural -> TacAutoTDB n
       | IDENT "CDHyp"; id = identref -> TacDestructHyp (true,id)
       | IDENT "DHyp";  id = identref -> TacDestructHyp (false,id)
       | IDENT "DConcl"  -> TacDestructConcl
       | IDENT "SuperAuto"; l = autoargs -> TacSuperAuto l
-      | IDENT "Auto"; n = OPT natural; IDENT "Decomp"; p = OPT natural ->
+      | IDENT "Auto"; n = OPT int_or_var; IDENT "Decomp"; p = OPT natural ->
 	  TacDAuto (n, p)
 
       (* Context management *)
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 643be98d..5ffd2fd7 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.6 2005/01/15 14:56:53 herbelin Exp $ *)
+(* $Id: g_tacticnew.ml4,v 1.35.2.7 2005/05/15 12:47:05 herbelin Exp $ *)
 
 open Pp
 open Ast
@@ -340,7 +340,7 @@ GEXTEND Gram
 
       (* Automation tactic *)
       | IDENT "trivial"; db = hintbases -> TacTrivial db
-      | IDENT "auto"; n = OPT natural; db = hintbases -> TacAuto (n, db)
+      | IDENT "auto"; n = OPT int_or_var; db = hintbases -> TacAuto (n, db)
 
 (* Obsolete since V8.0
       | IDENT "autotdb"; n = OPT natural -> TacAutoTDB n
@@ -349,7 +349,7 @@ GEXTEND Gram
       | IDENT "dconcl"  -> TacDestructConcl
       | IDENT "superauto"; l = autoargs -> TacSuperAuto l
 *)
-      | IDENT "auto"; n = OPT natural; IDENT "decomp"; p = OPT natural ->
+      | IDENT "auto"; n = OPT int_or_var; IDENT "decomp"; p = OPT natural ->
 	  TacDAuto (n, p)
 
       (* Context management *)
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index b5ab2387..a8922536 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.3 2005/01/15 14:56:53 herbelin Exp $ i*)
+(*i $Id: pcoq.ml4,v 1.80.2.4 2005/06/21 15:31:12 herbelin Exp $ i*)
 
 open Pp
 open Util
@@ -379,7 +379,8 @@ module Tactic =
       make_gen_entry utactic rawwit_constr_with_bindings "constr_with_bindings"
     let bindings =
       make_gen_entry utactic rawwit_bindings "bindings"
-    let constrarg = make_gen_entry utactic rawwit_constr_may_eval "constrarg"
+(*v7*) let constrarg = make_gen_entry utactic rawwit_constr_may_eval "constrarg"
+(*v8*) let constr_may_eval = make_gen_entry utactic rawwit_constr_may_eval "constr_may_eval"
     let quantified_hypothesis =
       make_gen_entry utactic rawwit_quant_hyp "quantified_hypothesis"
     let int_or_var = make_gen_entry utactic rawwit_int_or_var "int_or_var"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 361137f4..15a2c2cc 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.2 2005/01/15 14:56:53 herbelin Exp $ i*)
+(*i $Id: pcoq.mli,v 1.63.2.3 2005/06/21 15:31:12 herbelin Exp $ i*)
 
 open Util
 open Names
@@ -160,7 +160,8 @@ module Tactic :
     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
+(*v7*) val constrarg : (constr_expr,reference) may_eval Gram.Entry.e
+(*v8*) val constr_may_eval : (constr_expr,reference) may_eval Gram.Entry.e
     val quantified_hypothesis : quantified_hypothesis Gram.Entry.e
     val int_or_var : int or_var Gram.Entry.e
     val red_expr : raw_red_expr Gram.Entry.e
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 1d7a9428..4103ea00 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.3 2005/01/15 14:56:53 herbelin Exp $ *)
+(* $Id: pptactic.ml,v 1.54.2.5 2005/12/23 22:16:46 herbelin Exp $ *)
 
 open Pp
 open Names
@@ -42,6 +42,8 @@ let declare_extra_tactic_pprule for_v8 s (tags,prods) =
   Hashtbl.add prtac_tab_v7 (s,tags) prods;
   if for_v8 then Hashtbl.add prtac_tab (s,tags) prods
 
+let exists_extra_tactic_pprule s tags = Hashtbl.mem prtac_tab_v7 (s,tags)
+
 type 'a raw_extra_genarg_printer =
     (constr_expr -> std_ppcmds) -> (raw_tactic_expr -> std_ppcmds) ->
       'a -> std_ppcmds
@@ -536,7 +538,8 @@ and pr_atom1 = function
   | TacTrivial (Some []) as x -> pr_atom0 x
   | TacTrivial db -> hov 0 (str "Trivial" ++ pr_hintbases db)
   | TacAuto (None,Some []) as x -> pr_atom0 x
-  | TacAuto (n,db) -> hov 0 (str "Auto" ++ pr_opt int n ++ pr_hintbases db)
+  | TacAuto (n,db) ->
+      hov 0 (str "Auto" ++ pr_opt (pr_or_var int) n ++ pr_hintbases db)
   | TacAutoTDB None as x -> pr_atom0 x
   | TacAutoTDB (Some n) -> hov 0 (str "AutoTDB" ++ spc () ++ int n)
   | TacDestructHyp (true,(_,id)) -> hov 0 (str "CDHyp" ++ spc () ++ pr_id id)
@@ -546,7 +549,8 @@ and pr_atom1 = function
       hov 1 (str "SuperAuto" ++ pr_opt int n ++ pr_autoarg_adding l ++ 
              pr_autoarg_destructing b1 ++ pr_autoarg_usingTDB b2)
   | TacDAuto (n,p) ->
-      hov 1 (str "Auto" ++ pr_opt int n ++ str "Decomp" ++ pr_opt int p)
+      hov 1 (str "Auto" ++ pr_opt (pr_or_var int) n ++ str "Decomp" ++ 
+      pr_opt int p)
 
   (* Context management *)
   | TacClear l ->
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index b9cf7401..5c3035ba 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pptactic.mli,v 1.9.2.2 2005/01/21 17:19:37 herbelin Exp $ i*)
+(*i $Id: pptactic.mli,v 1.9.2.3 2005/12/23 22:16:46 herbelin Exp $ i*)
 
 open Pp
 open Genarg
@@ -46,6 +46,8 @@ type grammar_terminals = string option list
 val declare_extra_tactic_pprule : bool -> string -> 
   argument_type list * (string * grammar_terminals) -> unit
 
+val exists_extra_tactic_pprule : string -> argument_type list -> bool
+
 val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds
 
 val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 169eff94..1505745c 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: prettyp.ml,v 1.50.2.1 2004/07/16 19:30:40 herbelin Exp $ *)
+(* $Id: prettyp.ml,v 1.50.2.2 2005/11/21 09:16:28 herbelin Exp $ *)
 
 open Pp
 open Util
@@ -180,8 +180,10 @@ let print_located_qualid ref =
   let (loc,qid) = qualid_of_reference ref in
   let module N = Nametab in
   let expand = function
-    | TrueGlobal ref -> Term ref, N.shortest_qualid_of_global Idset.empty ref
-    | SyntacticDef kn -> Syntactic kn, N.shortest_qualid_of_syndef kn in
+    | TrueGlobal ref -> 
+	Term ref, N.shortest_qualid_of_global Idset.empty ref
+    | SyntacticDef kn -> 
+	Syntactic kn, N.shortest_qualid_of_syndef Idset.empty kn in
   match List.map expand (N.extended_locate_all qid) with
     | [] -> 
 	let (dir,id) = repr_qualid qid in
@@ -329,7 +331,7 @@ let print_constant_with_infos sp =
 let print_inductive sp = (print_mutual sp)
 
 let print_syntactic_def sep kn =
-  let qid = Nametab.shortest_qualid_of_syndef kn in
+  let qid = Nametab.shortest_qualid_of_syndef Idset.empty kn in
   let c = Syntax_def.search_syntactic_definition dummy_loc kn in 
   (str (if !Options.v7 then "Syntactic Definition " else "Notation ")
    ++ pr_qualid qid ++ str sep ++ 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index a278e3d5..e8e1830a 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.5 2005/01/15 14:56:54 herbelin Exp $ *)
+(* $Id: q_coqast.ml4,v 1.47.2.6 2005/05/15 12:47:05 herbelin Exp $ *)
 
 open Util
 open Names
@@ -454,7 +454,7 @@ let rec mlexpr_of_atomic_tactic = function
 
   (* Automation tactics *)
   | Tacexpr.TacAuto (n,l) ->
-      let n = mlexpr_of_option mlexpr_of_int n in
+      let n = mlexpr_of_option (mlexpr_of_or_var mlexpr_of_int) n in
       let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in
       <:expr< Tacexpr.TacAuto $n$ $l$ >>
 (*