diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 7 | ||||
| -rw-r--r-- | tactics/class_tactics.ml4 | 5 | ||||
| -rw-r--r-- | tactics/equality.ml | 11 | ||||
| -rw-r--r-- | tactics/rewrite.ml4 | 15 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
5 files changed, 25 insertions, 15 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 18e71661ff..af9420a245 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -840,11 +840,12 @@ open Unification let auto_unif_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; - use_metas_eagerly = false; + use_metas_eagerly_in_conv_on_closed_terms = false; modulo_delta = empty_transparent_state; modulo_delta_types = full_transparent_state; resolve_evars = true; - use_evars_pattern_unification = false; + use_pattern_unification = false; + use_meta_bound_pattern_unification = true; frozen_evars = ExistentialSet.empty; restrict_conv_on_strict_subterms = false; (* Compat *) modulo_betaiota = false; @@ -971,7 +972,7 @@ and my_find_search mod_delta = else my_find_search_nodelta and my_find_search_delta db_list local_db hdc concl = - let flags = {auto_unif_flags with use_metas_eagerly = true} in + let flags = {auto_unif_flags with use_metas_eagerly_in_conv_on_closed_terms = true} in let f = hintmap_of hdc concl in if occur_existential concl then list_map_append diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index b460222b95..aed9f59857 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -74,11 +74,12 @@ open Unification let auto_unif_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; - use_metas_eagerly = true; + use_metas_eagerly_in_conv_on_closed_terms = true; modulo_delta = var_full_transparent_state; modulo_delta_types = full_transparent_state; resolve_evars = false; - use_evars_pattern_unification = true; + use_pattern_unification = true; + use_meta_bound_pattern_unification = true; frozen_evars = ExistentialSet.empty; restrict_conv_on_strict_subterms = false; (* ? *) modulo_betaiota = true; diff --git a/tactics/equality.ml b/tactics/equality.ml index d2970603ea..3a40994f8c 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -82,11 +82,12 @@ type conditions = let rewrite_unif_flags = { Unification.modulo_conv_on_closed_terms = None; - Unification.use_metas_eagerly = true; + Unification.use_metas_eagerly_in_conv_on_closed_terms = true; Unification.modulo_delta = empty_transparent_state; Unification.modulo_delta_types = empty_transparent_state; Unification.resolve_evars = true; - Unification.use_evars_pattern_unification = true; + Unification.use_pattern_unification = true; + Unification.use_meta_bound_pattern_unification = true; Unification.frozen_evars = ExistentialSet.empty; Unification.restrict_conv_on_strict_subterms = false; Unification.modulo_betaiota = false; @@ -142,17 +143,19 @@ let rewrite_conv_closed_unif_flags = { (* We have this flag for historical reasons, it has e.g. the consequence *) (* to rewrite "?x+2" in "y+(1+1)=0" or to rewrite "?x+?x" in "2+(1+1)=0" *) - Unification.use_metas_eagerly = true; + Unification.use_metas_eagerly_in_conv_on_closed_terms = true; (* Combined with modulo_conv_on_closed_terms, this flag allows since 8.2 *) (* to rewrite e.g. "?x+(2+?x)" in "1+(1+2)=0" *) Unification.modulo_delta = empty_transparent_state; Unification.modulo_delta_types = full_transparent_state; Unification.resolve_evars = false; - Unification.use_evars_pattern_unification = true; + Unification.use_pattern_unification = true; (* To rewrite "?n x y" in "y+x=0" when ?n is *) (* a preexisting evar of the goal*) + Unification.use_meta_bound_pattern_unification = true; + Unification.frozen_evars = ExistentialSet.empty; (* This is set dynamically *) diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 821284ec7f..5400827bcf 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -302,11 +302,12 @@ let rewrite_transparent_state () = let rewrite_unif_flags = { Unification.modulo_conv_on_closed_terms = None; - Unification.use_metas_eagerly = true; + Unification.use_metas_eagerly_in_conv_on_closed_terms = true; Unification.modulo_delta = empty_transparent_state; Unification.modulo_delta_types = full_transparent_state; Unification.resolve_evars = true; - Unification.use_evars_pattern_unification = true; + Unification.use_pattern_unification = true; + Unification.use_meta_bound_pattern_unification = true; Unification.frozen_evars = ExistentialSet.empty; Unification.restrict_conv_on_strict_subterms = false; Unification.modulo_betaiota = false; @@ -316,11 +317,12 @@ let rewrite_unif_flags = { let rewrite2_unif_flags = { Unification.modulo_conv_on_closed_terms = Some conv_transparent_state; - Unification.use_metas_eagerly = true; + Unification.use_metas_eagerly_in_conv_on_closed_terms = true; Unification.modulo_delta = empty_transparent_state; Unification.modulo_delta_types = conv_transparent_state; Unification.resolve_evars = true; - Unification.use_evars_pattern_unification = true; + Unification.use_pattern_unification = true; + Unification.use_meta_bound_pattern_unification = true; Unification.frozen_evars = ExistentialSet.empty; Unification.restrict_conv_on_strict_subterms = false; Unification.modulo_betaiota = true; @@ -331,11 +333,12 @@ let rewrite2_unif_flags = let general_rewrite_unif_flags () = let ts = rewrite_transparent_state () in { Unification.modulo_conv_on_closed_terms = Some ts; - Unification.use_metas_eagerly = true; + Unification.use_metas_eagerly_in_conv_on_closed_terms = true; Unification.modulo_delta = ts; Unification.modulo_delta_types = ts; Unification.resolve_evars = true; - Unification.use_evars_pattern_unification = true; + Unification.use_pattern_unification = true; + Unification.use_meta_bound_pattern_unification = true; Unification.frozen_evars = ExistentialSet.empty; Unification.restrict_conv_on_strict_subterms = false; Unification.modulo_betaiota = true; diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 060cd94a87..97928c87c2 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -842,6 +842,7 @@ type conjunction_status = let make_projection sigma params cstr sign elim i n c = let elim = match elim with | NotADefinedRecordUseScheme elim -> + (* bugs: goes from right to left when i increases! *) let (na,b,t) = List.nth cstr.cs_args i in let b = match b with None -> mkRel (i+1) | Some b -> b in let branch = it_mkLambda_or_LetIn b cstr.cs_args in @@ -856,6 +857,7 @@ let make_projection sigma params cstr sign elim i n c = else None | DefinedRecord l -> + (* goes from left to right when i increases! *) match List.nth l i with | Some proj -> let t = Typeops.type_of_constant (Global.env()) proj in |