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.
---
 plugins/funind/g_indfun.ml4             | 2 +-
 plugins/funind/glob_term_to_relation.ml | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/funind')

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
-- 
cgit v1.2.3