diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-30 12:06:22 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-30 12:17:51 +0200 |
| commit | 49f144daf071dcb4e06be54315bd1e92dbe64d68 (patch) | |
| tree | f10d05b068b8596526101ae0ff3100182e8d9761 /tactics | |
| parent | f0a85b61cce59e55675df0ba6c9297166d757ce0 (diff) | |
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.
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 82d58074b..69cc87ee2 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) |