diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evar_kinds.ml | 1 | ||||
| -rw-r--r-- | engine/evar_kinds.mli | 1 | ||||
| -rw-r--r-- | engine/evd.ml | 5 | ||||
| -rw-r--r-- | engine/evd.mli | 4 | ||||
| -rw-r--r-- | engine/termops.ml | 7 |
5 files changed, 18 insertions, 0 deletions
diff --git a/engine/evar_kinds.ml b/engine/evar_kinds.ml index 71d68f739e..fb41c4491e 100644 --- a/engine/evar_kinds.ml +++ b/engine/evar_kinds.ml @@ -40,6 +40,7 @@ type t = | ImplicitArg of GlobRef.t * (int * Id.t option) * bool (** Force inference *) | BinderType of Name.t + | EvarType of Id.t option * Evar.t (* type of an optionally named evar *) | NamedHole of Id.t (* coming from some ?[id] syntax *) | QuestionMark of question_mark | CasesType of bool (* true = a subterm of the type *) diff --git a/engine/evar_kinds.mli b/engine/evar_kinds.mli index ffc57cfd15..b2b39d49be 100644 --- a/engine/evar_kinds.mli +++ b/engine/evar_kinds.mli @@ -39,6 +39,7 @@ type t = | ImplicitArg of GlobRef.t * (int * Id.t option) * bool (** Force inference *) | BinderType of Name.t + | EvarType of Id.t option * Evar.t (* type of an optionally named evar *) | NamedHole of Id.t (* coming from some ?[id] syntax *) | QuestionMark of question_mark | CasesType of bool (* true = a subterm of the type *) diff --git a/engine/evd.ml b/engine/evd.ml index 498a9d9825..59eea97ce9 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1231,6 +1231,11 @@ let restrict evk filter ?candidates ?src evd = let evd = declare_future_goal evk' evd in (evd, evk') +let update_source evd evk src = + let evar_info = EvMap.find evk evd.undf_evars in + let evar_info' = { evar_info with evar_source = src } in + { evd with undf_evars = EvMap.add evk evar_info' evd.undf_evars } + (**********************************************************) (* Accessing metas *) diff --git a/engine/evd.mli b/engine/evd.mli index 1c5c65924c..911e00c23a 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -290,6 +290,10 @@ val restrict : Evar.t-> Filter.t -> ?candidates:econstr list -> possibly limiting the instances to a set of candidates (candidates are filtered according to the filter) *) +val update_source : evar_map -> Evar.t -> Evar_kinds.t located -> evar_map +(** To update the source a posteriori, e.g. when an evar type of + another evar has to refer to this other evar, with a mutual dependency *) + val get_aliased_evars : evar_map -> Evar.t Evar.Map.t (** The map of aliased evars *) diff --git a/engine/termops.ml b/engine/termops.ml index 693945d5ac..ccd49ca495 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -123,6 +123,13 @@ let pr_evar_source env sigma = function str "subterm of pattern-matching return predicate" | Evar_kinds.BinderType (Name id) -> str "type of " ++ Id.print id | Evar_kinds.BinderType Anonymous -> str "type of anonymous binder" + | Evar_kinds.EvarType (ido,evk) -> + let pp = match ido with + | Some id -> str "?" ++ Id.print id + | None -> + try pr_existential_key sigma evk + with (* defined *) Not_found -> str "an internal placeholder" in + str "type of " ++ pp | Evar_kinds.ImplicitArg (c,(n,ido),b) -> let open Globnames in let print_constr = print_kconstr in |