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 +--
 test-suite/bugs/closed/5372.v                  | 7 +++++++
 2 files changed, 8 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/bugs/closed/5372.v

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
diff --git a/test-suite/bugs/closed/5372.v b/test-suite/bugs/closed/5372.v
new file mode 100644
index 0000000000..2dc78d4c7f
--- /dev/null
+++ b/test-suite/bugs/closed/5372.v
@@ -0,0 +1,7 @@
+(* coq bug 5372: https://coq.inria.fr/bugs/show_bug.cgi?id=5372 *)
+Function odd (n:nat) :=
+  match n with
+  | 0 => false
+  | S n => true
+  end
+with even (n:nat) := false.
-- 
cgit v1.2.3