diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 28e35cf97b..08eddef96c 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -931,7 +931,8 @@ let elimination_in_clause_scheme with_evars id elimclause indclause gl = let hyp = mkVar id in let hyp_typ = pf_type_of gl hyp in let hypclause = mk_clenv_from_n gl (Some 0) (hyp, hyp_typ) in - let elimclause'' = clenv_fchain ~allow_K:false hypmv elimclause' hypclause in + let elimclause'' = + clenv_fchain ~allow_K:false ~flags:elim_flags hypmv elimclause' hypclause in let new_hyp_typ = clenv_type elimclause'' in if eq_constr hyp_typ new_hyp_typ then errorlabstrm "general_rewrite_in" @@ -1959,7 +1960,7 @@ let compute_elim_sig ?elimc elimt = let nparams = Intset.cardinal (free_rels concl_with_args) in let preds,params = cut_list (List.length params_preds - nparams) params_preds in - (* A first approximation, further anlysis will tweak it *) + (* A first approximation, further analysis will tweak it *) let res = ref { empty_scheme with (* This fields are ok: *) elimc = elimc; elimt = elimt; concl = conclusion; |