3 files changed, 124 insertions, 0 deletions
diff --git a/contrib7/interface/AddDad.v b/contrib7/interface/AddDad.v
new file mode 100644
index 00000000..d22b7ed1
--- /dev/null
+++ b/contrib7/interface/AddDad.v
@@ -0,0 +1,19 @@
+Grammar vernac vernac : ast :=
+ add_dad_rule00 ["AddDadRule" stringarg($name) constrarg($pat) 
+       "first_path" "second_path" tacarg($tac) "."] ->
+    [(AddDadRule $name $pat (NUMBERLIST) (NUMBERLIST) (TACTIC $tac))].
+Grammar vernac vernac:ast :=
+| add_dad_rule01 ["AddDadRule" stringarg($name) constrarg($pat)
+       "first_path" "second_path" ne_numarg_list($l) tacarg($tac) "."] ->
+    [(AddDadRule $name $pat (NUMBERLIST) (NUMBERLIST ($LIST $l)) (TACTIC $tac))]
+| add_dad_rule10 ["AddDadRule" stringarg($name) constrarg($pat)
+       "first_path" ne_numarg_list($l) "second_path" tacarg($tac) "."] ->
+    [(AddDadRule $name $pat (NUMBERLIST ($LIST $l))(NUMBERLIST) (TACTIC $tac))]
+| add_dad_rule11 ["AddDadRule" stringarg($name) constrarg($pat)
+       "first_path" ne_numarg_list($l) "second_path" ne_numarg_list($l1)
+       tacarg($tac) "."] ->
+    [(AddDadRule $name $pat (NUMBERLIST ($LIST $l))(NUMBERLIST ($LIST $l1))
+       (TACTIC $tac))].
+
+Grammar vernac vernac : ast :=
+ start_dad [ "StartDad" "."] -> [(StartDad)].
diff --git a/contrib7/interface/Centaur.v b/contrib7/interface/Centaur.v
new file mode 100644
index 00000000..d27929f8
--- /dev/null
+++ b/contrib7/interface/Centaur.v
@@ -0,0 +1,88 @@
+(*
+Declare ML Module "ctast".
+Declare ML Module "paths".
+Declare ML Module "name_to_ast".
+Declare ML Module "xlate".
+Declare ML Module "vtp".
+Declare ML Module "translate".
+Declare ML Module "pbp".
+Declare ML Module "blast".
+Declare ML Module "dad".
+Declare ML Module "showproof_ct".
+Declare ML Module "showproof".
+Declare ML Module "debug_tac".
+Declare ML Module "paths".
+Declare ML Module "history".
+Declare ML Module "centaur".
+(* Require Export Illustrations. *)
+(* Require Export AddDad. *)
+(*
+Grammar vernac vernac : ast :=
+  goal_cmd [ "Goal" "Cmd" numarg($n) "with" tacarg($tac) "." ] ->
+        [(GOAL_CMD $n (TACTIC $tac))]
+| kill_proof_after [ "Kill" "Proof" "after"  numarg($n)"." ] -> [(KILL_NODE $n)]
+| kill_proof_at [ "Kill" "Proof" "at"  numarg($n)"." ] -> [(KILL_NODE $n)]
+| kill_sub_proof [ "Kill" "SubProof" numarg($n) "." ] -> [(KILL_SUB_PROOF $n)]
+
+| print_past_goal [ "Print" "Past" "Goal" numarg($n) "." ] ->
+        [(PRINT_GOAL_AT $n) ]
+
+| check_in_goal [ "CHECK_IN_GOAL" numarg($n) constrarg($c) "." ] ->
+       [(CHECK_IN_GOAL "CHECK" $n $c)]
+| eval_in_goal [ "EVAL_IN_GOAL" numarg($n) constrarg($c) "." ] ->
+       [(CHECK_IN_GOAL "EVAL" $n $c)]
+| compute_in_goal [ "COMPUTE_IN_GOAL" numarg($n) constrarg($c) "." ] ->
+       [(CHECK_IN_GOAL "COMPUTE" $n $c)]
+| centaur_reset [ "Centaur" "Reset" identarg($id) "." ] -> [(Centaur_Reset $id)]
+(*| show_dad_rules [ "Show" "Dad" "Rules" "." ] -> [(Show_dad_rules)]*)
+| start_pcoq [ "Start" "Pcoq" "Mode" "." ] -> [ (START_PCOQ) ]
+| start_pcoq [ "Start" "Pcoq" "Debug" "Mode" "." ] -> [ (START_PCOQ_DEBUG) ].
+Grammar vernac ne_id_list : ast list :=
+   id_one [ identarg($id)] -> [$id]
+ | id_more [identarg($id) ne_id_list($others)] -> [$id ($LIST $others)].
+
+Grammar tactic ne_num_list : ast list :=
+  ne_last [ numarg($n) ] -> [ $n ]
+| ne_num_ste  [ numarg($n) ne_num_list($ns) ] -> [ $n ($LIST $ns)].
+
+Grammar tactic two_numarg_list : ast list :=
+  two_single_and_ne [ numarg($n) "to"  ne_num_list($ns)] ->
+        [$n (TACTIC (to)) ($LIST $ns)]
+| two_rec [ numarg($n) two_numarg_list($ns)] -> [ $n ($LIST $ns)].
+
+Grammar tactic simple_tactic : ast :=
+  pbp0 [ "Pbp" ] -> [(PcoqPbp)]
+| pbp1 [ "Pbp" ne_num_list($ns) ] ->
+         [ (PcoqPbp ($LIST $ns)) ]
+| pbp2 [ "Pbp" identarg($id) ] -> [ (PcoqPbp $id) ]
+| pbp3 [ "Pbp" identarg($id) ne_num_list($ns)] ->
+         [ (PcoqPbp $id ($LIST $ns)) ]
+| blast1 [ "Blast" ne_num_list($ns) ] ->
+         [ (PcoqBlast ($LIST $ns)) ]
+| dad00 [ "Dad" "to" ] -> [(Dad (TACTIC (to)))]
+| dad01 [ "Dad" "to" ne_num_list($ns) ] ->
+        [(Dad (TACTIC (to)) ($LIST $ns))]
+| dadnn [ "Dad" two_numarg_list($ns) ] -> [ (Dad ($LIST $ns)) ]
+| debug_tac [ "DebugTac" tactic($tac) ] ->
+  [(CtDebugTac (TACTIC $tac))]
+| on_then_empty [ "OnThen" tactic($tac1) tactic($tac2) ] ->
+    [(OnThen (TACTIC $tac1) (TACTIC $tac2))]
+| on_then_ne [ "OnThen" tactic($tac1) tactic($tac2) ne_num_list($l) ] ->
+  [(OnThen (TACTIC $tac1) (TACTIC $tac2) ($LIST $l))]
+| debug_tac2 [ "DebugTac2" tactic($tac) ] ->
+  [(CtDebugTac2 (TACTIC $tac))].
+
+
+(* Maybe we should have syntactic rules to make sur that syntax errors are
+   displayed with a readable syntax.  It is not sure, since the error reporting
+   procedure changed from V6.1 and does not reprint the command anymore. *)
+Grammar vernac vernac : ast :=
+  text_proof_flag_on [ "Text" "Mode" "fr" "." ] ->
+       [(TEXT_MODE (AST "fr"))]
+| text_proof_flag_on [ "Text" "Mode" "en" "." ] ->
+       [(TEXT_MODE (AST "en"))]
+| text_proof_flag_on [ "Text" "Mode" "Off" "." ] ->
+       [(TEXT_MODE (AST "off"))].
+
+*)
+*)
diff --git a/contrib7/interface/vernacrc b/contrib7/interface/vernacrc
new file mode 100644
index 00000000..f95c4212
--- /dev/null
+++ b/contrib7/interface/vernacrc
@@ -0,0 +1,17 @@
+# $Id: vernacrc,v 1.1 2003/11/29 20:02:41 herbelin Exp $
+
+# This file is loaded initially by ./vernacparser.
+
+load_syntax_file 17 LogicSyntax
+load_syntax_file 36 SpecifSyntax
+load_syntax_file 18 Logic_TypeSyntax
+load_syntax_file 19 DatatypesSyntax
+load_syntax_file 21 Equality
+load_syntax_file 22 Inv
+load_syntax_file 26 Tauto
+load_syntax_file 34 Omega
+load_syntax_file 27 Ring
+quiet_parse_string
+Goal a.
+&& END--OF--DATA
+print_version