Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et commandes vernaculaires (cf dev/changements.txt pour plus de précisions)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2734 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 44 insertions, 2 deletions

diff --git a/dev/changements.txt b/dev/changements.txt
index 29eab892e..a294082f7 100644
--- a/dev/changements.txt
+++ b/dev/changements.txt
@@ -1,3 +1,45 @@
+MAIN CHANGES FROM COQ V7.3
+==========================
+
+New parsing model for tactics and vernacular commands
+
+  - Introduction of a dedicated type for tactic expressions
+    (Tacexpr.raw_tactic_expr)
+  - Introduction of a dedicated type for vernac expressions
+    (Vernacexpr.vernac_expr)
+  - Declaration of new vernacular parsing rules by a new camlp4 macro
+    GRAMMAR COMMAND EXTEND ... END  to be used in ML files
+  - Declaration of new tactics parsing/printing rules by a new camlp4 macro
+    TACTIC EXTEND ... END  to be used in ML files
+
+New organisation of THENS:
+tclTHENS tac tacs : tacs is now an array
+tclTHENSFIRSTn tac1 tacs tac2 :
+  apply tac1 then, apply the array tacs on the first n subgoals and
+  tac2 on the remaining subgoals (previously tclTHENST)
+tclTHENSLASTn tac1 tac2 tacs :
+  apply tac1 then, apply tac2 on the first subgoals and apply the array
+  tacs on the last n subgoals
+tclTHENFIRSTn tac1 tacs = tclTHENSFIRSTn tac1 tacs tclIDTAC (prev. tclTHENSI)
+tclTHENLASTn tac1 tacs  = tclTHENSLASTn tac1 tclIDTAC tacs
+tclTHENFIRST tac1 tac2  = tclTHENFIRSTn tac1 [|tac2|]
+tclTHENLAST tac1 tac2   = tclTHENLASTn tac1 [|tac2|] (previously tclTHENL)
+tclTHENS tac1 tacs = tclTHENSFIRSTn tac1 tacs (fun _ -> error "wrong number")
+tclTHENSV same as tclTHENS but with an array
+tclTHENSi : no longer available
+
+Proof_type: subproof field in type proof_tree glued with the ref field
+
+Tacmach: no more echo from functions of module Refiner
+
+Files contrib/*/g_*.ml4 take the place of files contrib/*/*.v.
+Files parsing/{vernac,tac}extend.ml{4,i} implements TACTIC EXTEND andd
+  VERNAC COMMAND EXTEND macros
+File syntax/PPTactic.v moved to parsing/pptactic.ml
+Tactics about False and not now in tactics/contradiction.ml
+Tactics depending on Init now tactics/*.ml4 (no longer in tactics/*.v)
+File tacinterp.ml moved from proofs to directory tactics
+
 MAIN CHANGES FROM COQ V7.1 TO COQ V7.2
 ======================================
 
diff --git a/dev/db_printers.ml b/dev/db_printers.ml
index c7857e968..3e4ba263f 100644
--- a/dev/db_printers.ml
+++ b/dev/db_printers.ml
@@ -8,7 +8,7 @@
 open Pp
 open Names
 
-let pP s = pP (hov 0 s)
+let pp s = pp (hov 0 s)
 
 let prid id = Format.print_string (string_of_id id)
 let prsp sp = Format.print_string (string_of_path sp)
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index b17942884..417bbfce2 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -79,7 +79,7 @@ let pp_universes u = pp (str"[" ++ pr_universes u ++ str"]")
 
 let ppenv e = pp (pr_rel_context e (rel_context e))
 
-let pptac = (fun x -> pp(gentacpr x))
+let pptac = (fun x -> pp(Pptactic.pr_raw_tactic x))
 
 let cnt = ref 0