diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-01-17 23:40:35 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-25 00:00:43 +0200 |
| commit | 30d3515546cf244837c6340b6b87c5f51e68cbf4 (patch) | |
| tree | 70dd074f483c34e9f71da20edf878062a4b5b3af /engine/evd.ml | |
| parent | 84eb5cd72a015c45337a5a6070c5651f56be6e74 (diff) | |
[location] Remove Loc.ghost.
Now it is a private field, locations are optional.
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 |