diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 5 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 9 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 11 | ||||
| -rw-r--r-- | pretyping/unification.ml | 4 |
4 files changed, 13 insertions, 16 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index c8ecf91d3..b76409f43 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -517,7 +517,10 @@ let rec detype flags avoid env sigma t = with Not_found -> isVarId id c in let id,l = try - let id = Evd.evar_ident evk sigma in + let id = match Evd.evar_ident evk sigma with + | None -> Evd.pr_evar_suggested_name evk sigma + | Some id -> id + in let l = Evd.evar_instance_array bound_to_itself_or_letin (Evd.find sigma evk) cl in let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> match kind_of_term c with Rel n -> (fvs,Int.Set.add n rels) | Var id -> (Id.Set.add id fvs,rels) | _ -> (fvs,rels)) (Id.Set.empty,Int.Set.empty) l in let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel c && Int.Set.mem (destRel c) rels || isVar c && (Id.Set.mem (destVar c) fvs)))) (Evd.find sigma evk) cl in diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 8c210e283..cd5188cd7 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -351,14 +351,7 @@ let new_pure_evar_full evd evi = (evd, evk) let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ = - let default_naming = - if principal then - (* waiting for a more principled approach - (unnamed evars, private names?) *) - Misctypes.IntroFresh (Names.Id.of_string "tmp_goal") - else - Misctypes.IntroAnonymous - in + let default_naming = Misctypes.IntroAnonymous in let naming = Option.default default_naming naming in let evi = { evar_hyps = sign; diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 3d6196c35..fc8fab2f9 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -494,15 +494,18 @@ let is_instance = function let resolvable = Store.field () let set_resolvable s b = - Store.set s resolvable b + if b then Store.remove s resolvable + else Store.set s resolvable () let is_resolvable evi = assert (match evi.evar_body with Evar_empty -> true | _ -> false); - Option.default true (Store.get evi.evar_extra resolvable) + Option.is_empty (Store.get evi.evar_extra resolvable) let mark_resolvability_undef b evi = - let t = Store.set evi.evar_extra resolvable b in - { evi with evar_extra = t } + if is_resolvable evi = b then evi + else + let t = set_resolvable evi.evar_extra b in + { evi with evar_extra = t } let mark_resolvability b evi = assert (match evi.evar_body with Evar_empty -> true | _ -> false); diff --git a/pretyping/unification.ml b/pretyping/unification.ml index b5e882bc4..027a3f86c 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1469,9 +1469,7 @@ let default_matching_core_flags sigma = check_applied_meta_types = true; use_pattern_unification = false; use_meta_bound_pattern_unification = false; - frozen_evars = - fold_undefined (fun evk _ evars -> Evar.Set.add evk evars) - sigma Evar.Set.empty; + frozen_evars = Evar.Map.domain (Evd.undefined_map sigma); restrict_conv_on_strict_subterms = false; modulo_betaiota = false; modulo_eta = false; |