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')

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/extraction/Extraction.v | 0
 plugins/extraction/vo.itarget   | 1 +
 plugins/funind/FunInd.v         | 0
 plugins/funind/vo.itarget       | 1 +
 4 files changed, 2 insertions(+)
 create mode 100644 plugins/extraction/Extraction.v
 create mode 100644 plugins/funind/FunInd.v

(limited to 'plugins')

diff --git a/plugins/extraction/Extraction.v b/plugins/extraction/Extraction.v
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/plugins/extraction/vo.itarget b/plugins/extraction/vo.itarget
index 9c30c5eb3e..3563f71dfc 100644
--- a/plugins/extraction/vo.itarget
+++ b/plugins/extraction/vo.itarget
@@ -1,3 +1,4 @@
+Extraction.vo
 ExtrHaskellBasic.vo
 ExtrHaskellNatNum.vo
 ExtrHaskellNatInt.vo
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