=?utf-8?q?D=C3=A9sinterdiction=20de=20GDELETE=5FRULE=20dans=20pcoq.ml4.=20Malheureusement,=20je=20ne

=20sais=20pas=20permettre=20que=20GDELETE=5FRULE=20soit=20appelable=20pendant=20une=20section
=20sans=20causer=20de=20potentiels=20soucis=20(bien=20que=20je=20trouve=20qu'il=20faille=20un
=20esprit=20sacr=C3=A9ment=20pervers=20pour=20faire=20Declare=20ML=20Module=20dans=20une=20section).?=
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 8bit

Je suppose qu'on est dans le même esprit d'information trop partielle
que pour les notations aux niveaux 8, 99 et 200.


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

1 files changed, 9 insertions, 1 deletions

diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index b7928b3b5..1c9e1e46b 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -134,7 +134,15 @@ module Gram =
       :: !camlp4_state;
       G.extend e pos rls
     let delete_rule e pil =
-      errorlabstrm "Pcoq.delete_rule" (str "GDELETE_RULE forbidden.")
+      (* spiwack: if you use load an ML module which contains GDELETE_RULE
+	  in a section, God kills a kitty. As it would corrupt remove_grammars.
+          There does not seem to be a good way to undo a delete rule. As deleting
+	  takes fewer arguments than extending. The production rule isn't returned
+	  by delete_rule. If we could retrieve the necessary information, then
+	  ByGEXTEND provides just the framework we need to allow this in section.
+	  I'm not entirely sure it makes sense, but at least it would be more correct.
+          *)
+      G.delete_rule e pil
   end