Nettoyage

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

1 files changed, 10 insertions, 26 deletions

diff --git a/contrib/ring/Setoid_ring.v b/contrib/ring/Setoid_ring.v
index 5a25fbc1f..567517e98 100644
--- a/contrib/ring/Setoid_ring.v
+++ b/contrib/ring/Setoid_ring.v
@@ -1,29 +1,13 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
 Require Export Setoid_ring_theory.
 Require Export Quote.
 Require Export Setoid_ring_normalize.
-
-(*
-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 := 
-| 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) "]" "." ] 
-  -> [(AddSemiSetoidRing $a $aequiv $asetth $aplus $amult $aone $azero $aeq $pm $mm $t
-      	   ($LIST $l))]
-.
-*)