From ebc0870ca932acf0ceea5fe513e2ca40e74c2a02 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 6 Oct 2016 17:34:12 +0200
Subject: Moving the Ltac plugin to a pack-based one.

This is cumbersome, because now code may fail at link time if it's not
referring to the correct module name. Therefore, one has to add corresponding
open statements a the top of every file depending on a Ltac module. This
includes seemingly unrelated files that use EXTEND statements.
---
 plugins/funind/g_indfun.ml4 | 1 +
 plugins/funind/invfun.ml    | 1 +
 2 files changed, 2 insertions(+)

(limited to 'plugins/funind')

diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 6603a95a84..368b23be30 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 (*i camlp4deps: "grammar/grammar.cma" i*)
+open Ltac_plugin
 open Compat
 open Util
 open Term
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index c8b4e48337..70333b063d 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Ltac_plugin
 open Tacexpr
 open Declarations
 open CErrors
-- 
cgit v1.2.3


From 3602b909afc6eac0f150c9961a04b0bf50d8bbf0 Mon Sep 17 00:00:00 2001
From: Tej Chajed
Date: Fri, 10 Mar 2017 11:05:27 -0500
Subject: funind: Ignore missing info for current function

Fixes [Coq bug #5372](https://coq.inria.fr/bugs/show_bug.cgi?id=5372)
"Anomaly: Not a valid information when defining mutual fixpoints that
are not mutual with Function".
---
 plugins/funind/functional_principles_proofs.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index b0ffc775b5..0bbe4bb4cb 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1215,7 +1215,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
     let mk_fixes : tactic =
       let pre_info,infos = list_chop fun_num infos in
       match pre_info,infos with
-	| [],[] -> tclIDTAC
+	| _,[] -> tclIDTAC
 	| _, this_fix_info::others_infos ->
 	    let other_fix_infos =
 	      List.map
@@ -1231,7 +1231,6 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	    else
 	      Proofview.V82.of_tactic (Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1)
 		other_fix_infos 0)
-	| _ -> anomaly (Pp.str "Not a valid information")
     in
     let first_tac : tactic = (* every operations until fix creations *)
       tclTHENSEQ
-- 
cgit v1.2.3


From 6d2802075606dcddb02dd13cbaf38ff76f8bf242 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 23 Mar 2017 01:13:38 +0100
Subject: Add empty Extraction.v and FunInd.v to prepare landing of PR#220.

This way, after we merge PR#220, scripts can be fixed in a way that is
compatible with the 8.6 and trunk branches.
---
 plugins/funind/FunInd.v   | 0
 plugins/funind/vo.itarget | 1 +
 2 files changed, 1 insertion(+)
 create mode 100644 plugins/funind/FunInd.v

(limited to 'plugins/funind')

diff --git a/plugins/funind/FunInd.v b/plugins/funind/FunInd.v
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/plugins/funind/vo.itarget b/plugins/funind/vo.itarget
index 33c9683028..a17a5ec122 100644
--- a/plugins/funind/vo.itarget
+++ b/plugins/funind/vo.itarget
@@ -1 +1,2 @@
+FunInd.vo
 Recdef.vo
-- 
cgit v1.2.3


From 9c38a23ae84e1542ab1eeab6ded4201718ec1cf8 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 23 Mar 2017 14:50:56 +0100
Subject: Revert "Add empty Extraction.v and FunInd.v to prepare landing of
 PR#220."

This reverts commit 6d2802075606dcddb02dd13cbaf38ff76f8bf242, which is
an 8.6 only commit.
---
 plugins/funind/FunInd.v   | 0
 plugins/funind/vo.itarget | 1 -
 2 files changed, 1 deletion(-)
 delete mode 100644 plugins/funind/FunInd.v

(limited to 'plugins/funind')

diff --git a/plugins/funind/FunInd.v b/plugins/funind/FunInd.v
deleted file mode 100644
index e69de29bb2..0000000000
diff --git a/plugins/funind/vo.itarget b/plugins/funind/vo.itarget
index a17a5ec122..33c9683028 100644
--- a/plugins/funind/vo.itarget
+++ b/plugins/funind/vo.itarget
@@ -1,2 +1 @@
-FunInd.vo
 Recdef.vo
-- 
cgit v1.2.3