diff options
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/auto.ml | 1 | ||||
-rw-r--r-- | tactics/class_tactics.ml4 | 3 | ||||
-rw-r--r-- | tactics/setoid_replace.ml | 2 | ||||
-rw-r--r-- | tactics/tacticals.ml | 4 | ||||
-rw-r--r-- | tactics/tactics.ml | 10 |
5 files changed, 15 insertions, 5 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 66fde8f6b..8823efe0b 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -586,6 +586,7 @@ open Unification let auto_unif_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; use_metas_eagerly = false; + use_types = false; modulo_delta = empty_transparent_state; } diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 4319a1d3d..72bc85c2f 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -72,6 +72,7 @@ open Unification let auto_unif_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; use_metas_eagerly = true; + use_types = true; modulo_delta = var_full_transparent_state; } @@ -631,6 +632,7 @@ let decompose_setoid_eqhyp env sigma c left2right = let rewrite_unif_flags = { Unification.modulo_conv_on_closed_terms = None; Unification.use_metas_eagerly = true; + Unification.use_types = true; Unification.modulo_delta = empty_transparent_state; } @@ -639,6 +641,7 @@ let conv_transparent_state = (Idpred.empty, Cpred.full) let rewrite2_unif_flags = { Unification.modulo_conv_on_closed_terms = Some conv_transparent_state; Unification.use_metas_eagerly = true; + Unification.use_types = true; Unification.modulo_delta = empty_transparent_state; } diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index dc8ff2b9c..b5710c966 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -1734,12 +1734,14 @@ let check_evar_map_of_evars_defs evd = let rewrite_unif_flags = { modulo_conv_on_closed_terms = None; use_metas_eagerly = true; + use_types = true; modulo_delta = empty_transparent_state; } let rewrite2_unif_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; use_metas_eagerly = true; + use_types = true; modulo_delta = empty_transparent_state; } diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index dd8aa1294..1bd65ecdf 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -329,7 +329,7 @@ let general_elim_then_using mk_elim ind indclause gl = let elim = mk_elim ind gl in (* applying elimination_scheme just a little modified *) - let indclause' = clenv_match_args indbindings indclause in + let indclause' = clenv_match_args true indbindings indclause in let elimclause = mk_clenv_from gl (elim,pf_type_of gl elim) in let indmv = match kind_of_term (last_arg elimclause.templval.Evd.rebus) with @@ -350,7 +350,7 @@ let general_elim_then_using mk_elim error ("The elimination combinator " ^ name_elim ^ " is not known") in let elimclause' = clenv_fchain indmv elimclause indclause' in - let elimclause' = clenv_match_args elimbindings elimclause' in + let elimclause' = clenv_match_args true elimbindings elimclause' in let branchsigns = compute_construtor_signatures isrec ind in let brnames = compute_induction_names (Array.length branchsigns) allnames in let after_tac ce i gl = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index d3f7cc5f1..cd8ad4c14 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -551,6 +551,7 @@ let last_arg c = match kind_of_term c with let elim_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; use_metas_eagerly = true; + use_types = true; modulo_delta = empty_transparent_state; } @@ -672,9 +673,10 @@ let simplest_case c = general_case_analysis false (c,NoBindings) (* Resolution with missing arguments *) -let general_apply with_delta with_destruct with_evars (c,lbind) gl = +let general_apply with_delta_and_types with_destruct with_evars (c,lbind) gl = let flags = - if with_delta then default_unify_flags else default_no_delta_unify_flags in + if with_delta_and_types then default_unify_flags + else simple_apply_unify_flags in (* The actual type of the theorem. It will be matched against the goal. If this fails, then the head constant will be unfolded step by step. *) @@ -684,7 +686,9 @@ let general_apply with_delta with_destruct with_evars (c,lbind) gl = let try_apply thm_ty nprod = let n = nb_prod thm_ty - nprod in if n<0 then error "Apply: theorem has not enough premisses."; - let clause = make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in + let clause = + make_clenv_binding_apply with_delta_and_types (Some n) gl (c,thm_ty) lbind + in Clenvtac.res_pf clause ~with_evars:with_evars ~flags:flags gl in try try_apply thm_ty0 concl_nprod with PretypeError _|RefinerError _|UserError _|Failure _ as exn -> |