diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-21 19:21:26 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-31 11:16:45 +0200 |
| commit | 2a69be9e8243fa67d5c7ef5f10e623b02a0a3e2f (patch) | |
| tree | 493d780d22515a60716845109d12690caf0b1f8a /vernac/comFixpoint.mli | |
| parent | ac8a84e3b4dc530b000e17b72c7e26f7a957420f (diff) | |
[api] Move `Constrexpr` to the `interp` module.
Continuing the interface cleanup we place `Constrexpr` in the
internalization module, which is the one that eliminates it.
This slims down `pretyping` considerably, including removing the
`Univdecls` module which existed only due to bad dependency ordering
in the first place. Thanks to @ Skyskimmer we also remove a duplicate
`univ_decl` definition among `Misctypes` and `UState`.
This is mostly a proof of concept yet as it depends on quite a few
patches of the tree. For sure some tweaks will be necessary, but it
should be good for review now.
IMO the tree is now in a state where we can could easy eliminate more
than 10 modules without any impact, IMHO this is a net saving API-wise
and would help people to understand the structure of the code better.
Diffstat (limited to 'vernac/comFixpoint.mli')
| -rw-r--r-- | vernac/comFixpoint.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index 36c2993af..a6992a30b 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -49,7 +49,7 @@ val interp_recursive : structured_fixpoint_expr list -> decl_notation list -> (* env / signature / univs / evar_map *) - (Environ.env * EConstr.named_context * Univdecls.universe_decl * Evd.evar_map) * + (Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) * (* names / defs / types *) (Id.t list * Constr.constr option list * Constr.types list) * (* ctx per mutual def / implicits / struct annotations *) @@ -74,19 +74,19 @@ type recursive_preentry = val interp_fixpoint : cofix:bool -> structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * Univdecls.universe_decl * UState.t * + recursive_preentry * UState.universe_decl * UState.t * (EConstr.rel_context * Impargs.manual_implicits * int option) list (** Registering fixpoints and cofixpoints in the environment *) (** [Not used so far] *) val declare_fixpoint : locality -> polymorphic -> - recursive_preentry * Univdecls.universe_decl * UState.t * + recursive_preentry * UState.universe_decl * UState.t * (Context.Rel.t * Impargs.manual_implicits * int option) list -> Proof_global.lemma_possible_guards -> decl_notation list -> unit val declare_cofixpoint : locality -> polymorphic -> - recursive_preentry * Univdecls.universe_decl * UState.t * + recursive_preentry * UState.universe_decl * UState.t * (Context.Rel.t * Impargs.manual_implicits * int option) list -> decl_notation list -> unit |