From 49f144daf071dcb4e06be54315bd1e92dbe64d68 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 30 Aug 2017 12:06:22 +0200
Subject: Fixing part of #5707 (allowing destruct to use non dependent case
 analysis).

The fix covers the case of a non-dependent goal with unavailable
dependent case analysis: destruct was not seeing that it could still
use non-dependent case analysis.
---
 tactics/tactics.ml            |  6 +++---
 test-suite/bugs/closed/5707.v | 12 ++++++++++++
 2 files changed, 15 insertions(+), 3 deletions(-)
 create mode 100644 test-suite/bugs/closed/5707.v

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 82d58074bc..69cc87ee29 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4078,7 +4078,7 @@ let guess_elim isrec dep s hyp0 gl =
       let env = Tacmach.New.pf_env gl in
       let sigma = Tacmach.New.project gl in
       let u = EInstance.kind (Tacmach.New.project gl) u in
-      if use_dependent_propositions_elimination () && dep
+      if use_dependent_propositions_elimination () && dep = Some true
       then
         let (sigma, ind) = build_case_analysis_scheme env sigma (mind, u) true s in
         let ind = EConstr.of_constr ind in
@@ -4112,7 +4112,7 @@ let find_induction_type isrec elim hyp0 gl =
     | None ->
        let sort = Tacticals.New.elimination_sort_of_goal gl in
        let _, (elimc,elimt),_ = 
-	 guess_elim isrec (* dummy: *) true sort hyp0 gl in
+	 guess_elim isrec None sort hyp0 gl in
 	let scheme = compute_elim_sig sigma ~elimc elimt in
 	(* We drop the scheme waiting to know if it is dependent *)
 	scheme, ElimOver (isrec,hyp0)
@@ -4146,7 +4146,7 @@ let get_eliminator elim dep s gl =
   | ElimUsing (elim,indsign) ->
       Tacmach.New.project gl, (* bugged, should be computed *) true, elim, indsign
   | ElimOver (isrec,id) ->
-      let evd, (elimc,elimt),_ as elims = guess_elim isrec dep s id gl in
+      let evd, (elimc,elimt),_ as elims = guess_elim isrec (Some dep) s id gl in
       let _, (l, s) = compute_elim_signature elims id in
       let branchlengthes = List.map (fun d -> assert (RelDecl.is_local_assum d); pi1 (decompose_prod_letin (Tacmach.New.project gl) (RelDecl.get_type d)))
                                     (List.rev s.branches)
diff --git a/test-suite/bugs/closed/5707.v b/test-suite/bugs/closed/5707.v
new file mode 100644
index 0000000000..785844c66d
--- /dev/null
+++ b/test-suite/bugs/closed/5707.v
@@ -0,0 +1,12 @@
+(* Destruct and primitive projections *)
+
+(* Checking the (superficial) part of #5707:
+   "destruct" should be able to use non-dependent case analysis when
+   dependent case analysis is not available and unneeded *)
+
+Set Primitive Projections.
+
+Inductive foo := Foo { proj1 : nat; proj2 : nat }.
+
+Goal forall x : foo, True.
+Proof. intros x. destruct x.
-- 
cgit v1.2.3