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.

9 files changed, 30 insertions, 64 deletions

diff --git a/ide/coq.lang b/ide/coq.lang
index a31eadc707..c65432bdb7 100644
--- a/ide/coq.lang
+++ b/ide/coq.lang
@@ -29,13 +29,12 @@
     <define-regex id="qualit">(\%{ident}\.)*\%{ident}</define-regex>
     <define-regex id="dot_sep">\.(\s|\z)</define-regex>
     <define-regex id="bullet">([-+*]+|{)(\s|\z)|}(\s*})*</define-regex>
-    <define-regex id="assume">(?'gal0'Assume)\%{space}\[\%{ident}*\]\%{space}</define-regex>
     <define-regex id="single_decl">Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion</define-regex>
     <define-regex id="mult_decl">Hypothes[ie]s|Axiom(s)?|Variable(s)?|Parameter(s)?|Context|Implicit\%{space}Type(s)?</define-regex>
     <define-regex id="locality">((Local|Global)\%{space})?</define-regex>
     <define-regex id="begin_proof">Theorem|Lemma|Fact|Remark|Corollary|Proposition|Property</define-regex>
     <define-regex id="end_proof">Qed|Defined|Admitted|Abort|Save</define-regex>
-    <define-regex id="decl_head">((\%{assume})?(?'gal'\%{locality}(Program\%{space})?(\%{single_decl}|\%{begin_proof}))\%{space}(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}\%{ident})*))|(?'gal2'Goal)</define-regex>
+    <define-regex id="decl_head">((?'gal'\%{locality}(Program\%{space})?(\%{single_decl}|\%{begin_proof}))\%{space}(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}\%{ident})*))|(?'gal2'Goal)</define-regex>
 
     <!-- Strings, with '""' an escape sequence -->
     <context id="string" style-ref="string" class="string">
@@ -107,7 +106,6 @@
           <end>\%{dot_sep}</end>
           <include>
             <context sub-pattern="id" where="start" style-ref="identifier"/>
-            <context sub-pattern="gal0" where="start" style-ref="gallina-keyword"/>
             <context sub-pattern="gal" where="start" style-ref="gallina-keyword"/>
             <context sub-pattern="gal2" where="start" style-ref="gallina-keyword"/>
             <context sub-pattern="id_list" where="start" style-ref="identifier"/>
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 2f2f973761..d7b269a1de 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -303,14 +303,10 @@ type vernac_expr =
   | VernacExactProof of constr_expr
   | VernacAssumption of (locality option * assumption_object_kind) *
       inline * simple_binder with_coercion list
-  | VernacInductive of
-      bool (*[false] => assume positive*) *
-      private_flag * inductive_flag * (inductive_expr * decl_notation list) list
+  | VernacInductive of private_flag * inductive_flag * (inductive_expr * decl_notation list) list
   | VernacFixpoint of
-      Declarations.typing_flags *
       locality option * (fixpoint_expr * decl_notation list) list
   | VernacCoFixpoint of
-      Declarations.typing_flags *
       locality option * (cofixpoint_expr * decl_notation list) list
   | VernacScheme of (lident option * scheme) list
   | VernacCombinedScheme of lident * lident list
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 ] ]
   ;
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 91fcb3f8b9..61f03d6f22 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -166,7 +166,7 @@ VERNAC COMMAND EXTEND Function
            | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in
          match
            Vernac_classifier.classify_vernac
-             (Vernacexpr.VernacFixpoint({Declarations.check_guarded=true},None, List.map snd recsl))
+             (Vernacexpr.VernacFixpoint(None, List.map snd recsl))
          with
          | Vernacexpr.VtSideff ids, _ when hard ->
              Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index b4febba668..f1c379ecc6 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1435,7 +1435,7 @@ let do_build_inductive
 	in
 	let msg =
 	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,false,Decl_kinds.Finite,repacked_rel_inds))
+	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds))
 	    ++ fnl () ++
 	    msg
 	in
@@ -1450,7 +1450,7 @@ let do_build_inductive
 	in
 	let msg =
 	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,false,Decl_kinds.Finite,repacked_rel_inds))
+	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds))
 	    ++ fnl () ++
 	    Errors.print reraise
 	in
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 8a8521ccc1..832c08fe0e 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -399,15 +399,6 @@ module Make
     | None -> mt ()
     | Some i -> spc () ++ str "|" ++ spc () ++ int i
 
-  let pr_assume ?(positive=false) ?(guarded=false) () =
-    let assumed =
-      (if guarded then [str"Guarded"] else []) @
-      (if positive then [str"Positive"] else [])
-    in
-    match assumed with
-    | [] -> mt ()
-    | l -> keyword"Assume" ++ spc() ++ str"[" ++ prlist (fun x->x) l ++ str"]" ++ spc()
-
 (**************************************)
 (* Pretty printer for vernac commands *)
 (**************************************)
@@ -770,7 +761,7 @@ module Make
               (pr_assumption_token (n > 1) stre ++ spc() ++
                  pr_ne_params_list pr_lconstr_expr l)
           )
-        | VernacInductive (chk,p,f,l) ->
+        | VernacInductive (p,f,l) ->
           let pr_constructor (coe,(id,c)) =
             hov 2 (pr_lident id ++ str" " ++
                      (if coe then str":>" else str":") ++
@@ -806,7 +797,7 @@ module Make
               (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
           )
 
-        | VernacFixpoint (flags,local, recs) ->
+        | VernacFixpoint (local, recs) ->
           let local = match local with
             | Some Discharge -> "Let "
             | Some Local -> "Local "
@@ -821,11 +812,11 @@ module Make
                 prlist (pr_decl_notation pr_constr) ntn
           in
           return (
-            hov 0 (pr_assume ~guarded:flags.Declarations.check_guarded ()++str local ++ keyword "Fixpoint" ++ spc () ++
+            hov 0 (str local ++ keyword "Fixpoint" ++ spc () ++
                      prlist_with_sep (fun _ -> fnl () ++ keyword "with" ++ spc ()) pr_onerec recs)
           )
 
-        | VernacCoFixpoint (flags,local, corecs) ->
+        | VernacCoFixpoint (local, corecs) ->
           let local = match local with
             | Some Discharge -> keyword "Let" ++ spc ()
             | Some Local -> keyword "Local" ++ spc ()
@@ -838,7 +829,7 @@ module Make
               prlist (pr_decl_notation pr_constr) ntn
           in
           return (
-            hov 0 (pr_assume ~guarded:flags.Declarations.check_guarded ()++local ++ keyword "CoFixpoint" ++ spc() ++
+            hov 0 (local ++ keyword "CoFixpoint" ++ spc() ++
                      prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onecorec corecs)
           )
         | VernacScheme l ->
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index 4f014be2de..9edc1f1c70 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -580,7 +580,7 @@ let rec tmpp v loc =
       let l = match l with Some x -> x | None -> Decl_kinds.Global in
       let kind = string_of_assumption_kind l a many in
       xmlAssumption kind loc exprs
-  | VernacInductive (_,_, _, iednll) ->
+  | VernacInductive (_, _, iednll) ->
       let kind =
         let (_, _, _, k, _),_ = List.hd iednll in
 	  begin
@@ -598,14 +598,14 @@ let rec tmpp v loc =
             (fun (ie, dnl) -> (pp_inductive_expr ie) @
                               (List.map pp_decl_notation dnl)) iednll) in
       xmlInductive kind loc exprs
-  | VernacFixpoint (_,_, fednll) ->
+  | VernacFixpoint (_, fednll) ->
       let exprs =
         List.flatten (* should probably not be flattened *)
           (List.map
             (fun (fe, dnl) -> (pp_fixpoint_expr fe) @
                               (List.map pp_decl_notation dnl)) fednll) in
       xmlFixpoint exprs
-  | VernacCoFixpoint (_,_, cfednll) ->
+  | VernacCoFixpoint (_, cfednll) ->
       (* Nota: it is like VernacFixpoint without so could be merged *)
       let exprs =
         List.flatten (* should probably not be flattened *)
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 574cc0044c..2b5eb86834 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -125,14 +125,14 @@ let rec classify_vernac e =
           CList.map_filter (function (Some(_,i), _) -> Some i | _ -> None) l in
         VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
     | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater
-    | VernacFixpoint (_,_,l) ->
+    | VernacFixpoint (_,l) ->
         let ids, open_proof =
           List.fold_left (fun (l,b) (((_,id),_,_,_,p),_) ->
             id::l, b || p = None) ([],false) l in
         if open_proof
         then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
         else VtSideff ids, VtLater
-    | VernacCoFixpoint (_,_,l) ->
+    | VernacCoFixpoint (_,l) ->
         let ids, open_proof =
           List.fold_left (fun (l,b) (((_,id),_,_,p),_) ->
             id::l, b || p = None) ([],false) l in
@@ -144,7 +144,7 @@ let rec classify_vernac e =
         let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd l) l) in
         VtSideff ids, VtLater    
     | VernacDefinition (_,(_,id),DefineBody _) -> VtSideff [id], VtLater
-    | VernacInductive (_,_,_,l) ->
+    | VernacInductive (_,_,l) ->
         let ids = List.map (fun (((_,(_,id)),_,_,_,cl),_) -> id :: match cl with
         | Constructors l -> List.map (fun (_,((_,id),_)) -> id) l
         | RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 40dfa1b9a5..a5e771d75d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1856,6 +1856,7 @@ let vernac_load interp fname =
   try while true do interp (snd (parse_sentence input)) done
   with End_of_input -> ()
 
+let all_checks = { Declarations.check_guarded = true }
 
 (* "locality" is the prefix "Local" attribute, while the "local" component
  * is the outdated/deprecated "Local" attribute of some vernacular commands
@@ -1894,9 +1895,9 @@ let interp ?proof locality poly c =
   | VernacEndProof e -> vernac_end_proof ?proof e
   | VernacExactProof c -> vernac_exact_proof c
   | VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl
-  | VernacInductive (chk,priv,finite,l) -> vernac_inductive chk poly priv finite l
-  | VernacFixpoint (flags,local, l) -> vernac_fixpoint ~flags locality poly local l
-  | VernacCoFixpoint (flags,local, l) -> vernac_cofixpoint ~flags locality poly local l
+  | VernacInductive (priv,finite,l) -> vernac_inductive true poly priv finite l
+  | VernacFixpoint (local, l) -> vernac_fixpoint locality ~flags:all_checks poly local l
+  | VernacCoFixpoint (local, l) -> vernac_cofixpoint ~flags:all_checks locality poly local l
   | VernacScheme l -> vernac_scheme l
   | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l
   | VernacUniverse l -> vernac_universe l