aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-21 19:21:26 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-31 11:16:45 +0200
commit2a69be9e8243fa67d5c7ef5f10e623b02a0a3e2f (patch)
tree493d780d22515a60716845109d12690caf0b1f8a
parentac8a84e3b4dc530b000e17b72c7e26f7a957420f (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.
-rw-r--r--dev/doc/changes.md9
-rw-r--r--engine/uState.ml16
-rw-r--r--engine/uState.mli10
-rw-r--r--interp/constrexpr.ml (renamed from pretyping/constrexpr.ml)3
-rw-r--r--interp/constrexpr_ops.ml32
-rw-r--r--interp/constrexpr_ops.mli7
-rw-r--r--interp/genredexpr.ml (renamed from pretyping/genredexpr.ml)0
-rw-r--r--interp/implicit_quantifiers.ml6
-rw-r--r--interp/implicit_quantifiers.mli4
-rw-r--r--interp/interp.mllib3
-rw-r--r--interp/modintern.ml2
-rw-r--r--interp/redops.ml (renamed from pretyping/redops.ml)20
-rw-r--r--interp/redops.mli (renamed from pretyping/redops.mli)5
-rw-r--r--library/misctypes.ml6
-rw-r--r--plugins/ltac/tacsubst.ml2
-rw-r--r--pretyping/miscops.ml21
-rw-r--r--pretyping/miscops.mli6
-rw-r--r--pretyping/pretyping.mllib4
-rw-r--r--pretyping/typeclasses_errors.ml4
-rw-r--r--pretyping/typeclasses_errors.mli4
-rw-r--r--pretyping/univdecls.ml52
-rw-r--r--pretyping/univdecls.mli21
-rw-r--r--proofs/pfedit.mli2
-rw-r--r--proofs/proof_global.ml13
-rw-r--r--proofs/proof_global.mli6
-rw-r--r--proofs/redexpr.ml2
-rw-r--r--vernac/classes.ml6
-rw-r--r--vernac/classes.mli2
-rw-r--r--vernac/comAssumption.ml2
-rw-r--r--vernac/comDefinition.ml2
-rw-r--r--vernac/comDefinition.mli2
-rw-r--r--vernac/comFixpoint.ml5
-rw-r--r--vernac/comFixpoint.mli8
-rw-r--r--vernac/comInductive.ml2
-rw-r--r--vernac/comProgramFixpoint.ml2
-rw-r--r--vernac/explainErr.ml2
-rw-r--r--vernac/g_vernac.ml41
-rw-r--r--vernac/himsg.ml1
-rw-r--r--vernac/himsg.mli2
-rw-r--r--vernac/lemmas.ml4
-rw-r--r--vernac/lemmas.mli6
-rw-r--r--vernac/obligations.ml6
-rw-r--r--vernac/obligations.mli4
-rw-r--r--vernac/ppvernac.ml2
-rw-r--r--vernac/record.ml2
45 files changed, 150 insertions, 171 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 346b7c7dd..4838dd734 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -41,6 +41,15 @@ Printer.ml API
pr_subgoal and pr_goal was removed to simplify the code. It was
earlierly used by PCoq.
+Source code organization
+
+- We have eliminated / fused some redundant modules and relocated a
+ few interfaces files. The `intf` folder is gone, and now for example
+ `Constrexpr` is located in `interp/`, `Vernacexpr` in `vernac/` and
+ so on. Changes should be compatible, but in a few cases stricter
+ layering requirements may mean that functions have moved. In all
+ cases adapting is a matter of changing the module name.
+
Vernacular commands
- The implementation of vernacular commands has been refactored so it
diff --git a/engine/uState.ml b/engine/uState.ml
index 15cf4d4c1..643c621fd 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -305,8 +305,20 @@ let reference_of_level uctx =
let pr_uctx_level uctx l =
Libnames.pr_reference (reference_of_level uctx l)
+type ('a, 'b) gen_universe_decl = {
+ univdecl_instance : 'a; (* Declared universes *)
+ univdecl_extensible_instance : bool; (* Can new universes be added *)
+ univdecl_constraints : 'b; (* Declared constraints *)
+ univdecl_extensible_constraints : bool (* Can new constraints be added *) }
+
type universe_decl =
- (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
+ (Misctypes.lident list, Univ.Constraint.t) gen_universe_decl
+
+let default_univ_decl =
+ { univdecl_instance = [];
+ univdecl_extensible_instance = true;
+ univdecl_constraints = Univ.Constraint.empty;
+ univdecl_extensible_constraints = true }
let error_unbound_universes left uctx =
let open Univ in
@@ -367,7 +379,6 @@ let check_implication uctx cstrs cstrs' =
(str "Universe constraints are not implied by the ones declared.")
let check_mono_univ_decl uctx decl =
- let open Misctypes in
let () =
let names = decl.univdecl_instance in
let extensible = decl.univdecl_extensible_instance in
@@ -380,7 +391,6 @@ let check_mono_univ_decl uctx decl =
uctx.uctx_local
let check_univ_decl ~poly uctx decl =
- let open Misctypes in
let ctx =
let names = decl.univdecl_instance in
let extensible = decl.univdecl_extensible_instance in
diff --git a/engine/uState.mli b/engine/uState.mli
index d1678a155..e2f25642e 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -138,8 +138,16 @@ val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst
(** Universe minimization *)
val minimize : t -> t
+type ('a, 'b) gen_universe_decl = {
+ univdecl_instance : 'a; (* Declared universes *)
+ univdecl_extensible_instance : bool; (* Can new universes be added *)
+ univdecl_constraints : 'b; (* Declared constraints *)
+ univdecl_extensible_constraints : bool (* Can new constraints be added *) }
+
type universe_decl =
- (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
+ (Misctypes.lident list, Univ.Constraint.t) gen_universe_decl
+
+val default_univ_decl : universe_decl
(** [check_univ_decl ctx decl]
diff --git a/pretyping/constrexpr.ml b/interp/constrexpr.ml
index 1443dfb51..ca6ea94f0 100644
--- a/pretyping/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -16,8 +16,7 @@ open Decl_kinds
(** {6 Concrete syntax for terms } *)
(** [constr_expr] is the abstract syntax tree produced by the parser *)
-
-type universe_decl_expr = (lident list, Glob_term.glob_constraint list) gen_universe_decl
+type universe_decl_expr = (lident list, Glob_term.glob_constraint list) UState.gen_universe_decl
type ident_decl = lident * universe_decl_expr option
type name_decl = lname * universe_decl_expr option
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 3eb5acfc5..1be1dd96c 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -600,3 +600,35 @@ let _ = Goptions.declare_bool_option {
Goptions.optread = (fun () -> !asymmetric_patterns);
Goptions.optwrite = (fun a -> asymmetric_patterns:=a);
}
+
+(** Local universe and constraint declarations. *)
+
+let interp_univ_constraints env evd cstrs =
+ let interp (evd,cstrs) (u, d, u') =
+ let ul = Pretyping.interp_known_glob_level evd u in
+ let u'l = Pretyping.interp_known_glob_level evd u' in
+ let cstr = (ul,d,u'l) in
+ let cstrs' = Univ.Constraint.add cstr cstrs in
+ try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in
+ evd, cstrs'
+ with Univ.UniverseInconsistency e ->
+ CErrors.user_err ~hdr:"interp_constraint"
+ (Univ.explain_universe_inconsistency (Termops.pr_evd_level evd) e)
+ in
+ List.fold_left interp (evd,Univ.Constraint.empty) cstrs
+
+let interp_univ_decl env decl =
+ let open UState in
+ let pl : lident list = decl.univdecl_instance in
+ let evd = Evd.from_ctx (UState.make_with_initial_binders (Environ.universes env) pl) in
+ let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
+ let decl = { univdecl_instance = pl;
+ univdecl_extensible_instance = decl.univdecl_extensible_instance;
+ univdecl_constraints = cstrs;
+ univdecl_extensible_constraints = decl.univdecl_extensible_constraints }
+ in evd, decl
+
+let interp_univ_decl_opt env l =
+ match l with
+ | None -> Evd.from_env env, UState.default_univ_decl
+ | Some decl -> interp_univ_decl env decl
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 2df9e5a8c..b4f0886ac 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -116,3 +116,10 @@ val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a
(** Placeholder for global option, should be moved to a parameter *)
val asymmetric_patterns : bool ref
+
+(** Local universe and constraint declarations. *)
+val interp_univ_decl : Environ.env -> universe_decl_expr ->
+ Evd.evar_map * UState.universe_decl
+
+val interp_univ_decl_opt : Environ.env -> universe_decl_expr option ->
+ Evd.evar_map * UState.universe_decl
diff --git a/pretyping/genredexpr.ml b/interp/genredexpr.ml
index 80697461a..80697461a 100644
--- a/pretyping/genredexpr.ml
+++ b/interp/genredexpr.ml
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 289890544..b48db9ac5 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -17,12 +17,14 @@ open Glob_term
open Constrexpr
open Libnames
open Typeclasses
-open Typeclasses_errors
open Pp
open Libobject
open Nameops
open Context.Rel.Declaration
+exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Context.Rel.t (* found, expected *)
+let mismatched_ctx_inst_err env c n m = raise (MismatchedContextInstance (env, c, n, m))
+
module RelDecl = Context.Rel.Declaration
(*i*)
@@ -238,7 +240,7 @@ let implicit_application env ?(allow_partial=true) f ty =
let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in
let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in
if not (Int.equal needlen applen) then
- Typeclasses_errors.mismatched_ctx_inst (Global.env ()) Parameters (List.map fst par) rd
+ mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd
end;
let pars = List.rev (List.combine ci rd) in
let args, avoid = combine_params avoid f par pars in
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 39d0174f9..e64c5c542 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -45,3 +45,7 @@ val implicit_application : Id.Set.t -> ?allow_partial:bool ->
(Id.Set.t -> GlobRef.t option * Context.Rel.Declaration.t ->
Constrexpr.constr_expr * Id.Set.t) ->
constr_expr -> constr_expr * Id.Set.t
+
+(* Should be likely located elsewhere *)
+exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Context.Rel.t (* found, expected *)
+val mismatched_ctx_inst_err : Environ.env -> Typeclasses_errors.contexts -> constr_expr list -> Context.Rel.t -> 'a
diff --git a/interp/interp.mllib b/interp/interp.mllib
index 37a327a7d..8ed2b9fad 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -1,3 +1,6 @@
+Constrexpr
+Genredexpr
+Redops
Tactypes
Stdarg
Genintern
diff --git a/interp/modintern.ml b/interp/modintern.ml
index dc93d8dc4..fefd2ab6f 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -63,7 +63,7 @@ let transl_with_decl env = function
| CWith_Module ({CAst.v=fqid},qid) ->
WithMod (fqid,lookup_module qid), Univ.ContextSet.empty
| CWith_Definition ({CAst.v=fqid},udecl,c) ->
- let sigma, udecl = Univdecls.interp_univ_decl_opt env udecl in
+ let sigma, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in
let c, ectx = interp_constr env sigma c in
begin match UState.check_univ_decl ~poly:(Flags.is_universe_polymorphism()) ectx udecl with
| Entries.Polymorphic_const_entry ctx ->
diff --git a/pretyping/redops.ml b/interp/redops.ml
index 90c3bdfae..b9a74136e 100644
--- a/pretyping/redops.ml
+++ b/interp/redops.ml
@@ -42,3 +42,23 @@ let make_red_flag l =
let all_flags =
{rBeta = true; rMatch = true; rFix = true; rCofix = true;
rZeta = true; rDelta = true; rConst = []}
+
+(** Mapping [red_expr_gen] *)
+
+let map_flags f flags =
+ { flags with rConst = List.map f flags.rConst }
+
+let map_occs f (occ,e) = (occ,f e)
+
+let map_red_expr_gen f g h = function
+ | Fold l -> Fold (List.map f l)
+ | Pattern occs_l -> Pattern (List.map (map_occs f) occs_l)
+ | Simpl (flags,occs_o) ->
+ Simpl (map_flags g flags, Option.map (map_occs (Util.map_union g h)) occs_o)
+ | Unfold occs_l -> Unfold (List.map (map_occs g) occs_l)
+ | Cbv flags -> Cbv (map_flags g flags)
+ | Lazy flags -> Lazy (map_flags g flags)
+ | CbvVm occs_o -> CbvVm (Option.map (map_occs (Util.map_union g h)) occs_o)
+ | CbvNative occs_o -> CbvNative (Option.map (map_occs (Util.map_union g h)) occs_o)
+ | Cbn flags -> Cbn (map_flags g flags)
+ | ExtraRedExpr _ | Red _ | Hnf as x -> x
diff --git a/pretyping/redops.mli b/interp/redops.mli
index 285931ecd..7254f29b2 100644
--- a/pretyping/redops.mli
+++ b/interp/redops.mli
@@ -13,3 +13,8 @@ open Genredexpr
val make_red_flag : 'a red_atom list -> 'a glob_red_flag
val all_flags : 'a glob_red_flag
+
+(** Mapping [red_expr_gen] *)
+
+val map_red_expr_gen : ('a -> 'd) -> ('b -> 'e) -> ('c -> 'f) ->
+ ('a,'b,'c) red_expr_gen -> ('d,'e,'f) red_expr_gen
diff --git a/library/misctypes.ml b/library/misctypes.ml
index a3c887045..cfae07484 100644
--- a/library/misctypes.ml
+++ b/library/misctypes.ml
@@ -112,9 +112,3 @@ type multi =
| UpTo of int
| RepeatStar
| RepeatPlus
-
-type ('a, 'b) gen_universe_decl = {
- univdecl_instance : 'a; (* Declared universes *)
- univdecl_extensible_instance : bool; (* Can new universes be added *)
- univdecl_constraints : 'b; (* Declared constraints *)
- univdecl_extensible_constraints : bool (* Can new constraints be added *) }
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index a1d8b087e..50bf687b1 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -112,7 +112,7 @@ let subst_glob_constr_or_pattern subst (bvars,c,p) =
(bvars,subst_glob_constr subst c,subst_pattern subst p)
let subst_redexp subst =
- Miscops.map_red_expr_gen
+ Redops.map_red_expr_gen
(subst_glob_constr subst)
(subst_evaluable subst)
(subst_glob_constr_or_pattern subst)
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 1b536bfda..1697e54ab 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -10,7 +10,6 @@
open Util
open Misctypes
-open Genredexpr
(** Mapping [cast_type] *)
@@ -42,26 +41,6 @@ let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with
| IntroFresh id1, IntroFresh id2 -> Names.Id.equal id1 id2
| _ -> false
-(** Mapping [red_expr_gen] *)
-
-let map_flags f flags =
- { flags with rConst = List.map f flags.rConst }
-
-let map_occs f (occ,e) = (occ,f e)
-
-let map_red_expr_gen f g h = function
- | Fold l -> Fold (List.map f l)
- | Pattern occs_l -> Pattern (List.map (map_occs f) occs_l)
- | Simpl (flags,occs_o) ->
- Simpl (map_flags g flags, Option.map (map_occs (map_union g h)) occs_o)
- | Unfold occs_l -> Unfold (List.map (map_occs g) occs_l)
- | Cbv flags -> Cbv (map_flags g flags)
- | Lazy flags -> Lazy (map_flags g flags)
- | CbvVm occs_o -> CbvVm (Option.map (map_occs (map_union g h)) occs_o)
- | CbvNative occs_o -> CbvNative (Option.map (map_occs (map_union g h)) occs_o)
- | Cbn flags -> Cbn (map_flags g flags)
- | ExtraRedExpr _ | Red _ | Hnf as x -> x
-
(** Mapping bindings *)
let map_explicit_bindings f l =
diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli
index 1d4504541..6a84fb9eb 100644
--- a/pretyping/miscops.mli
+++ b/pretyping/miscops.mli
@@ -9,7 +9,6 @@
(************************************************************************)
open Misctypes
-open Genredexpr
(** Mapping [cast_type] *)
@@ -25,11 +24,6 @@ val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool
val intro_pattern_naming_eq :
intro_pattern_naming_expr -> intro_pattern_naming_expr -> bool
-(** Mapping [red_expr_gen] *)
-
-val map_red_expr_gen : ('a -> 'd) -> ('b -> 'e) -> ('c -> 'f) ->
- ('a,'b,'c) red_expr_gen -> ('d,'e,'f) red_expr_gen
-
(** Mapping bindings *)
val map_bindings : ('a -> 'b) -> 'a bindings -> 'b bindings
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index c48decdb0..3d9b5d3cf 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -16,13 +16,10 @@ Evarsolve
Recordops
Evarconv
Typing
-Constrexpr
-Genredexpr
Miscops
Glob_term
Ltac_pretype
Glob_ops
-Redops
Pattern
Patternops
Constr_matching
@@ -37,4 +34,3 @@ Indrec
Cases
Pretyping
Unification
-Univdecls
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 89c5d7e7b..a1ac53c73 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -12,7 +12,6 @@
open Names
open EConstr
open Environ
-open Constrexpr
(*i*)
type contexts = Parameters | Properties
@@ -20,7 +19,6 @@ type contexts = Parameters | Properties
type typeclass_error =
| NotAClass of constr
| UnboundMethod of GlobRef.t * Misctypes.lident (* Class name, method *)
- | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (* found, expected *)
exception TypeClassError of env * typeclass_error
@@ -29,5 +27,3 @@ let typeclass_error env err = raise (TypeClassError (env, err))
let not_a_class env c = typeclass_error env (NotAClass c)
let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id))
-
-let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m))
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 4aabc0aee..1003f2ae1 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -11,14 +11,12 @@
open Names
open EConstr
open Environ
-open Constrexpr
type contexts = Parameters | Properties
type typeclass_error =
| NotAClass of constr
| UnboundMethod of GlobRef.t * Misctypes.lident (** Class name, method *)
- | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (** found, expected *)
exception TypeClassError of env * typeclass_error
@@ -26,5 +24,3 @@ val not_a_class : env -> constr -> 'a
val unbound_method : env -> GlobRef.t -> Misctypes.lident -> 'a
-val mismatched_ctx_inst : env -> contexts -> constr_expr list -> Context.Rel.t -> 'a
-
diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml
deleted file mode 100644
index 8864be576..000000000
--- a/pretyping/univdecls.ml
+++ /dev/null
@@ -1,52 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-open CErrors
-
-(** Local universes and constraints declarations *)
-type universe_decl =
- (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
-
-let default_univ_decl =
- let open Misctypes in
- { univdecl_instance = [];
- univdecl_extensible_instance = true;
- univdecl_constraints = Univ.Constraint.empty;
- univdecl_extensible_constraints = true }
-
-let interp_univ_constraints env evd cstrs =
- let interp (evd,cstrs) (u, d, u') =
- let ul = Pretyping.interp_known_glob_level evd u in
- let u'l = Pretyping.interp_known_glob_level evd u' in
- let cstr = (ul,d,u'l) in
- let cstrs' = Univ.Constraint.add cstr cstrs in
- try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in
- evd, cstrs'
- with Univ.UniverseInconsistency e ->
- user_err ~hdr:"interp_constraint"
- (Univ.explain_universe_inconsistency (Termops.pr_evd_level evd) e)
- in
- List.fold_left interp (evd,Univ.Constraint.empty) cstrs
-
-let interp_univ_decl env decl =
- let open Misctypes in
- let pl : lident list = decl.univdecl_instance in
- let evd = Evd.from_ctx (UState.make_with_initial_binders (Environ.universes env) pl) in
- let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
- let decl = { univdecl_instance = pl;
- univdecl_extensible_instance = decl.univdecl_extensible_instance;
- univdecl_constraints = cstrs;
- univdecl_extensible_constraints = decl.univdecl_extensible_constraints }
- in evd, decl
-
-let interp_univ_decl_opt env l =
- match l with
- | None -> Evd.from_env env, default_univ_decl
- | Some decl -> interp_univ_decl env decl
diff --git a/pretyping/univdecls.mli b/pretyping/univdecls.mli
deleted file mode 100644
index 305d045b1..000000000
--- a/pretyping/univdecls.mli
+++ /dev/null
@@ -1,21 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-(** Local universe and constraint declarations. *)
-type universe_decl =
- (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
-
-val default_univ_decl : universe_decl
-
-val interp_univ_decl : Environ.env -> Constrexpr.universe_decl_expr ->
- Evd.evar_map * universe_decl
-
-val interp_univ_decl_opt : Environ.env -> Constrexpr.universe_decl_expr option ->
- Evd.evar_map * universe_decl
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 805635dfa..7b7973224 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -24,7 +24,7 @@ open Decl_kinds
proof of mutually dependent theorems) *)
val start_proof :
- Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr ->
+ Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr ->
?init_tac:unit Proofview.tactic ->
Proof_global.proof_terminator -> unit
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index d5cb5b09f..3abdd129e 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -97,7 +97,7 @@ type pstate = {
proof : Proof.t;
strength : Decl_kinds.goal_kind;
mode : proof_mode CEphemeron.key;
- universe_decl: Univdecls.universe_decl;
+ universe_decl: UState.universe_decl;
}
type t = pstate list
@@ -238,13 +238,6 @@ let activate_proof_mode mode =
let disactivate_current_proof_mode () =
CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ())
-let default_universe_decl =
- let open Misctypes in
- { univdecl_instance = [];
- univdecl_extensible_instance = true;
- univdecl_constraints = Univ.Constraint.empty;
- univdecl_extensible_constraints = true }
-
(** [start_proof sigma id pl str goals terminator] starts a proof of name
[id] with goals [goals] (a list of pairs of environment and
conclusion); [str] describes what kind of theorem/definition this
@@ -253,7 +246,7 @@ let default_universe_decl =
end of the proof to close the proof. The proof is started in the
evar map [sigma] (which can typically contain universe
constraints), and with universe bindings pl. *)
-let start_proof sigma id ?(pl=default_universe_decl) str goals terminator =
+let start_proof sigma id ?(pl=UState.default_univ_decl) str goals terminator =
let initial_state = {
pid = id;
terminator = CEphemeron.create terminator;
@@ -265,7 +258,7 @@ let start_proof sigma id ?(pl=default_universe_decl) str goals terminator =
universe_decl = pl } in
push initial_state pstates
-let start_dependent_proof id ?(pl=default_universe_decl) str goals terminator =
+let start_dependent_proof id ?(pl=UState.default_univ_decl) str goals terminator =
let initial_state = {
pid = id;
terminator = CEphemeron.create terminator;
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index de4cec488..0141cacb9 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -71,14 +71,14 @@ val apply_terminator : proof_terminator -> proof_ending -> unit
evar map [sigma] (which can typically contain universe
constraints), and with universe bindings pl. *)
val start_proof :
- Evd.evar_map -> Names.Id.t -> ?pl:Univdecls.universe_decl ->
+ Evd.evar_map -> Names.Id.t -> ?pl:UState.universe_decl ->
Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list ->
proof_terminator -> unit
(** Like [start_proof] except that there may be dependencies between
initial goals. *)
val start_dependent_proof :
- Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind ->
+ Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind ->
Proofview.telescope -> proof_terminator -> unit
(** Update the proofs global environment after a side-effecting command
@@ -130,7 +130,7 @@ val set_used_variables :
val get_used_variables : unit -> Context.Named.t option
(** Get the universe declaration associated to the current proof. *)
-val get_universe_decl : unit -> Univdecls.universe_decl
+val get_universe_decl : unit -> UState.universe_decl
module V82 : sig
val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list *
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index f9e7bbfac..03ebc3275 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -263,7 +263,7 @@ let subst_mps subst c =
EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c))
let subst_red_expr subs =
- Miscops.map_red_expr_gen
+ Redops.map_red_expr_gen
(subst_mps subs)
(Mod_subst.subst_evaluable_reference subs)
(Patternops.subst_pattern subs)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index c82208980..946a7bb32 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -77,8 +77,8 @@ let existing_instance glob g info =
~hdr:"declare_instance"
(Pp.str "Constant does not build instances of a declared type class.")
-let mismatched_params env n m = mismatched_ctx_inst env Parameters n m
-let mismatched_props env n m = mismatched_ctx_inst env Properties n m
+let mismatched_params env n m = Implicit_quantifiers.mismatched_ctx_inst_err env Parameters n m
+let mismatched_props env n m = Implicit_quantifiers.mismatched_ctx_inst_err env Properties n m
(* Declare everything in the parameters as implicit, and the class instance as well *)
@@ -137,7 +137,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
?(tac:unit Proofview.tactic option) ?hook pri =
let env = Global.env() in
let ({CAst.loc;v=instid}, pl) = instid in
- let sigma, decl = Univdecls.interp_univ_decl_opt env pl in
+ let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
let tclass, ids =
match bk with
| Decl_kinds.Implicit ->
diff --git a/vernac/classes.mli b/vernac/classes.mli
index 631da8400..eea2a211d 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -32,7 +32,7 @@ val declare_instance_constant :
Impargs.manual_explicitation list -> (** implicits *)
?hook:(GlobRef.t -> unit) ->
Id.t -> (** name *)
- Univdecls.universe_decl ->
+ UState.universe_decl ->
bool -> (* polymorphic *)
Evd.evar_map -> (* Universes *)
Constr.t -> (** body *)
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 492ae1d9b..a8ac52846 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -136,7 +136,7 @@ let do_assumptions kind nl l =
let open Context.Named.Declaration in
let env = Global.env () in
let udecl, l = process_assumptions_udecls kind l in
- let sigma, udecl = Univdecls.interp_univ_decl_opt env udecl in
+ let sigma, udecl = interp_univ_decl_opt env udecl in
let l =
if pi2 kind (* poly *) then
(* Separate declarations so that A B : Type puts A and B in different levels. *)
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 2d4bd6779..f55c852c0 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -65,7 +65,7 @@ let interp_definition pl bl poly red_option c ctypopt =
let open EConstr in
let env = Global.env() in
(* Explicitly bound universes and constraints *)
- let evd, decl = Univdecls.interp_univ_decl_opt env pl in
+ let evd, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
(* Build the parameters *)
let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars env evd bl in
(* Build the type *)
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 6f81c4575..7f1c902c0 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -29,4 +29,4 @@ val do_definition : program_mode:bool ->
val interp_definition :
universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr ->
constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map *
- Univdecls.universe_decl * Impargs.manual_implicits
+ UState.universe_decl * Impargs.manual_implicits
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index d996443d6..ea731b34c 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -173,11 +173,12 @@ let interp_recursive ~program_mode ~cofix fixl notations =
| None , acc -> acc
| x , None -> x
| Some ls , Some us ->
- let lsu = ls.univdecl_instance and usu = us.univdecl_instance in
+ let open UState in
+ let lsu = ls.univdecl_instance and usu = us.univdecl_instance in
if not (CList.for_all2eq (fun x y -> Id.equal x.CAst.v y.CAst.v) lsu usu) then
user_err Pp.(str "(co)-recursive definitions should all have the same universe binders");
Some us) fixl None in
- let sigma, decl = Univdecls.interp_univ_decl_opt env all_universes in
+ let sigma, decl = interp_univ_decl_opt env all_universes in
let sigma, (fixctxs, fiximppairs, fixannots) =
on_snd List.split3 @@
List.fold_left_map (fun sigma -> interp_fix_context env sigma ~cofix) sigma fixl in
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
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 790e83dbe..101c14266 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -333,7 +333,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
List.iter check_param paramsl;
let env0 = Global.env() in
let pl = (List.hd indl).ind_univs in
- let sigma, decl = Univdecls.interp_univ_decl_opt env0 pl in
+ let sigma, decl = interp_univ_decl_opt env0 pl in
let sigma, (impls, ((env_params, ctx_params), userimpls)) =
interp_context_evars env0 sigma paramsl
in
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index f41e0fc44..a6d7fccf3 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -91,7 +91,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in
Coqlib.check_required_library ["Coq";"Program";"Wf"];
let env = Global.env() in
- let sigma, decl = Univdecls.interp_univ_decl_opt env pl in
+ let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
let sigma, (_, ((env', binders_rel), impls)) = interp_context_evars env sigma bl in
let len = List.length binders_rel in
let top_env = push_rel_context binders_rel env in
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index f68dcae26..504e7095b 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -66,6 +66,8 @@ let process_vernac_interp_error exn = match fst exn with
wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te)
| Typeclasses_errors.TypeClassError(env, te) ->
wrap_vernac_error exn (Himsg.explain_typeclass_error env te)
+ | Implicit_quantifiers.MismatchedContextInstance(e,c,l,x) ->
+ wrap_vernac_error exn (Himsg.explain_mismatched_contexts e c l x)
| InductiveError e ->
wrap_vernac_error exn (Himsg.explain_inductive_error e)
| Modops.ModuleTypingError e ->
diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4
index 6c7df8cfa..0964d46ac 100644
--- a/vernac/g_vernac.ml4
+++ b/vernac/g_vernac.ml4
@@ -230,6 +230,7 @@ GEXTEND Gram
ext = [ "+" -> true | -> false ]; "}" -> (l',ext)
| ext = [ "}" -> true | "|}" -> false ] -> ([], ext) ]
->
+ let open UState in
{ univdecl_instance = l;
univdecl_extensible_instance = ext;
univdecl_constraints = fst cs;
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index d4c5def6f..5d671ef52 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1033,7 +1033,6 @@ let explain_mismatched_contexts env c i j =
let explain_typeclass_error env = function
| NotAClass c -> explain_not_a_class env c
| UnboundMethod (cid, id) -> explain_unbound_method env cid id
- | MismatchedContextInstance (c,i,j) -> explain_mismatched_contexts env c i j
(* Refiner errors *)
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index 0e20d18c6..1d3807502 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -25,6 +25,8 @@ val explain_pretype_error : env -> Evd.evar_map -> pretype_error -> Pp.t
val explain_inductive_error : inductive_error -> Pp.t
+val explain_mismatched_contexts : env -> contexts -> Constrexpr.constr_expr list -> Context.Rel.t -> Pp.t
+
val explain_typeclass_error : env -> typeclass_error -> Pp.t
val explain_recursion_scheme_error : recursion_scheme_error -> Pp.t
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 3c7ede3c9..ce74f2344 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -436,7 +436,7 @@ let start_proof_with_initialization kind sigma decl recguard thms snl hook =
let start_proof_com ?inference_hook kind thms hook =
let env0 = Global.env () in
let decl = fst (List.hd thms) in
- let evd, decl = Univdecls.interp_univ_decl_opt env0 (snd decl) in
+ let evd, decl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in
let evd, thms = List.fold_left_map (fun evd ((id, _), (bl, t)) ->
let evd, (impls, ((env, ctx), imps)) = interp_context_evars env0 evd bl in
let evd, (t', imps') = interp_type_evars_impls ~impls env evd t in
@@ -456,7 +456,7 @@ let start_proof_com ?inference_hook kind thms hook =
you look at the previous lines... *)
let thms = List.map (fun (n, (t, info)) -> (n, (nf_evar evd t, info))) thms in
let () =
- let open Misctypes in
+ let open UState in
if not (decl.univdecl_extensible_instance && decl.univdecl_extensible_constraints) then
ignore (Evd.check_univ_decl ~poly:(pi2 kind) evd decl)
in
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 398f7d6d0..c9e4876ee 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -21,13 +21,13 @@ val call_hook :
(** A hook start_proof calls on the type of the definition being started *)
val set_start_hook : (EConstr.types -> unit) -> unit
-val start_proof : Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map ->
+val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
?terminator:(Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) ->
?sign:Environ.named_context_val -> EConstr.types ->
?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards ->
unit declaration_hook -> unit
-val start_proof_univs : Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map ->
+val start_proof_univs : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
?terminator:(Proof_global.lemma_possible_guards -> (UState.t option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
?sign:Environ.named_context_val -> EConstr.types ->
?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards ->
@@ -39,7 +39,7 @@ val start_proof_com :
unit declaration_hook -> unit
val start_proof_with_initialization :
- goal_kind -> Evd.evar_map -> Univdecls.universe_decl ->
+ goal_kind -> Evd.evar_map -> UState.universe_decl ->
(bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option ->
(Id.t (* name of thm *) *
(EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 6ef8294df..1a3b1f39b 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -308,7 +308,7 @@ type program_info_aux = {
prg_body: constr;
prg_type: constr;
prg_ctx: UState.t;
- prg_univdecl: Univdecls.universe_decl;
+ prg_univdecl: UState.universe_decl;
prg_obligations: obligations;
prg_deps : Id.t list;
prg_fixkind : fixpoint_kind option ;
@@ -1099,7 +1099,7 @@ let show_term n =
Printer.pr_constr_env env sigma prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
++ Printer.pr_constr_env env sigma prg.prg_body)
-let add_definition n ?term t ctx ?(univdecl=Univdecls.default_univ_decl)
+let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls =
let sign = Decls.initialize_named_context_for_proof () in
@@ -1119,7 +1119,7 @@ let add_definition n ?term t ctx ?(univdecl=Univdecls.default_univ_decl)
| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
| _ -> res)
-let add_mutual_definitions l ctx ?(univdecl=Univdecls.default_univ_decl) ?tactic
+let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic
?(kind=Global,false,Definition) ?(reduce=reduce)
?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind =
let sign = Decls.initialize_named_context_for_proof () in
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 4b6165fb1..b1eaf51ac 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -54,7 +54,7 @@ val default_tactic : unit Proofview.tactic ref
val add_definition : Names.Id.t -> ?term:constr -> types ->
UState.t ->
- ?univdecl:Univdecls.universe_decl -> (* Universe binders and constraints *)
+ ?univdecl:UState.universe_decl -> (* Universe binders and constraints *)
?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list ->
?kind:Decl_kinds.definition_kind ->
?tactic:unit Proofview.tactic ->
@@ -72,7 +72,7 @@ val add_mutual_definitions :
(Names.Id.t * constr * types *
(Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
UState.t ->
- ?univdecl:Univdecls.universe_decl -> (* Universe binders and constraints *)
+ ?univdecl:UState.universe_decl -> (* Universe binders and constraints *)
?tactic:unit Proofview.tactic ->
?kind:Decl_kinds.definition_kind ->
?reduce:(constr -> constr) ->
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 3655947a5..7e67e12cb 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -55,7 +55,7 @@ open Pputils
(if extensible then str"+" else mt())
let pr_universe_decl l =
- let open Misctypes in
+ let open UState in
match l with
| None -> mt ()
| Some l ->
diff --git a/vernac/record.ml b/vernac/record.ml
index 5ff118473..e6a3afe4e 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -102,7 +102,7 @@ let binders_of_decls = List.map binder_of_decl
let typecheck_params_and_fields finite def id poly pl t ps nots fs =
let env0 = Global.env () in
- let sigma, decl = Univdecls.interp_univ_decl_opt env0 pl in
+ let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env0 pl in
let _ =
let error bk {CAst.loc; v=name} =
match bk, name with