diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-09-15 10:00:35 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-09-15 10:00:35 +0200 |
| commit | 6c678a68c081ce24bbdcb092db3f57ef7e171dac (patch) | |
| tree | d963048adb529427abc19d49f453f276b720df7d /tactics | |
| parent | eb439843c5fd3841aa22b36453c49d9dd07bd770 (diff) | |
| parent | 49f144daf071dcb4e06be54315bd1e92dbe64d68 (diff) | |
Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" Inductive-keyworded record failing even on non-dependent goal)
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 6 |
1 files changed, 3 insertions, 3 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) |