diff options
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 5419a10a8..9e81ccd36 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -151,7 +151,7 @@ let make_evar hyps ccl = { evar_hyps = hyps; evar_body = Evar_empty; evar_filter = Filter.identity; - evar_source = (Loc.ghost,Evar_kinds.InternalHole); + evar_source = Loc.tag @@ Evar_kinds.InternalHole; evar_candidates = None; evar_extra = Store.empty } @@ -704,11 +704,11 @@ let extract_all_conv_pbs evd = let loc_of_conv_pb evd (pbty,env,t1,t2) = match kind_of_term (fst (decompose_app t1)) with - | Evar (evk1,_) -> fst (evar_source evk1 evd) + | Evar (evk1,_) -> Some (fst (evar_source evk1 evd)) | _ -> match kind_of_term (fst (decompose_app t2)) with - | Evar (evk2,_) -> fst (evar_source evk2 evd) - | _ -> Loc.ghost + | Evar (evk2,_) -> Some (fst (evar_source evk2 evd)) + | _ -> None (** The following functions return the set of evars immediately contained in the object *) @@ -1086,8 +1086,8 @@ let retract_coercible_metas evd = let evar_source_of_meta mv evd = match meta_name evd mv with - | Anonymous -> (Loc.ghost,Evar_kinds.GoalEvar) - | Name id -> (Loc.ghost,Evar_kinds.VarInstance id) + | Anonymous -> Loc.tag Evar_kinds.GoalEvar + | Name id -> Loc.tag @@ Evar_kinds.VarInstance id let dependent_evar_ident ev evd = let evi = find evd ev in |