From dcf4d3e28813e09fc71f974b79ddf42d2e525976 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 5 Jun 2016 21:50:22 +0200
Subject: Remove the syntax changes introduced by this branch.

We decided to only export the API, so that an external plugin can provide
this feature without having to merge it in current Coq trunk. This postpones
the attribute implementation in vernacular commands after 8.6.
---
 parsing/g_vernac.ml4 | 40 ++++++++++------------------------------
 1 file changed, 10 insertions(+), 30 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3ad5e77fcf..e8a1b512c0 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -71,19 +71,6 @@ let make_bullet s =
   | '*' -> Star n
   | _ -> assert false
 
-type nl_assumption =
-  | Positive
-  | Guarded
-let eq_nl_assumption x y =
-  match x,y with
-  | Positive,Positive -> true
-  | Guarded,Guarded -> true
-  | _ , _ -> false
-let check_positivity l =
-  not (List.mem_f eq_nl_assumption Positive l)
-let check_guardedness l =
-  not (List.mem_f eq_nl_assumption Guarded l)
-
 let default_command_entry =
   Gram.Entry.of_parser "command_entry"
     (fun strm -> Gram.parse_tokens_after_filter (get_command_entry ()) strm)
@@ -213,19 +200,19 @@ GEXTEND Gram
       | IDENT "Let"; id = identref; b = def_body ->
           VernacDefinition ((Some Discharge, Definition), id, b)
       (* Gallina inductive declarations *)
-      | priv = private_token; a = assume_token; f = finite_token;
+      | priv = private_token; f = finite_token;
         indl = LIST1 inductive_definition SEP "with" ->
 	  let (k,f) = f in
 	  let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
-          VernacInductive (check_positivity a,priv,f,indl)
-      | "Fixpoint"; a=assume_token; recs = LIST1 rec_definition SEP "with" ->
-          VernacFixpoint ({Declarations.check_guarded=check_guardedness a},None, recs)
-      | IDENT "Let"; "Fixpoint"; a=assume_token; recs = LIST1 rec_definition SEP "with" ->
-          VernacFixpoint ({Declarations.check_guarded=check_guardedness a},Some Discharge, recs)
-      | "CoFixpoint"; a=assume_token; corecs = LIST1 corec_definition SEP "with" ->
-          VernacCoFixpoint ({Declarations.check_guarded=check_guardedness a},None, corecs)
-      | IDENT "Let"; "CoFixpoint"; a=assume_token; corecs = LIST1 corec_definition SEP "with" ->
-          VernacCoFixpoint ({Declarations.check_guarded=check_guardedness a},Some Discharge, corecs)
+          VernacInductive (priv,f,indl)
+      | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
+          VernacFixpoint (None, recs)
+      | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
+          VernacFixpoint (Some Discharge, recs)
+      | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
+          VernacCoFixpoint (None, corecs)
+      | IDENT "Let"; "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
+          VernacCoFixpoint (Some Discharge, corecs)
       | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l
       | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from";
 	      l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l)
@@ -282,13 +269,6 @@ GEXTEND Gram
       | IDENT "Structure" -> (Structure,BiFinite)
       | IDENT "Class" -> (Class true,BiFinite) ] ]
   ;
-  assume_token:
-    [ [ IDENT "Assume"; "[" ; l=LIST1 nl_assumption ; "]" -> l | -> [] ] ]
-  ;
-  nl_assumption:
-    [ [ IDENT "Positive" -> Positive
-      | IDENT "Guarded" -> Guarded ] ]
-  ;
   private_token:
     [ [ IDENT "Private" -> true | -> false ] ]
   ;
-- 
cgit v1.2.3