diff options
| -rw-r--r-- | tactics/tactics.ml | 6 | ||||
| -rw-r--r-- | test-suite/bugs/closed/5707.v | 12 | ||||
| -rw-r--r-- | vernac/himsg.ml | 2 |
3 files changed, 16 insertions, 4 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 67bc55d3f..32e366bc4 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4131,7 +4131,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 @@ -4165,7 +4165,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) @@ -4199,7 +4199,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 000000000..785844c66 --- /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. diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 2be10a039..e15911dd6 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1176,7 +1176,7 @@ let error_not_allowed_case_analysis isrec kind i = pr_inductive (Global.env()) (fst i) ++ str "." let error_not_allowed_dependent_analysis isrec i = - str "Dependent " ++ str (if isrec then "Induction" else "Case analysis") ++ + str "Dependent " ++ str (if isrec then "induction" else "case analysis") ++ strbrk " is not allowed for inductive definition " ++ pr_inductive (Global.env()) i ++ str "." |