diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 1 | ||||
| -rw-r--r-- | tactics/class_tactics.ml4 | 1 | ||||
| -rw-r--r-- | tactics/equality.ml | 32 | ||||
| -rw-r--r-- | tactics/rewrite.ml4 | 3 |
4 files changed, 29 insertions, 8 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 4c00a60d00..6780ae2fcf 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -845,6 +845,7 @@ let auto_unif_flags = { modulo_delta_types = full_transparent_state; resolve_evars = true; use_evars_pattern_unification = false; + frozen_evars = ExistentialSet.empty; modulo_betaiota = false; modulo_eta = true; allow_K_in_toplevel_higher_order_unification = false diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 3b193f6d93..3f4e773eca 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -79,6 +79,7 @@ let auto_unif_flags = { modulo_delta_types = full_transparent_state; resolve_evars = false; use_evars_pattern_unification = true; + frozen_evars = ExistentialSet.empty; modulo_betaiota = true; modulo_eta = true; allow_K_in_toplevel_higher_order_unification = false diff --git a/tactics/equality.ml b/tactics/equality.ml index 3b734b4c64..f6e8837f8b 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -87,12 +87,25 @@ let rewrite_unif_flags = { Unification.modulo_delta_types = empty_transparent_state; Unification.resolve_evars = true; Unification.use_evars_pattern_unification = true; + Unification.frozen_evars = ExistentialSet.empty; Unification.modulo_betaiota = false; Unification.modulo_eta = true; Unification.allow_K_in_toplevel_higher_order_unification = false (* allow_K does not matter in practice because calls w_typed_unify *) } +let freeze_initial_evars sigma flags clause = + (* We take evars of the type: this may include old evars! For excluding *) + (* all old evars, including the ones occurring in the rewriting lemma, *) + (* we would have to take the clenv_value *) + let newevars = Evd.collect_evars (clenv_type clause) in + let evars = + fold_undefined (fun evk _ evars -> + if ExistentialSet.mem evk newevars then evars + else ExistentialSet.add evk evars) + sigma ExistentialSet.empty in + { flags with Unification.frozen_evars = evars } + let side_tac tac sidetac = match sidetac with | None -> tac @@ -110,8 +123,9 @@ let instantiate_lemma_all env sigma gl c ty l l2r concl = let try_occ (evd', c') = clenv_pose_dependent_evars true {eqclause with evd = evd'} in + let flags = freeze_initial_evars sigma rewrite_unif_flags eqclause in let occs = - Unification.w_unify_to_subterm_all ~flags:rewrite_unif_flags env + Unification.w_unify_to_subterm_all ~flags env ((if l2r then c1 else c2),concl) eqclause.evd in List.map try_occ occs @@ -129,20 +143,22 @@ let rewrite_conv_closed_unif_flags = { Unification.modulo_delta_types = full_transparent_state; Unification.resolve_evars = false; Unification.use_evars_pattern_unification = true; + Unification.frozen_evars = ExistentialSet.empty; Unification.modulo_betaiota = false; Unification.modulo_eta = true; Unification.allow_K_in_toplevel_higher_order_unification = false } -let rewrite_elim with_evars c e = - general_elim_clause_gen - (elimination_clause_scheme with_evars ~flags:rewrite_conv_closed_unif_flags) - c e +let rewrite_elim with_evars c e gl = + let flags = + freeze_initial_evars (project gl) rewrite_conv_closed_unif_flags c in + general_elim_clause_gen (elimination_clause_scheme with_evars ~flags) c e gl -let rewrite_elim_in with_evars id c e = +let rewrite_elim_in with_evars id c e gl = + let flags = + freeze_initial_evars (project gl) rewrite_conv_closed_unif_flags c in general_elim_clause_gen - (elimination_in_clause_scheme with_evars - ~flags:rewrite_conv_closed_unif_flags id) c e + (elimination_in_clause_scheme with_evars ~flags id) c e gl (* Ad hoc asymmetric general_elim_clause *) let general_elim_clause with_evars cls rew elim = diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 41ed88d2f7..b8ebf84a61 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -307,6 +307,7 @@ let rewrite_unif_flags = { Unification.modulo_delta_types = full_transparent_state; Unification.resolve_evars = true; Unification.use_evars_pattern_unification = true; + Unification.frozen_evars = ExistentialSet.empty; Unification.modulo_betaiota = false; Unification.modulo_eta = true; Unification.allow_K_in_toplevel_higher_order_unification = true @@ -319,6 +320,7 @@ let rewrite2_unif_flags = Unification.modulo_delta_types = conv_transparent_state; Unification.resolve_evars = true; Unification.use_evars_pattern_unification = true; + Unification.frozen_evars = ExistentialSet.empty; Unification.modulo_betaiota = true; Unification.modulo_eta = true; Unification.allow_K_in_toplevel_higher_order_unification = true @@ -332,6 +334,7 @@ let general_rewrite_unif_flags () = Unification.modulo_delta_types = ts; Unification.resolve_evars = true; Unification.use_evars_pattern_unification = true; + Unification.frozen_evars = ExistentialSet.empty; Unification.modulo_betaiota = true; Unification.modulo_eta = true; Unification.allow_K_in_toplevel_higher_order_unification = true } |