diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 2 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 24 | ||||
| -rw-r--r-- | tactics/equality.ml | 28 |
3 files changed, 27 insertions, 27 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 499e7a63d7..67f49f0074 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -49,7 +49,7 @@ let auto_core_unif_flags_of st1 st2 = { check_applied_meta_types = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; - frozen_evars = Evar.Set.empty; + allowed_evars = AllowAll; restrict_conv_on_strict_subterms = false; (* Compat *) modulo_betaiota = false; modulo_eta = true; diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 05f40d0570..cf5c64c3ae 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -151,7 +151,7 @@ let pr_ev evs ev = open Auto open Unification -let auto_core_unif_flags st freeze = { +let auto_core_unif_flags st allowed_evars = { modulo_conv_on_closed_terms = Some st; use_metas_eagerly_in_conv_on_closed_terms = true; use_evars_eagerly_in_conv_on_closed_terms = false; @@ -160,14 +160,14 @@ let auto_core_unif_flags st freeze = { check_applied_meta_types = false; use_pattern_unification = true; use_meta_bound_pattern_unification = true; - frozen_evars = freeze; + allowed_evars; restrict_conv_on_strict_subterms = false; (* ? *) modulo_betaiota = true; modulo_eta = false; } -let auto_unif_flags freeze st = - let fl = auto_core_unif_flags st freeze in +let auto_unif_flags ?(allowed_evars = AllowAll) st = + let fl = auto_core_unif_flags st allowed_evars in { core_unify_flags = fl; merge_unify_flags = fl; subterm_unify_flags = fl; @@ -357,23 +357,25 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm let open Proofview.Notations in let prods, concl = EConstr.decompose_prod_assum sigma concl in let nprods = List.length prods in - let freeze = + let allowed_evars = try match hdc with | Some (hd,_) when only_classes -> let cl = Typeclasses.class_info env sigma hd in if cl.cl_strict then - Evarutil.undefined_evars_of_term sigma concl - else Evar.Set.empty - | _ -> Evar.Set.empty - with e when CErrors.noncritical e -> Evar.Set.empty + let undefined = lazy (Evarutil.undefined_evars_of_term sigma concl) in + let allowed evk = not (Evar.Set.mem evk (Lazy.force undefined)) in + AllowFun allowed + else AllowAll + | _ -> AllowAll + with e when CErrors.noncritical e -> AllowAll in let hint_of_db = hintmap_of sigma hdc secvars concl in let hintl = List.map_append (fun db -> let tacs = hint_of_db db in - let flags = auto_unif_flags freeze (Hint_db.transparent_state db) in + let flags = auto_unif_flags ~allowed_evars (Hint_db.transparent_state db) in List.map (fun x -> (flags, x)) tacs) (local_db::db_list) in @@ -1198,7 +1200,7 @@ let autoapply c i = let hintdb = try Hints.searchtable_map i with Not_found -> CErrors.user_err (Pp.str ("Unknown hint database " ^ i ^ ".")) in - let flags = auto_unif_flags Evar.Set.empty + let flags = auto_unif_flags (Hints.Hint_db.transparent_state hintdb) in let cty = Tacmach.New.pf_unsafe_type_of gl c in let ce = mk_clenv_from gl (c,cty) in diff --git a/tactics/equality.ml b/tactics/equality.ml index b9d718dd61..220b9bc475 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -38,7 +38,6 @@ open Coqlib open Declarations open Indrec open Clenv -open Evd open Ind_tables open Eqschemes open Locus @@ -107,7 +106,7 @@ let rewrite_core_unif_flags = { check_applied_meta_types = true; use_pattern_unification = true; use_meta_bound_pattern_unification = true; - frozen_evars = Evar.Set.empty; + allowed_evars = AllowAll; restrict_conv_on_strict_subterms = false; modulo_betaiota = false; modulo_eta = true; @@ -126,16 +125,17 @@ 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 = Evarutil.undefined_evars_of_term sigma (clenv_type clause) in - let evars = - fold_undefined (fun evk _ evars -> - if Evar.Set.mem evk newevars then evars - else Evar.Set.add evk evars) - sigma Evar.Set.empty in + let newevars = lazy (Evarutil.undefined_evars_of_term sigma (clenv_type clause)) in + let initial = Evd.undefined_map sigma in + let allowed evk = + if Evar.Map.mem evk initial then false + else Evar.Set.mem evk (Lazy.force newevars) + in + let allowed_evars = AllowFun allowed in {flags with - core_unify_flags = {flags.core_unify_flags with frozen_evars = evars}; - merge_unify_flags = {flags.merge_unify_flags with frozen_evars = evars}; - subterm_unify_flags = {flags.subterm_unify_flags with frozen_evars = evars}} + core_unify_flags = {flags.core_unify_flags with allowed_evars}; + merge_unify_flags = {flags.merge_unify_flags with allowed_evars}; + subterm_unify_flags = {flags.subterm_unify_flags with allowed_evars}} let make_flags frzevars sigma flags clause = if frzevars then freeze_initial_evars sigma flags clause else flags @@ -188,8 +188,7 @@ let rewrite_conv_closed_core_unif_flags = { use_meta_bound_pattern_unification = true; - frozen_evars = Evar.Set.empty; - (* This is set dynamically *) + allowed_evars = AllowAll; restrict_conv_on_strict_subterms = false; modulo_betaiota = false; @@ -223,8 +222,7 @@ let rewrite_keyed_core_unif_flags = { use_meta_bound_pattern_unification = true; - frozen_evars = Evar.Set.empty; - (* This is set dynamically *) + allowed_evars = AllowAll; restrict_conv_on_strict_subterms = false; modulo_betaiota = true; |