diff options
| author | Matthieu Sozeau | 2014-06-18 17:16:59 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-18 17:21:21 +0200 |
| commit | 23f4804b50307766219392229757e75da9aa41d9 (patch) | |
| tree | 4df833759b600b1a3d638bdbc65cf5060eb3e24f /pretyping | |
| parent | 77839ae306380e99a8ceac0bf26ff86ec9159346 (diff) | |
Proofs now take and return an evar_universe_context, simplifying interfaces
and avoiding explicit substitutions and merging of contexts, e.g. in obligations.ml.
The context produced by typechecking a statement is passed in the proof, allowing the
universe name context to be correctly folded as well. Mainly an API cleanup.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evd.ml | 11 | ||||
| -rw-r--r-- | pretyping/evd.mli | 8 |
2 files changed, 10 insertions, 9 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 8b9631b4bd..d5aaf9df35 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -305,10 +305,10 @@ let empty_evar_universe_context = uctx_universes = Univ.initial_universes; uctx_initial_universes = Univ.initial_universes } -let evar_universe_context_from e c = +let evar_universe_context_from e = let u = universes e in {empty_evar_universe_context with - uctx_local = c; uctx_universes = u; uctx_initial_universes = u} + uctx_universes = u; uctx_initial_universes = u} let is_empty_evar_universe_context ctx = Univ.ContextSet.is_empty ctx.uctx_local && @@ -751,9 +751,10 @@ let empty = { effects = Declareops.no_seff; } -let from_env ?(ctx=Univ.ContextSet.empty) e = - { empty with universes = evar_universe_context_from e ctx } - +let from_env ?ctx e = + match ctx with + | None -> { empty with universes = evar_universe_context_from e } + | Some ctx -> { empty with universes = ctx } let has_undefined evd = not (EvMap.is_empty evd.undf_evars) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 3b58910e1f..1393a33d3c 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -117,6 +117,9 @@ val map_evar_info : (constr -> constr) -> evar_info -> evar_info (** {6 Unification state} **) +type evar_universe_context +(** The universe context associated to an evar map *) + type evar_map (** Type of unification state. Essentially a bunch of state-passing data needed to handle incremental term construction. *) @@ -128,7 +131,7 @@ val progress_evar_map : evar_map -> evar_map -> bool val empty : evar_map (** The empty evar map. *) -val from_env : ?ctx:Univ.universe_context_set -> env -> evar_map +val from_env : ?ctx:evar_universe_context -> env -> evar_map (** The empty evar map with given universe context, taking its initial universes from env. *) @@ -408,9 +411,6 @@ val univ_rigid : rigid val univ_flexible : rigid val univ_flexible_alg : rigid -(** The universe context associated to an evar map *) -type evar_universe_context - type 'a in_evar_universe_context = 'a * evar_universe_context val evar_universe_context_set : evar_universe_context -> Univ.universe_context_set |