diff options
41 files changed, 254 insertions, 222 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 20dac57a77..e56693eac2 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -268,7 +268,7 @@ ci-color: <<: *ci-template variables: <<: *ci-template-vars - EXTRA_PACKAGES: "$TIMING_PACKAGES subversion" + EXTRA_PACKAGES: "$TIMING_PACKAGES" ci-compcert: <<: *ci-template diff --git a/API/API.mli b/API/API.mli index 21d5ada764..3ed008ff5f 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1293,65 +1293,6 @@ sig type to_patch_substituted end -module Decl_kinds : -sig - type polymorphic = bool - type cumulative_inductive_flag = bool - type recursivity_kind = - | Finite - | CoFinite - | BiFinite - - type discharge = - | DoDischarge - | NoDischarge - - type locality = - | Discharge - | Local - | Global - - type definition_object_kind = - | Definition - | Coercion - | SubClass - | CanonicalStructure - | Example - | Fixpoint - | CoFixpoint - | Scheme - | StructureComponent - | IdentityCoercion - | Instance - | Method - | Let - type theorem_kind = - | Theorem - | Lemma - | Fact - | Remark - | Property - | Proposition - | Corollary - type goal_object_kind = - | DefinitionBody of definition_object_kind - | Proof of theorem_kind - type goal_kind = locality * polymorphic * goal_object_kind - type assumption_object_kind = - | Definitional - | Logical - | Conjectural - type logical_kind = - | IsAssumption of assumption_object_kind - | IsDefinition of definition_object_kind - | IsProof of theorem_kind - type binding_kind = - | Explicit - | Implicit - type private_flag = bool - type definition_kind = locality * polymorphic * definition_object_kind -end - module Retroknowledge : sig type action @@ -1501,10 +1442,15 @@ sig type record_body = (Id.t * Constant.t array * projection_body array) option + type recursivity_kind = + | Finite + | CoFinite + | BiFinite + type mutual_inductive_body = { mind_packets : one_inductive_body array; mind_record : record_body option; - mind_finite : Decl_kinds.recursivity_kind; + mind_finite : recursivity_kind; mind_ntypes : int; mind_hyps : Context.Named.t; mind_nparams : int; @@ -1578,7 +1524,7 @@ sig (** Some (Some id): primitive record with id the binder name of the record in projections. Some None: non-primitive record *) - mind_entry_finite : Decl_kinds.recursivity_kind; + mind_entry_finite : Declarations.recursivity_kind; mind_entry_params : (Id.t * local_entry) list; mind_entry_inds : one_inductive_entry list; mind_entry_universes : inductive_universes; @@ -2057,7 +2003,7 @@ end module Univops : sig - val universes_of_constr : Constr.constr -> Univ.LSet.t + val universes_of_constr : Environ.env -> Constr.constr -> Univ.LSet.t val restrict_universe_context : Univ.ContextSet.t -> Univ.LSet.t -> Univ.ContextSet.t end @@ -2210,6 +2156,66 @@ sig | SubEvar of Evar.t end +module Decl_kinds : +sig + type polymorphic = bool + type cumulative_inductive_flag = bool + type recursivity_kind = Declarations.recursivity_kind = + | Finite + | CoFinite + | BiFinite + [@@ocaml.deprecated "Please use [Declarations.recursivity_kind"] + + type discharge = + | DoDischarge + | NoDischarge + + type locality = + | Discharge + | Local + | Global + + type definition_object_kind = + | Definition + | Coercion + | SubClass + | CanonicalStructure + | Example + | Fixpoint + | CoFixpoint + | Scheme + | StructureComponent + | IdentityCoercion + | Instance + | Method + | Let + type theorem_kind = + | Theorem + | Lemma + | Fact + | Remark + | Property + | Proposition + | Corollary + type goal_object_kind = + | DefinitionBody of definition_object_kind + | Proof of theorem_kind + type goal_kind = locality * polymorphic * goal_object_kind + type assumption_object_kind = + | Definitional + | Logical + | Conjectural + type logical_kind = + | IsAssumption of assumption_object_kind + | IsDefinition of definition_object_kind + | IsProof of theorem_kind + type binding_kind = + | Explicit + | Implicit + type private_flag = bool + type definition_kind = locality * polymorphic * definition_object_kind +end + module Glob_term : sig type 'a cases_pattern_r = @@ -4001,7 +4007,7 @@ sig type instance_flag = bool option type coercion_flag = bool - type inductive_flag = Decl_kinds.recursivity_kind + type inductive_flag = Declarations.recursivity_kind type lname = Names.Name.t Loc.located type lident = Names.Id.t Loc.located type opacity_flag = @@ -4966,8 +4972,6 @@ sig val pf_conv_x : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr -> bool - val pf_is_matching : Goal.goal Evd.sigma -> Pattern.constr_pattern -> EConstr.constr -> bool - val pf_hyps_types : Goal.goal Evd.sigma -> (Names.Id.t * EConstr.types) list val pr_gls : Goal.goal Evd.sigma -> Pp.t @@ -6072,7 +6076,7 @@ sig val do_mutual_inductive : (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic -> - Decl_kinds.private_flag -> Decl_kinds.recursivity_kind -> unit + Decl_kinds.private_flag -> Declarations.recursivity_kind -> unit val do_definition : Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.universe_decl_expr option -> Constrexpr.local_binder_expr list -> Redexpr.red_expr option -> Constrexpr.constr_expr -> @@ -6098,7 +6102,7 @@ sig structured_inductive_expr -> Vernacexpr.decl_notation list -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic -> - Decl_kinds.private_flag -> Decl_kinds.recursivity_kind -> + Decl_kinds.private_flag -> Declarations.recursivity_kind -> Entries.mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list val declare_mutual_inductive_with_eliminations : @@ -30,7 +30,7 @@ package "lib" ( directory = "lib" - requires = "coq.config" + requires = "str, unix, threads, coq.config" archive(byte) = "clib.cma" archive(byte) += "lib.cma" @@ -65,7 +65,7 @@ package "kernel" ( directory = "kernel" - requires = "coq.lib, coq.vm" + requires = "dynlink, coq.lib, coq.vm" archive(byte) = "kernel.cma" archive(native) = "kernel.cmxa" @@ -168,7 +168,7 @@ package "parsing" ( description = "Coq Parsing Engine" version = "8.7" - requires = "coq.proofs" + requires = "camlp5.gramlib, coq.proofs" directory = "parsing" archive(byte) = "parsing.cma" diff --git a/Makefile.install b/Makefile.install index b590aad549..27694106fd 100644 --- a/Makefile.install +++ b/Makefile.install @@ -101,12 +101,16 @@ INSTALLCMI = $(sort \ $(foreach lib,$(CORECMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES))))) \ $(PLUGINS:.cmo=.cmi) +INSTALLCMX = $(sort $(filter-out checker/% ide/% tools/% dev/% configure.cmx, $(MLFILES:.ml=.cmx))) + install-devfiles: $(MKDIR) $(FULLBINDIR) $(INSTALLBIN) $(COQMKTOP) $(FULLBINDIR) $(MKDIR) $(FULLCOQLIB) $(INSTALLSH) $(FULLCOQLIB) $(GRAMMARCMA) $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI) + $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMX) + $(INSTALLSH) $(FULLCOQLIB) $(PLUGINSCMO:.cmo=.o) $(INSTALLSH) $(FULLCOQLIB) $(TOOLS_HELPERS) ifeq ($(BEST),opt) $(INSTALLSH) $(FULLCOQLIB) $(LINKCMX) $(CORECMA:.cma=.a) $(STATICPLUGINS:.cma=.a) diff --git a/default.nix b/default.nix index 5b5304e5a0..3dd24bac4d 100644 --- a/default.nix +++ b/default.nix @@ -55,6 +55,8 @@ stdenv.mkDerivation rec { ] else []) ++ (if lib.inNixShell then [ ocamlPackages.merlin + ocamlPackages.ocpIndent + ocamlPackages.ocp-index ] else []); src = diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 168a34e6e4..232b8a56e4 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -115,7 +115,8 @@ ######################################################################## # CoLoR ######################################################################## -: ${Color_CI_SVNURL:=https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color} +: ${CoLoR_CI_BRANCH:=master} +: ${CoLoR_CI_GITURL:=https://github.com/fblanqui/color.git} ######################################################################## # SF diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index 309050057c..c3ae7552a9 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -3,33 +3,11 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -Color_CI_DIR=${CI_BUILD_DIR}/color +CoLoR_CI_DIR=${CI_BUILD_DIR}/color # Setup Bignums - source ${ci_dir}/ci-bignums.sh -# Compiles CoLoR - -svn checkout ${Color_CI_SVNURL} ${Color_CI_DIR} - -sed -i -e "s/From Coq Require Import BigN/From Bignums Require Import BigN/" ${Color_CI_DIR}/Util/*/*.v -sed -i -e "s/From Coq Require Export BigN/From Bignums Require Export BigN/" ${Color_CI_DIR}/Util/*/*.v -sed -i -e "s/From Coq Require Import BigZ/From Bignums Require Import BigZ/" ${Color_CI_DIR}/Util/*/*.v -sed -i -e "s/From Coq Require Export BigZ/From Bignums Require Export BigZ/" ${Color_CI_DIR}/Util/*/*.v - -# Adapt to PR #220 (FunInd not loaded in Prelude anymore) -sed -i -e "15i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/basis/ordered_set.v -sed -i -e "8i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/equational_extension.v -sed -i -e "6i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/more_list_extention.v -sed -i -e "6i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/ring_extention.v -sed -i -e "27i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/dickson.v -sed -i -e "26i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_permut.v -sed -i -e "23i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_set.v -sed -i -e "25i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_sort.v -sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/more_list.v -sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/List/ListUtil.v -sed -i -e "17i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Multiset/MultisetOrder.v -sed -i -e "13i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Set/SetUtil.v - -( cd ${Color_CI_DIR} && make ) +# Compile CoLoR +git_checkout ${CoLoR_CI_BRANCH} ${CoLoR_CI_GITURL} ${CoLoR_CI_DIR} +( cd ${CoLoR_CI_DIR} && make ) diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index fc3cef3426..7bf2c7427d 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -8,4 +8,5 @@ CompCert_CI_DIR=${CI_BUILD_DIR}/CompCert opam install -j ${NJOBS} -y menhir git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR} -( cd ${CompCert_CI_DIR} && ./configure -ignore-coq-version x86_32-linux && make && make check-proof ) +#( cd ${CompCert_CI_DIR} && ./configure -ignore-coq-version x86_32-linux && make && make check-proof ) +( cd ${CompCert_CI_DIR} && ./configure -ignore-coq-version x86_32-linux && make ) diff --git a/dev/ci/ci-ltac2.sh b/dev/ci/ci-ltac2.sh index 4865be31ec..ed40036012 100755 --- a/dev/ci/ci-ltac2.sh +++ b/dev/ci/ci-ltac2.sh @@ -3,7 +3,7 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -ltac2_CI_DIR=${CI_BUILD_DIR}/coq-dpdgraph +ltac2_CI_DIR=${CI_BUILD_DIR}/ltac2 git_checkout ${ltac2_CI_BRANCH} ${ltac2_CI_GITURL} ${ltac2_CI_DIR} diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index 217540cc19..4e8c7e145e 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -3,13 +3,10 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -# XXX: Needs fixing to properly set the build directory. -wget ${sf_lf_CI_TARURL} -wget ${sf_plf_CI_TARURL} -wget ${sf_vfa_CI_TARURL} -tar xvfz lf.tgz -tar xvfz plf.tgz -tar xvfz vfa.tgz +mkdir -p ${CI_BUILD_DIR} && cd ${CI_BUILD_DIR} +wget -qO- ${sf_lf_CI_TARURL} | tar xvz +wget -qO- ${sf_plf_CI_TARURL} | tar xvz +wget -qO- ${sf_vfa_CI_TARURL} | tar xvz sed -i.bak '1i From Coq Require Extraction.' lf/Extraction.v sed -i.bak '1i From Coq Require Extraction.' vfa/Extract.v diff --git a/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh b/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh new file mode 100644 index 0000000000..7e9b5febdd --- /dev/null +++ b/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh @@ -0,0 +1,4 @@ +if [ "$TRAVIS_PULL_REQUEST" = "6324" ] || [ "$TRAVIS_BRANCH" = "fix-6323-restrict+abstract" ]; then + Equations_CI_BRANCH=fix-coq-6324 + Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations.git +fi diff --git a/engine/eConstr.ml b/engine/eConstr.ml index ea098902a2..d303038c5d 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -645,12 +645,25 @@ let eq_constr_universes_proj env sigma m n = let res = eq_constr' (unsafe_to_constr m) (unsafe_to_constr n) in if res then Some !cstrs else None -let universes_of_constr sigma c = +let universes_of_constr env sigma c = let open Univ in + let open Declarations in let rec aux s c = match kind sigma c with - | Const (_, u) | Ind (_, u) | Construct (_, u) -> - LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s + | Const (c, u) -> + begin match (Environ.lookup_constant c env).const_universes with + | Polymorphic_const _ -> + LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s + | Monomorphic_const (univs, _) -> + LSet.union s univs + end + | Ind ((mind,_), u) | Construct (((mind,_),_), u) -> + begin match (Environ.lookup_mind mind env).mind_universes with + | Cumulative_ind _ | Polymorphic_ind _ -> + LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s + | Monomorphic_ind (univs,_) -> + LSet.union s univs + end | Sort u -> let sort = ESorts.kind sigma u in if Sorts.is_small sort then s diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 771dbb8e88..f54c422adc 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -203,7 +203,7 @@ val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a (** Gather the universes transitively used in the term, including in the type of evars appearing in it. *) -val universes_of_constr : Evd.evar_map -> t -> Univ.LSet.t +val universes_of_constr : Environ.env -> Evd.evar_map -> t -> Univ.LSet.t (** {6 Substitutions} *) diff --git a/engine/uState.ml b/engine/uState.ml index c28e78f7da..6566ad989c 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -22,6 +22,7 @@ type uinfo = { type t = { uctx_names : Universes.universe_binders * uinfo Univ.LMap.t; uctx_local : Univ.ContextSet.t; (** The local context of variables *) + uctx_seff_univs : Univ.LSet.t; (** Local universes used through private constants *) uctx_univ_variables : Universes.universe_opt_subst; (** The local universes that are unification variables *) uctx_univ_algebraic : Univ.LSet.t; @@ -34,6 +35,7 @@ type t = let empty = { uctx_names = UNameMap.empty, Univ.LMap.empty; uctx_local = Univ.ContextSet.empty; + uctx_seff_univs = Univ.LSet.empty; uctx_univ_variables = Univ.LMap.empty; uctx_univ_algebraic = Univ.LSet.empty; uctx_universes = UGraph.initial_universes; @@ -60,6 +62,7 @@ let union ctx ctx' = else if is_empty ctx' then ctx else let local = Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local in + let seff = Univ.LSet.union ctx.uctx_seff_univs ctx'.uctx_seff_univs in let names = uname_union (fst ctx.uctx_names) (fst ctx'.uctx_names) in let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local) (Univ.ContextSet.levels ctx.uctx_local) in @@ -70,6 +73,7 @@ let union ctx ctx' = let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in { uctx_names = (names, names_rev); uctx_local = local; + uctx_seff_univs = seff; uctx_univ_variables = Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables; uctx_univ_algebraic = @@ -365,12 +369,21 @@ let check_univ_decl ~poly uctx decl = ctx let restrict ctx vars = + let vars = Univ.LSet.union vars ctx.uctx_seff_univs in let vars = Names.Id.Map.fold (fun na l vars -> Univ.LSet.add l vars) (fst ctx.uctx_names) vars in let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in { ctx with uctx_local = uctx' } +let demote_seff_univs entry uctx = + let open Entries in + match entry.const_entry_universes with + | Polymorphic_const_entry _ -> uctx + | Monomorphic_const_entry (univs, _) -> + let seff = Univ.LSet.union uctx.uctx_seff_univs univs in + { uctx with uctx_seff_univs = seff } + type rigid = | UnivRigid | UnivFlexible of bool (** Is substitution by an algebraic ok? *) @@ -552,7 +565,8 @@ let refresh_undefined_univ_variables uctx = let initial = declare uctx.uctx_initial_universes in let univs = declare UGraph.initial_universes in let uctx' = {uctx_names = uctx.uctx_names; - uctx_local = ctx'; + uctx_local = ctx'; + uctx_seff_univs = uctx.uctx_seff_univs; uctx_univ_variables = vars; uctx_univ_algebraic = alg; uctx_universes = univs; uctx_initial_universes = initial } in @@ -569,7 +583,8 @@ let normalize uctx = Universes.refresh_constraints uctx.uctx_initial_universes us' in { uctx_names = uctx.uctx_names; - uctx_local = us'; + uctx_local = us'; + uctx_seff_univs = uctx.uctx_seff_univs; (* not sure about this *) uctx_univ_variables = vars'; uctx_univ_algebraic = algs'; uctx_universes = universes; diff --git a/engine/uState.mli b/engine/uState.mli index fc98f492dc..6657d6047d 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -87,6 +87,8 @@ val universe_of_name : t -> Id.t -> Univ.Level.t val restrict : t -> Univ.LSet.t -> t +val demote_seff_univs : Safe_typing.private_constants Entries.definition_entry -> t -> t + type rigid = | UnivRigid | UnivFlexible of bool (** Is substitution by an algebraic ok? *) diff --git a/engine/univops.ml b/engine/univops.ml index 9a9ae12cab..df25d87252 100644 --- a/engine/univops.ml +++ b/engine/univops.ml @@ -9,12 +9,25 @@ open Univ open Constr -let universes_of_constr c = +let universes_of_constr env c = + let open Declarations in let rec aux s c = match kind c with - | Const (_, u) | Ind (_, u) | Construct (_, u) -> - LSet.fold LSet.add (Instance.levels u) s - | Sort u when not (Sorts.is_small u) -> + | Const (c, u) -> + begin match (Environ.lookup_constant c env).const_universes with + | Polymorphic_const _ -> + LSet.fold LSet.add (Instance.levels u) s + | Monomorphic_const (univs, _) -> + LSet.union s univs + end + | Ind ((mind,_), u) | Construct (((mind,_),_), u) -> + begin match (Environ.lookup_mind mind env).mind_universes with + | Cumulative_ind _ | Polymorphic_ind _ -> + LSet.fold LSet.add (Instance.levels u) s + | Monomorphic_ind (univs,_) -> + LSet.union s univs + end + | Sort u when not (Sorts.is_small u) -> let u = Sorts.univ_of_sort u in LSet.fold LSet.add (Universe.levels u) s | _ -> Constr.fold aux s c diff --git a/engine/univops.mli b/engine/univops.mli index 9af568bcb3..30fcc43681 100644 --- a/engine/univops.mli +++ b/engine/univops.mli @@ -9,7 +9,8 @@ open Constr open Univ -(** Shrink a universe context to a restricted set of variables *) +(** The universes of monomorphic constants appear. *) +val universes_of_constr : Environ.env -> constr -> LSet.t -val universes_of_constr : constr -> LSet.t +(** Shrink a universe context to a restricted set of variables *) val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index f6f46710c2..a561ea3703 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -82,7 +82,7 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } = "classifiers. Only one classifier is called.") ^ "\n"); (make_patt pt, ploc_vala None, - <:expr< fun loc -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>) + <:expr< fun () -> ( CErrors.anomaly (Pp.str "No classification given for command " ^ s ) ) >>) let make_fun_clauses loc s l = let map c = diff --git a/intf/decl_kinds.ml b/intf/decl_kinds.ml index 1dea6d9e98..b0c1f66613 100644 --- a/intf/decl_kinds.ml +++ b/intf/decl_kinds.ml @@ -75,7 +75,8 @@ type logical_kind = (** Recursive power of type declarations *) -type recursivity_kind = +type recursivity_kind = Declarations.recursivity_kind = | Finite (** = inductive *) | CoFinite (** = coinductive *) | BiFinite (** = non-recursive, like in "Record" definitions *) +[@@ocaml.deprecated "Please use [Declarations.recursivity_kind"] diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 5c9141fd6f..c7a9db1cbc 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -145,7 +145,7 @@ type coercion_flag = bool (* true = AddCoercion false = NoCoercion *) type instance_flag = bool option (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *) type export_flag = bool (* true = Export; false = Import *) -type inductive_flag = Decl_kinds.recursivity_kind +type inductive_flag = Declarations.recursivity_kind type onlyparsing_flag = Flags.compat_version option (* Some v = Parse only; None = Print also. If v<>Current, it contains the name of the coq version @@ -482,18 +482,39 @@ and vernac_argument_status = { implicit_status : vernac_implicit_status; } -(* A vernac classifier has to tell if a command: - vernac_when: has to be executed now (alters the parser) or later - vernac_type: if it is starts, ends, continues a proof or +(* A vernac classifier provides information about the exectuion of a + command: + + - vernac_when: encodes if the vernac may alter the parser [thus + forcing immediate execution], or if indeed it is pure and parsing + can continue without its execution. + + - vernac_type: if it is starts, ends, continues a proof or alters the global state or is a control command like BackTo or is - a query like Check *) + a query like Check. + + The classification works on the assumption that we have 3 states: + parsing, execution (global enviroment, etc...), and proof + state. For example, commands that only alter the proof state are + considered safe to delegate to a worker. + +*) type vernac_type = + (* Start of a proof *) | VtStartProof of vernac_start + (* Command altering the global state, bad for parallel + processing. *) | VtSideff of vernac_sideff_type + (* End of a proof *) | VtQed of vernac_qed_type + (* A proof step *) | VtProofStep of proof_step + (* To be removed *) | VtProofMode of string + (* Queries are commands assumed to be "pure", that is to say, they + don't modify the interpretation state. *) | VtQuery of vernac_part_of_script * Feedback.route_id + (* To be removed *) | VtMeta | VtUnknown and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index d5312c5006..7f4b85fd05 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -172,13 +172,18 @@ type abstract_inductive_universes = | Polymorphic_ind of Univ.AUContext.t | Cumulative_ind of Univ.ACumulativityInfo.t +type recursivity_kind = + | Finite (** = inductive *) + | CoFinite (** = coinductive *) + | BiFinite (** = non-recursive, like in "Record" definitions *) + type mutual_inductive_body = { mind_packets : one_inductive_body array; (** The component of the mutual inductive block *) mind_record : record_body option; (** The record information *) - mind_finite : Decl_kinds.recursivity_kind; (** Whether the type is inductive or coinductive *) + mind_finite : recursivity_kind; (** Whether the type is inductive or coinductive *) mind_ntypes : int; (** Number of types in the block *) diff --git a/kernel/entries.ml b/kernel/entries.ml index c44a17df2a..ca79de404d 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -51,7 +51,7 @@ type mutual_inductive_entry = { (** Some (Some id): primitive record with id the binder name of the record in projections. Some None: non-primitive record *) - mind_entry_finite : Decl_kinds.recursivity_kind; + mind_entry_finite : Declarations.recursivity_kind; mind_entry_params : (Id.t * local_entry) list; mind_entry_inds : one_inductive_entry list; mind_entry_universes : inductive_universes; diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index b0a76137b7..766adfc63a 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -141,7 +141,7 @@ let def_id = Id.of_string "def" let p_id = Id.of_string "p" let rec_res_id = Id.of_string "rec_res";; let lt = function () -> (coq_init_constant "lt") -let le = function () -> (coq_init_constant "le") +let le = function () -> (Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules "le") let ex = function () -> (coq_init_constant "ex") let nat = function () -> (coq_init_constant "nat") let iter_ref () = @@ -857,9 +857,13 @@ let rec prove_le g = Proofview.V82.of_tactic (apply (delayed_force le_n)); begin try - let matching_fun = - pf_is_matching g - (Pattern.PApp(Pattern.PRef (Globnames.global_of_constr (EConstr.Unsafe.to_constr (le ()))),[|Pattern.PVar (destVar sigma x);Pattern.PMeta None|])) in + let matching_fun c = match EConstr.kind sigma c with + | App (c, [| x0 ; _ |]) -> + EConstr.isVar sigma x0 && + Id.equal (destVar sigma x0) (destVar sigma x) && + is_global sigma (le ()) c + | _ -> false + in let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) in let y = diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 34fea6175b..8b9eb39837 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -471,7 +471,7 @@ END VERNAC COMMAND FUNCTIONAL EXTEND VernacTacticNotation | [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] => - [ VtUnknown, VtNow ] -> + [ VtSideff [], VtNow ] -> [ fun ~atts ~st -> let open Vernacinterp in let n = Option.default 0 n in Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n r e; diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index f22f00839a..e3e749b754 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -152,7 +152,8 @@ let ic_unsafe c = (*FIXME remove *) let decl_constant na univs c = let open Constr in - let vars = Univops.universes_of_constr c in + let env = Global.env () in + let vars = Univops.universes_of_constr env c in let univs = Univops.restrict_universe_context univs vars in let univs = Monomorphic_const_entry univs in mkConst(declare_constant (Id.of_string na) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 20ef65c884..478ba73fd5 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -13,7 +13,6 @@ open Util open Names open Globnames open Termops -open Reductionops open Term open EConstr open Vars @@ -207,7 +206,7 @@ let merge_binding sigma allow_bound_rels ctx n cT subst = in constrain sigma n c subst -let matches_core env sigma convert allow_partial_app allow_bound_rels +let matches_core env sigma allow_partial_app allow_bound_rels (binding_vars,pat) c = let open EConstr in let convref ref c = @@ -216,11 +215,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | ConstRef c, Const (c',_) -> Constant.equal c c' | IndRef i, Ind (i', _) -> Names.eq_ind i i' | ConstructRef c, Construct (c',u) -> Names.eq_constructor c c' - | _, _ -> - (if convert then - let sigma,c' = Evd.fresh_global env sigma ref in - is_conv env sigma (EConstr.of_constr c') c - else false) + | _, _ -> false in let rec sorec ctx env subst p t = let cT = strip_outer_cast sigma t in @@ -378,14 +373,14 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels in sorec [] env (Id.Map.empty, Id.Map.empty) pat c -let matches_core_closed env sigma convert allow_partial_app pat c = - let names, subst = matches_core env sigma convert allow_partial_app false pat c in +let matches_core_closed env sigma allow_partial_app pat c = + let names, subst = matches_core env sigma allow_partial_app false pat c in (names, Id.Map.map snd subst) -let extended_matches env sigma = matches_core env sigma false true true +let extended_matches env sigma = matches_core env sigma true true let matches env sigma pat c = - snd (matches_core_closed env sigma false true (Id.Set.empty,pat) c) + snd (matches_core_closed env sigma true (Id.Set.empty,pat) c) let special_meta = (-1) @@ -412,7 +407,7 @@ let matches_head env sigma pat c = (* Tells if it is an authorized occurrence and if the instance is closed *) let authorized_occ env sigma partial_app closed pat c mk_ctx = try - let subst = matches_core_closed env sigma false partial_app pat c in + let subst = matches_core_closed env sigma partial_app pat c in if closed && Id.Map.exists (fun _ c -> not (closed0 sigma c)) (snd subst) then (fun next -> next ()) else (fun next -> mkresult subst (mk_ctx (mkMeta special_meta)) next) @@ -552,10 +547,3 @@ let is_matching_appsubterm ?(closed=true) env sigma pat c = let pat = (Id.Set.empty,pat) in let results = sub_match ~partial_app:true ~closed env sigma pat c in not (IStream.is_empty results) - -let matches_conv env sigma p c = - snd (matches_core_closed env sigma true false (Id.Set.empty,p) c) - -let is_matching_conv env sigma pat n = - try let _ = matches_conv env sigma pat n in true - with PatternMatchingFailure -> false diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index 780ccc23d1..60e1c34a15 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -55,12 +55,6 @@ val is_matching : env -> Evd.evar_map -> constr_pattern -> constr -> bool prefix of it matches against [pat] *) val is_matching_head : env -> Evd.evar_map -> constr_pattern -> constr -> bool -(** [matches_conv env sigma] matches up to conversion in environment - [(env,sigma)] when constants in pattern are concerned; it raises - [PatternMatchingFailure] if not matchable; bindings are given in - increasing order based on the numbers given in the pattern *) -val matches_conv : env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map - (** The type of subterm matching results: a substitution + a context (whose hole is denoted here with [special_meta]) *) type matching_result = @@ -85,8 +79,3 @@ val match_subterm_gen : env -> Evd.evar_map -> (** [is_matching_appsubterm pat c] tells if a subterm of [c] matches against [pat] taking partial subterms into consideration *) val is_matching_appsubterm : ?closed:bool -> env -> Evd.evar_map -> constr_pattern -> constr -> bool - -(** [is_matching_conv env sigma pat c] tells if [c] matches against [pat] - up to conversion for constants in patterns *) -val is_matching_conv : - env -> Evd.evar_map -> constr_pattern -> constr -> bool diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 31a73db04f..6b503a0112 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -140,6 +140,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo let status = by tac in let _,(const,univs,_) = cook_proof () in Proof_global.discard_current (); + let univs = UState.demote_seff_univs const univs in const, status, univs with reraise -> let reraise = CErrors.push reraise in diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 535ef2013d..167d6bda0d 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -348,13 +348,9 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now nf t else t in - let used_univs_body = Univops.universes_of_constr body in - let used_univs_typ = Univops.universes_of_constr typ in - (* Universes for private constants are relevant to the body *) - let used_univs_body = - List.fold_left (fun acc (us,_) -> Univ.LSet.union acc us) - used_univs_body (Safe_typing.universes_of_private eff) - in + let env = Global.env () in + let used_univs_body = Univops.universes_of_constr env body in + let used_univs_typ = Univops.universes_of_constr env typ in if keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff) then let initunivs = UState.const_univ_entry ~poly initial_euctx in @@ -362,7 +358,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now (* For vi2vo compilation proofs are computed now but we need to complement the univ constraints of the typ with the ones of the body. So we keep the two sets distinct. *) - let used_univs = Univ.LSet.union used_univs_body used_univs_typ in + let used_univs = Univ.LSet.union used_univs_body used_univs_typ in let ctx_body = UState.restrict ctx used_univs in let univs = UState.check_mono_univ_decl ctx_body universe_decl in (initunivs, typ), ((body, univs), eff) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index a8ec4d8ca3..cab8d7b52a 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -102,9 +102,6 @@ let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind let pf_hnf_type_of gls = pf_get_type_of gls %> pf_whd_all gls -let pf_is_matching gl p c = pf_apply Constr_matching.is_matching_conv gl p c -let pf_matches gl p c = pf_apply Constr_matching.matches_conv gl p c - (********************************************) (* Definition of the most primitive tactics *) (********************************************) @@ -223,8 +220,6 @@ module New = struct let pf_hnf_type_of gl t = pf_whd_all gl (pf_get_type_of gl t) - let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t - let pf_whd_all gl t = pf_apply whd_all gl t let pf_compute gl t = pf_apply compute gl t diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index d9496d2b4f..e0fb8fbc5d 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -12,9 +12,7 @@ open Environ open EConstr open Proof_type open Redexpr -open Pattern open Locus -open Ltac_pretype (** Operations for handling terms under a local typing context. *) @@ -79,10 +77,6 @@ val pf_const_value : goal sigma -> pconstant -> constr val pf_conv_x : goal sigma -> constr -> constr -> bool val pf_conv_x_leq : goal sigma -> constr -> constr -> bool -val pf_matches : goal sigma -> constr_pattern -> constr -> patvar_map -val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool - - (** {6 The most primitive tactics. } *) val refiner : rule -> tactic @@ -138,8 +132,6 @@ module New : sig val pf_whd_all : 'a Proofview.Goal.t -> constr -> constr val pf_compute : 'a Proofview.Goal.t -> constr -> constr - val pf_matches : 'a Proofview.Goal.t -> constr_pattern -> constr -> patvar_map - val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr end diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 1ca572a36c..c5ae27a110 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -185,12 +185,12 @@ let rec classify_vernac e = (* These commands alter the parser *) | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _ | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _ - | VernacSyntaxExtension _ + | VernacSyntaxExtension _ | VernacSyntacticDefinition _ | VernacRequire _ | VernacImport _ | VernacInclude _ | VernacDeclareMLModule _ | VernacContext _ (* TASSI: unsure *) - | VernacProofMode _ + | VernacProofMode _ -> VtSideff [], VtNow (* These are ambiguous *) | VernacInstance _ -> VtUnknown, VtNow (* Stm will install a new classifier to handle these *) @@ -201,7 +201,7 @@ let rec classify_vernac e = (* What are these? *) | VernacToplevelControl _ | VernacRestoreState _ - | VernacWriteState _ -> VtUnknown, VtNow + | VernacWriteState _ -> VtSideff [], VtNow (* Plugins should classify their commands *) | VernacExtend (s,l) -> try List.assoc s !classifiers l () diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 8e851375a6..2c8ca19722 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -39,7 +39,6 @@ type testing_function = Evd.evar_map -> EConstr.constr -> bool let mkmeta n = Nameops.make_ident "X" (Some n) let meta1 = mkmeta 1 let meta2 = mkmeta 2 -let meta3 = mkmeta 3 let op2bool = function Some _ -> true | None -> false @@ -460,22 +459,6 @@ let find_this_eq_data_decompose gl eqn = user_err Pp.(str "Don't know what to do with JMeq on arguments not of same type.") in (lbeq,u,eq_args) -let match_eq_nf gls eqn (ref, hetero) = - let n = if hetero then 4 else 3 in - let args = List.init n (fun i -> mkGPatVar ("X" ^ string_of_int (i + 1))) in - let pat = mkPattern (mkGAppRef ref args) in - match Id.Map.bindings (pf_matches gls pat eqn) with - | [(m1,t);(m2,x);(m3,y)] -> - assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3); - (t,pf_whd_all gls x,pf_whd_all gls y) - | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms.") - -let dest_nf_eq gls eqn = - try - snd (first_match (match_eq_nf gls eqn) equalities) - with PatternMatchingFailure -> - user_err Pp.(str "Not an equality.") - (*** Sigma-types *) let match_sigma env sigma ex = diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 8ff6fe95c6..237ed42d55 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -144,9 +144,6 @@ val is_matching_sigma : Environ.env -> evar_map -> constr -> bool [t,u,T] and a boolean telling if equality is on the left side *) val match_eqdec : Environ.env -> evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr -(** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *) -val dest_nf_eq : 'a Proofview.Goal.t -> constr -> (constr * constr * constr) - (** Match a negation *) val is_matching_not : Environ.env -> evar_map -> constr -> bool val is_matching_imp_False : Environ.env -> evar_map -> constr -> bool diff --git a/tactics/inv.ml b/tactics/inv.ml index 46b10bf33e..cb0bbfd0e7 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -334,6 +334,16 @@ let remember_first_eq id x = if !x == MoveLast then x := MoveAfter id If it can discriminate then the goal is proved, if not tries to use it as a rewrite rule. It erases the clause which is given as input *) +let dest_nf_eq env sigma t = match EConstr.kind sigma t with +| App (r, [| t; x; y |]) -> + let open Reductionops in + let lazy eq = Coqlib.coq_eq_ref in + if EConstr.is_global sigma eq r then + (t, whd_all env sigma x, whd_all env sigma y) + else user_err Pp.(str "Not an equality.") +| _ -> + user_err Pp.(str "Not an equality.") + let projectAndApply as_mode thin avoid id eqname names depids = let subst_hyp l2r id = tclTHEN (tclTRY(rewriteInConcl l2r (EConstr.mkVar id))) @@ -344,7 +354,7 @@ let projectAndApply as_mode thin avoid id eqname names depids = let sigma = project gl in (** We only look at the type of hypothesis "id" *) let hyp = pf_nf_evar gl (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in - let (t,t1,t2) = Hipattern.dest_nf_eq gl hyp in + let (t,t1,t2) = dest_nf_eq (pf_env gl) sigma hyp in match (EConstr.kind sigma t1, EConstr.kind sigma t2) with | Var id1, _ -> generalizeRewriteIntros as_mode (subst_hyp true id) depids id1 | _, Var id2 -> generalizeRewriteIntros as_mode (subst_hyp false id) depids id2 diff --git a/test-suite/bugs/closed/6323.v b/test-suite/bugs/closed/6323.v new file mode 100644 index 0000000000..fdc33befc6 --- /dev/null +++ b/test-suite/bugs/closed/6323.v @@ -0,0 +1,9 @@ +Goal True. + simple refine (let X : Type := _ in _); + [ abstract exact Set using Set' + | let X' := (eval cbv delta [X] in X) in + clear X; + simple refine (let id' : { x : X' | True } -> X' := _ in _); + [ abstract refine (@proj1_sig _ _) | ] + ]. +Abort. diff --git a/vernac/classes.ml b/vernac/classes.ml index cb1d2f7c73..3e47f881c1 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -114,9 +114,10 @@ let instance_hook k info global imps ?hook cst = let declare_instance_constant k info global imps ?hook id decl poly evm term termtype = let kind = IsDefinition Instance in - let evm = - let levels = Univ.LSet.union (Univops.universes_of_constr termtype) - (Univops.universes_of_constr term) in + let evm = + let env = Global.env () in + let levels = Univ.LSet.union (Univops.universes_of_constr env termtype) + (Univops.universes_of_constr env term) in Evd.restrict_universe_context evm levels in let uctx = Evd.check_univ_decl ~poly evm decl in diff --git a/vernac/command.ml b/vernac/command.ml index 66d4fe9847..23be2c3082 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -105,7 +105,7 @@ let interp_definition pl bl poly red_option c ctypopt = let c = EConstr.Unsafe.to_constr c in let nf,subst = Evarutil.e_nf_evars_and_universes evdref in let body = nf (it_mkLambda_or_LetIn c ctx) in - let vars = EConstr.universes_of_constr !evdref (EConstr.of_constr body) in + let vars = EConstr.universes_of_constr env !evdref (EConstr.of_constr body) in let () = evdref := Evd.restrict_universe_context !evdref vars in let uctx = Evd.check_univ_decl ~poly !evdref decl in imps1@(Impargs.lift_implicits nb_args imps2), @@ -130,8 +130,8 @@ let interp_definition pl bl poly red_option c ctypopt = in if not (try List.for_all chk imps2 with Not_found -> false) then warn_implicits_in_term (); - let bodyvars = EConstr.universes_of_constr !evdref (EConstr.of_constr body) in - let tyvars = EConstr.universes_of_constr !evdref (EConstr.of_constr ty) in + let bodyvars = EConstr.universes_of_constr env !evdref (EConstr.of_constr body) in + let tyvars = EConstr.universes_of_constr env !evdref (EConstr.of_constr ty) in let vars = Univ.LSet.union bodyvars tyvars in let () = evdref := Evd.restrict_universe_context !evdref vars in let uctx = Evd.check_univ_decl ~poly !evdref decl in @@ -315,7 +315,7 @@ let do_assumptions kind nl l = let nf_evar c = EConstr.to_constr evd (EConstr.of_constr c) in let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) -> let t = nf_evar t in - let uvars = Univ.LSet.union uvars (Univops.universes_of_constr t) in + let uvars = Univ.LSet.union uvars (Univops.universes_of_constr env t) in uvars, (coe,t,imps)) Univ.LSet.empty l in @@ -1188,7 +1188,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind let env = Global.env() in let indexes = search_guard env indexes fixdecls in let fiximps = List.map (fun (n,r,p) -> r) fiximps in - let vars = Univops.universes_of_constr (mkFix ((indexes,0),fixdecls)) in + let vars = Univops.universes_of_constr env (mkFix ((indexes,0),fixdecls)) in let fixdecls = List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in let evd = Evd.from_ctx ctx in @@ -1221,7 +1221,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n let fixdefs = List.map Option.get fixdefs in let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in - let vars = Univops.universes_of_constr (List.hd fixdecls) in + let env = Global.env () in + let vars = Univops.universes_of_constr env (List.hd fixdecls) in let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in let evd = Evd.from_ctx ctx in diff --git a/vernac/command.mli b/vernac/command.mli index a1f916c782..c7342e6da9 100644 --- a/vernac/command.mli +++ b/vernac/command.mli @@ -82,7 +82,7 @@ type one_inductive_impls = val interp_mutual_inductive : structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag -> - polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> + polymorphic -> private_flag -> Declarations.recursivity_kind -> mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list (** Registering a mutual inductive definition together with its @@ -96,7 +96,7 @@ val declare_mutual_inductive_with_eliminations : val do_mutual_inductive : (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag -> - polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> unit + polymorphic -> private_flag -> Declarations.recursivity_kind -> unit (** {6 Fixpoints and cofixpoints} *) diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 24d6649515..4f011e6ade 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -477,7 +477,10 @@ let declare_definition prg = let fix_exn = Hook.get get_fix_exn () in let typ = nf typ in let body = nf body in - let uvars = Univ.LSet.union (Univops.universes_of_constr typ) (Univops.universes_of_constr body) in + let env = Global.env () in + let uvars = Univ.LSet.union + (Univops.universes_of_constr env typ) + (Univops.universes_of_constr env body) in let uctx = UState.restrict prg.prg_ctx uvars in let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl in let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in diff --git a/vernac/record.mli b/vernac/record.mli index 9fdd5e1c46..e632e7bbff 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -15,7 +15,7 @@ val primitive_flag : bool ref val definition_structure : inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic * - Decl_kinds.recursivity_kind * ident_decl with_coercion * local_binder_expr list * + Declarations.recursivity_kind * ident_decl with_coercion * local_binder_expr list * (local_decl_expr with_instance with_priority with_notation) list * Id.t * constr_expr option -> global_reference |