Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.v

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

7 files changed, 166 insertions, 67 deletions

diff --git a/contrib/ring/ArithRing.v b/contrib/ring/ArithRing.v
index b9883d5cd4..e89017daf7 100644
--- a/contrib/ring/ArithRing.v
+++ b/contrib/ring/ArithRing.v
@@ -34,7 +34,7 @@ Hints Resolve nateq_prop eq2eqT : arithring.
 
 Definition NatTheory : (Semi_Ring_Theory plus mult (1) (0) nateq).
   Split; Intros; Auto with arith arithring.
-  Apply eq2eqT; Apply simpl_plus_l with n.
+  Apply eq2eqT; Apply simpl_plus_l with n:=n.
   Apply eqT2eq; Trivial.
 Defined.
 
diff --git a/contrib/ring/Quote.v b/contrib/ring/Quote.v
index 1565e522b4..e2bd0c5378 100644
--- a/contrib/ring/Quote.v
+++ b/contrib/ring/Quote.v
@@ -83,10 +83,3 @@ Save.
 End variables_map.
 
 Unset Implicit Arguments.
-
-Declare ML Module "quote".
-
-Grammar tactic simple_tactic : ast := 
-  quote [ "Quote" identarg($f) ] -> [(Quote $f)]
-| quote_lc [ "Quote" identarg($f) "[" ne_identarg_list($lc) "]"] ->  
-                   [ (Quote $f ($LIST $lc)) ].
diff --git a/contrib/ring/Ring.v b/contrib/ring/Ring.v
index 93c6eaf539..fa2ba1ca0c 100644
--- a/contrib/ring/Ring.v
+++ b/contrib/ring/Ring.v
@@ -14,55 +14,6 @@ Require Export Quote.
 Require Export Ring_normalize.
 Require Export Ring_abstract.
 
-Declare ML Module "ring".
-
-Grammar tactic simple_tactic : ast :=
-  ring [ "Ring" constrarg_list($arg) ] -> [(Ring ($LIST $arg))].
-
-Syntax tactic level 0:
-  ring [ << (Ring ($LIST $lc)) >> ] -> [ "Ring" [1 1] (LISTSPC ($LIST $lc)) ] 
-| ring_e [ << (Ring) >> ] -> ["Ring"].
- 
-Grammar vernac vernac : ast := 
-  addring [ "Add" "Ring" 
-     constrarg($a) constrarg($aplus) constrarg($amult) constrarg($aone)
-     constrarg($azero) constrarg($aopp) constrarg($aeq) constrarg($t)
-     "[" ne_constrarg_list($l) "]" "." ] 
-  -> [(AddRing $a $aplus $amult $aone $azero $aopp $aeq $t
-     ($LIST $l))]
-
-| addsemiring [ "Add" "Semi" "Ring" 
-      	       	 constrarg($a) constrarg($aplus) constrarg($amult) 
-                 constrarg($aone) constrarg($azero) constrarg($aeq) 
-                 constrarg($t) 
-      	       	 "[" ne_constrarg_list($l) "]" "." ] 
-  -> [(AddSemiRing $a $aplus $amult $aone $azero $aeq $t
-      	   ($LIST $l))]
-| addabstractring [ "Add" "Abstract" "Ring" 
-      	     constrarg($a) constrarg($aplus) constrarg($amult)
-             constrarg($aone) constrarg($azero) constrarg($aopp)
-             constrarg($aeq) constrarg($t) "." ] 
-  -> [(AddAbstractRing $a $aplus $amult $aone $azero $aopp $aeq $t)]
-
-| addabstractsemiring [ "Add" "Abstract" "Semi" "Ring" 
-      	       	 constrarg($a) constrarg($aplus) constrarg($amult) 
-                 constrarg($aone) constrarg($azero) constrarg($aeq) 
-                 constrarg($t) "." ] 
-  -> [(AddAbstractSemiRing $a $aplus $amult $aone $azero $aeq $t )]
-| addsetoidring [ "Add" "Setoid" "Ring"
-      	    constrarg($a) constrarg($aequiv) constrarg($asetth) constrarg($aplus) constrarg($amult) 
-	    constrarg($aone) constrarg($azero) constrarg($aopp) constrarg($aeq) constrarg($pm)
-	    constrarg($mm) constrarg($om) constrarg($t) "[" ne_constrarg_list($l) "]" "." ] 
-  -> [(AddSetoidRing $a $aequiv $asetth $aplus $amult $aone $azero $aopp $aeq $pm $mm $om $t
-      	 ($LIST $l))]
-| addsetoidsemiring [ "Add" "Semi" "Setoid" "Ring" 
-      	  constrarg($a) constrarg($aequiv) constrarg($asetth) constrarg($aplus)
-	  constrarg($amult) constrarg($aone) constrarg($azero) constrarg($aeq) 
-          constrarg($pm) constrarg($mm) constrarg($t) "[" ne_constrarg_list($l) "]" "." ] 
-  -> [(AddSemiRing $a $aequiv $asetth $aplus $amult $aone $azero $aeq $pm $mm $t
-      	   ($LIST $l))]
-.
-
 (* As an example, we provide an instantation for bool. *)
 (* Other instatiations are given in ArithRing and ZArithRing in the
    same directory *)
diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v
index bd1fc79b66..f2fe16f3a1 100644
--- a/contrib/ring/Ring_abstract.v
+++ b/contrib/ring/Ring_abstract.v
@@ -459,7 +459,7 @@ Save.
 
 Hint rew_isacs_aux : core := Extern 10 (eqT A ? ?) Rewrite isacs_aux_ok.
 
-Tactic Definition Solve1 := 
+Tactic Definition Solve1 v v0 H H0 := 
   Simpl; Elim (varlist_lt v v0); Simpl; Rewrite isacs_aux_ok;
     [Rewrite H; Simpl; Auto
     |Simpl in H0; Rewrite H0; Auto ].
@@ -475,7 +475,7 @@ Lemma signed_sum_merge_ok : (x,y:signed_sum)
 
   Auto.
 
-  Solve1.
+  Solve1 v v0 H H0.
 
   Simpl; Generalize (varlist_eq_prop v v0).
   Elim (varlist_eq v v0); Simpl.
@@ -491,7 +491,7 @@ Lemma signed_sum_merge_ok : (x,y:signed_sum)
   Rewrite (Th_plus_zero_left T).
   Reflexivity.
 
-  Solve1.
+  Solve1 v v0 H H0.
 
   Induction y; Intros.
 
@@ -509,13 +509,13 @@ Lemma signed_sum_merge_ok : (x,y:signed_sum)
   Rewrite (Th_plus_zero_left T).
   Reflexivity.
 
-  Solve1.
+  Solve1 v v0 H H0.
 
-  Solve1.
+  Solve1 v v0 H H0.
 
 Save.
 
-Tactic Definition Solve2 :=
+Tactic Definition Solve2 l v H :=
  	Elim (varlist_lt l v); Simpl; Rewrite isacs_aux_ok;
   	[ Auto
   	| Rewrite H; Auto ].
@@ -529,7 +529,7 @@ Proof.
   Trivial.
 
   Simpl; Intros.
-  Solve2.
+  Solve2 l v H.
 
   Simpl; Intros.
   Generalize (varlist_eq_prop l v).
@@ -542,7 +542,7 @@ Proof.
   Rewrite (Th_plus_zero_left T).
   Reflexivity.
 
-  Solve2.
+  Solve2 l v H.
 
 Save.
 
@@ -567,9 +567,9 @@ Proof.
   Auto.
 
   Simpl; Intros.
-  Solve2.
+  Solve2 l v H.
 
-  Simpl; Intros; Solve2.
+  Simpl; Intros; Solve2 l v H.
 
 Save.
 
diff --git a/contrib/ring/Setoid_ring.v b/contrib/ring/Setoid_ring.v
index 59ccc43d32..5a25fbc1fe 100644
--- a/contrib/ring/Setoid_ring.v
+++ b/contrib/ring/Setoid_ring.v
@@ -2,6 +2,7 @@ Require Export Setoid_ring_theory.
 Require Export Quote.
 Require Export Setoid_ring_normalize.
 
+(*
 Declare ML Module "ring".
 
 Grammar tactic simple_tactic : ast :=
@@ -25,3 +26,4 @@ Grammar vernac vernac : ast :=
   -> [(AddSemiSetoidRing $a $aequiv $asetth $aplus $amult $aone $azero $aeq $pm $mm $t
       	   ($LIST $l))]
 .
+*)
diff --git a/contrib/ring/g_quote.ml4 b/contrib/ring/g_quote.ml4
new file mode 100644
index 0000000000..fdbfb4a724
--- /dev/null
+++ b/contrib/ring/g_quote.ml4
@@ -0,0 +1,18 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id$ *)
+
+open Quote
+
+TACTIC EXTEND Quote
+  [ "Quote" ident(f) ] -> [ quote f [] ]
+| [ "Quote" ident(f) "[" ne_ident_list(lc) "]"] -> [ quote f lc ]
+END
diff --git a/contrib/ring/g_ring.ml4 b/contrib/ring/g_ring.ml4
new file mode 100644
index 0000000000..e971815b54
--- /dev/null
+++ b/contrib/ring/g_ring.ml4
@@ -0,0 +1,135 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id$ *)
+
+open Quote
+open Ring
+
+TACTIC EXTEND Ring
+  [ "Ring" constr_list(l) ] -> [ polynom l ]
+END
+
+(* The vernac commands "Add Ring" and co *)
+
+let cset_of_comarg_list l = 
+  List.fold_right ConstrSet.add (List.map constr_of l) ConstrSet.empty
+
+VERNAC COMMAND EXTEND AddRing
+  [ "Add" "Ring" 
+          constr(a) constr(aplus) constr(amult) constr(aone) constr(azero)
+          constr(aopp) constr(aeq) constr(t) "[" ne_constr_list(l) "]" ] 
+  -> [ add_theory true false false
+			 (constr_of a)
+			 None
+			 None
+			 None
+			 (constr_of aplus)
+			 (constr_of amult)
+			 (constr_of aone)
+			 (constr_of azero)
+			 (Some (constr_of aopp))
+			 (constr_of aeq)
+			 (constr_of t)
+			 (cset_of_comarg_list l) ]
+
+| [ "Add" "Semi" "Ring" 
+      	  constr(a) constr(aplus) constr(amult) constr(aone) constr(azero)
+          constr(aeq) constr(t) "[" ne_constr_list(l) "]" ] 
+  -> [ add_theory false false false
+			 (constr_of a)
+			 None
+			 None
+			 None
+			 (constr_of aplus)
+			 (constr_of amult)
+			 (constr_of aone)
+			 (constr_of azero)
+			 None
+			 (constr_of aeq)
+			 (constr_of t)
+			 (cset_of_comarg_list l) ]
+
+| [ "Add" "Abstract" "Ring" 
+    	  constr(a) constr(aplus) constr(amult) constr(aone)
+          constr(azero) constr(aopp) constr(aeq) constr(t) ] 
+  -> [ add_theory true true false
+			 (constr_of a)
+			 None
+			 None
+			 None
+			 (constr_of aplus)
+			 (constr_of amult)
+			 (constr_of aone)
+			 (constr_of azero)
+			 (Some (constr_of aopp))
+			 (constr_of aeq)
+			 (constr_of t)
+			 ConstrSet.empty ]
+
+| [ "Add" "Abstract" "Semi" "Ring" 
+          constr(a) constr(aplus) constr(amult) constr(aone)
+          constr(azero) constr(aeq) constr(t) ] 
+  -> [ add_theory false true false
+			 (constr_of a)
+			 None
+			 None
+			 None
+			 (constr_of aplus)
+			 (constr_of amult)
+			 (constr_of aone)
+			 (constr_of azero)
+			 None
+			 (constr_of aeq)
+			 (constr_of t)
+			 ConstrSet.empty ]
+
+| [ "Add" "Setoid" "Ring"
+      	  constr(a) constr(aequiv) constr(asetth) constr(aplus) constr(amult) 
+	  constr(aone) constr(azero) constr(aopp) constr(aeq) constr(pm)
+	  constr(mm) constr(om) constr(t) "[" ne_constr_list(l) "]" ] 
+  -> [ add_theory true false true
+			 (constr_of a)
+			 (Some (constr_of aequiv))
+			 (Some (constr_of asetth))
+			 (Some {
+			    plusm = (constr_of pm);
+			    multm = (constr_of mm);
+			    oppm = Some (constr_of om) })
+			 (constr_of aplus)
+			 (constr_of amult)
+			 (constr_of aone)
+			 (constr_of azero)
+			 (Some (constr_of aopp))
+			 (constr_of aeq)
+			 (constr_of t)
+			 (cset_of_comarg_list l) ]
+
+| [ "Add" "Semi" "Setoid" "Ring" 
+          constr(a) constr(aequiv) constr(asetth) constr(aplus)
+	  constr(amult) constr(aone) constr(azero) constr(aeq) 
+          constr(pm) constr(mm) constr(t) "[" ne_constr_list(l) "]" ] 
+  -> [ add_theory false false true
+			 (constr_of a)
+			 (Some (constr_of aequiv))
+			 (Some (constr_of asetth))
+			 (Some {
+			    plusm = (constr_of pm);
+			    multm = (constr_of mm);
+			    oppm = None })
+			 (constr_of aplus)
+			 (constr_of amult)
+			 (constr_of aone)
+			 (constr_of azero)
+			 None
+			 (constr_of aeq)
+			 (constr_of t)
+			 (cset_of_comarg_list l) ]
+END