aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitlab-ci.yml14
-rw-r--r--Makefile.ci3
-rwxr-xr-xdev/ci/ci-basic-overlay.sh7
-rwxr-xr-xdev/ci/ci-equations.sh2
-rwxr-xr-xdev/ci/ci-metacoq.sh8
-rw-r--r--doc/changelog/04-tactics/11362-micromega-fix-11191.rst5
-rw-r--r--doc/sphinx/changes.rst2
-rwxr-xr-xdoc/sphinx/conf.py2
-rw-r--r--doc/stdlib/hidden-files1
-rw-r--r--doc/tools/coqrst/coqdomain.py2
-rw-r--r--kernel/kernel.mllib2
-rw-r--r--kernel/reduction.ml2
-rw-r--r--kernel/relevanceops.ml (renamed from kernel/retypeops.ml)0
-rw-r--r--kernel/relevanceops.mli (renamed from kernel/retypeops.mli)0
-rw-r--r--kernel/term_typing.ml2
-rw-r--r--pretyping/indrec.ml15
-rw-r--r--pretyping/retyping.ml10
-rw-r--r--proofs/tacmach.mli12
-rw-r--r--theories/micromega/ZifyPow.v1
-rw-r--r--vernac/declareObl.ml35
-rw-r--r--vernac/declareObl.mli3
-rw-r--r--vernac/obligations.ml23
-rw-r--r--vernac/vernacentries.ml3
23 files changed, 93 insertions, 61 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 5b343a23c5..cf1dc47fab 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -731,10 +731,24 @@ plugin:ci-elpi:
plugin:ci-equations:
extends: .ci-template
+ artifacts:
+ name: "$CI_JOB_NAME"
+ paths:
+ - _build_ci
plugin:ci-fiat_parsers:
extends: .ci-template
+plugin:ci-metacoq:
+ extends: .ci-template
+ stage: stage-3
+ needs:
+ - build:base
+ - plugin:ci-equations
+ dependencies:
+ - build:base
+ - plugin:ci-equations
+
plugin:ci-mtac2:
extends: .ci-template
diff --git a/Makefile.ci b/Makefile.ci
index dfb3f69a8c..f58dd9f37a 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -33,6 +33,7 @@ CI_TARGETS= \
ci-iris-lambda-rust \
ci-math-classes \
ci-math-comp \
+ ci-metacoq \
ci-mtac2 \
ci-paramcoq \
ci-perennial \
@@ -72,6 +73,8 @@ ci-fiat-crypto: ci-coqprime ci-rewriter
ci-simple-io: ci-ext-lib
ci-quickchick: ci-ext-lib ci-simple-io
+ci-metacoq: ci-equations
+
# Generic rule, we use make to ease CI integration
$(CI_TARGETS): ci-%:
+./dev/ci/ci-wrapper.sh $*
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index bd7ee46358..70e3fe5c69 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -330,3 +330,10 @@
: "${perennial_CI_REF:=master}"
: "${perennial_CI_GITURL:=https://github.com/mit-pdos/perennial}"
: "${perennial_CI_ARCHIVEURL:=${perennial_CI_GITURL}/archive}"
+
+########################################################################
+# metacoq
+########################################################################
+: "${metacoq_CI_REF:=master}"
+: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/metacoq}"
+: "${metacoq_CI_ARCHIVEURL:=${metacoq_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh
index 871d033f5b..30047e624b 100755
--- a/dev/ci/ci-equations.sh
+++ b/dev/ci/ci-equations.sh
@@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")"
git_download equations
-( cd "${CI_BUILD_DIR}/equations" && ./configure.sh coq && make ci)
+( cd "${CI_BUILD_DIR}/equations" && ./configure.sh coq && make ci && make install )
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh
new file mode 100755
index 0000000000..1302065961
--- /dev/null
+++ b/dev/ci/ci-metacoq.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download metacoq
+
+( cd "${CI_BUILD_DIR}/metacoq" && ./configure.sh local && make ci-local && make install )
diff --git a/doc/changelog/04-tactics/11362-micromega-fix-11191.rst b/doc/changelog/04-tactics/11362-micromega-fix-11191.rst
index 79879c78d5..20d48929f2 100644
--- a/doc/changelog/04-tactics/11362-micromega-fix-11191.rst
+++ b/doc/changelog/04-tactics/11362-micromega-fix-11191.rst
@@ -1,5 +1,8 @@
- **Fixed:**
- Regression of :tacn:`lia` due to more powerful :tacn:`zify`
+ :tacn:`zify` now handles :g:`Z.pow_pos` by default.
+ In Coq 8.11, this was the case only when loading module
+ :g:`ZifyPow` because this triggered a regression of :tacn:`lia`.
+ The regression is now fixed, and the module kept only for compatibility
(`#11362 <https://github.com/coq/coq/pull/11362>`_,
fixes `#11191 <https://github.com/coq/coq/issues/11191>`_,
by Frédéric Besson).
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index a0cf9730a9..f76b60097a 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -4,7 +4,7 @@
Recent changes
--------------
-.. ifconfig:: not coq_config.is_a_released_version
+.. ifconfig:: not is_a_released_version
.. include:: ../unreleased.rst
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index c2c1c68f5c..2ed9ec21b3 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -100,7 +100,7 @@ def copy_formatspecific_files(app):
def setup(app):
app.connect('builder-inited', copy_formatspecific_files)
- app.add_config_value('coq_config', coq_config, 'env')
+ app.add_config_value('is_a_released_version', coq_config.is_a_released_version, 'env')
# The master toctree document.
# We create this file in `copy_master_doc` above.
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index 60d6039b0f..67d0b37e81 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -50,6 +50,7 @@ theories/micromega/ZifyInst.v
theories/micromega/ZifyBool.v
theories/micromega/ZifyComparison.v
theories/micromega/ZifyClasses.v
+theories/micromega/ZifyPow.v
theories/micromega/Zify.v
theories/nsatz/Nsatz.v
theories/omega/Omega.v
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 84f32e187b..0b94b0d675 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -519,7 +519,7 @@ class ProductionObject(CoqObject):
row = nodes.inline(classes=['prodn-row'])
entry = nodes.inline(classes=['prodn-cell-nonterminal'])
if lhs != "":
- target_name = 'grammar-token-' + lhs
+ target_name = 'grammar-token-' + nodes.make_id(lhs)
target = nodes.target('', '', ids=[target_name], names=[target_name])
# putting prodn-target on the target node won't appear in the tex file
inline = nodes.inline(classes=['prodn-target'])
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index f1e994b337..cc9da3a2ce 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -27,7 +27,7 @@ Conv_oracle
Environ
Primred
CClosure
-Retypeops
+Relevanceops
Reduction
Clambda
Nativelambda
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 5fbe501169..469d5ccaa2 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -331,7 +331,7 @@ let skip_pattern infos n c1 c2 =
let is_irrelevant infos lft c =
let env = info_env infos.cnv_inf in
- try Retypeops.relevance_of_fterm env infos.relevances lft c == Sorts.Irrelevant with _ -> false
+ try Relevanceops.relevance_of_fterm env infos.relevances lft c == Sorts.Irrelevant with _ -> false
(* Conversion between [lft1]term1 and [lft2]term2 *)
let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
diff --git a/kernel/retypeops.ml b/kernel/relevanceops.ml
index 3f3e722245..3f3e722245 100644
--- a/kernel/retypeops.ml
+++ b/kernel/relevanceops.ml
diff --git a/kernel/retypeops.mli b/kernel/relevanceops.mli
index 86734e747e..86734e747e 100644
--- a/kernel/retypeops.mli
+++ b/kernel/relevanceops.mli
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 0c89d51033..c8c2301171 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -143,7 +143,7 @@ let infer_declaration env (dcl : constant_entry) =
Cooking.cook_body = def;
cook_type = typ;
cook_universes = univs;
- cook_relevance = Retypeops.relevance_of_term env j.uj_val;
+ cook_relevance = Relevanceops.relevance_of_term env j.uj_val;
cook_inline = c.const_entry_inline_code;
cook_context = c.const_entry_secctx;
}
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index c92c9a75a0..b5d81f762a 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -530,22 +530,25 @@ let change_sort_arity sort =
corresponding eta-expanded term *)
let weaken_sort_scheme env evd set sort npars term ty =
let evdref = ref evd in
- let rec drec np elim =
+ let rec drec ctx np elim =
match kind elim with
| Prod (n,t,c) ->
+ let ctx = LocalAssum (n, t) :: ctx in
if Int.equal np 0 then
let osort, t' = change_sort_arity sort t in
evdref := (if set then Evd.set_eq_sort else Evd.set_leq_sort) env !evdref sort osort;
mkProd (n, t', c),
- mkLambda (n, t', mkApp(term,Termops.rel_vect 0 (npars+1)))
+ mkLambda (n, t', mkApp(term, Context.Rel.to_extended_vect mkRel 0 ctx))
else
- let c',term' = drec (np-1) c in
+ let c',term' = drec ctx (np-1) c in
mkProd (n, t, c'), mkLambda (n, t, term')
- | LetIn (n,b,t,c) -> let c',term' = drec np c in
- mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term')
+ | LetIn (n,b,t,c) ->
+ let ctx = LocalDef (n, b, t) :: ctx in
+ let c',term' = drec ctx np c in
+ mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term')
| _ -> anomaly ~label:"weaken_sort_scheme" (Pp.str "wrong elimination type.")
in
- let ty, term = drec npars ty in
+ let ty, term = drec [] npars ty in
!evdref, ty, term
(**********************************************************************)
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index d4fa2461b4..821c57d033 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -273,8 +273,8 @@ let relevance_of_term env sigma c =
| Rel n ->
let len = Range.length rels in
if n <= len then Range.get rels (n - 1)
- else Retypeops.relevance_of_rel env (n - len)
- | Var x -> Retypeops.relevance_of_var env x
+ else Relevanceops.relevance_of_rel env (n - len)
+ | Var x -> Relevanceops.relevance_of_var env x
| Sort _ -> Sorts.Relevant
| Cast (c, _, _) -> aux rels c
| Prod ({binder_relevance=r}, _, codom) ->
@@ -284,13 +284,13 @@ let relevance_of_term env sigma c =
| LetIn ({binder_relevance=r}, _, _, bdy) ->
aux (Range.cons r rels) bdy
| App (c, _) -> aux rels c
- | Const (c,_) -> Retypeops.relevance_of_constant env c
+ | Const (c,_) -> Relevanceops.relevance_of_constant env c
| Ind _ -> Sorts.Relevant
- | Construct (c,_) -> Retypeops.relevance_of_constructor env c
+ | Construct (c,_) -> Relevanceops.relevance_of_constructor env c
| Case (ci, _, _, _) -> ci.ci_relevance
| Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance
| CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance
- | Proj (p, _) -> Retypeops.relevance_of_projection env p
+ | Proj (p, _) -> Relevanceops.relevance_of_projection env p
| Int _ | Float _ -> Sorts.Relevant
| Meta _ | Evar _ -> Sorts.Relevant
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 19d4ed91e6..d8f7b7eed8 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -37,6 +37,7 @@ val pf_unsafe_type_of : Goal.goal sigma -> constr -> types
[@@ocaml.deprecated "Use [type_of] or retyping according to your needs."]
val pf_type_of : Goal.goal sigma -> constr -> evar_map * types
val pf_hnf_type_of : Goal.goal sigma -> constr -> types
+[@@ocaml.deprecated "This is a no-op now"]
val pf_get_hyp : Goal.goal sigma -> Id.t -> named_declaration
val pf_get_hyp_typ : Goal.goal sigma -> Id.t -> types
@@ -49,22 +50,33 @@ val pf_eapply : (env -> evar_map -> 'a -> evar_map * 'b) ->
val pf_reduce :
(env -> evar_map -> constr -> constr) ->
Goal.goal sigma -> constr -> constr
+[@@ocaml.deprecated "Use the version in Tacmach.New"]
+
val pf_e_reduce :
(env -> evar_map -> constr -> evar_map * constr) ->
Goal.goal sigma -> constr -> evar_map * constr
+[@@ocaml.deprecated "Use the version in Tacmach.New"]
val pf_whd_all : Goal.goal sigma -> constr -> constr
+[@@ocaml.deprecated "Use the version in Tacmach.New"]
val pf_hnf_constr : Goal.goal sigma -> constr -> constr
+[@@ocaml.deprecated "Use the version in Tacmach.New"]
val pf_nf : Goal.goal sigma -> constr -> constr
+[@@ocaml.deprecated "Use the version in Tacmach.New"]
val pf_nf_betaiota : Goal.goal sigma -> constr -> constr
val pf_reduce_to_quantified_ind : Goal.goal sigma -> types -> (inductive * EInstance.t) * types
val pf_reduce_to_atomic_ind : Goal.goal sigma -> types -> (inductive * EInstance.t) * types
+[@@ocaml.deprecated "Use Tacred.pf_reduce_to_atomic_ind"]
val pf_compute : Goal.goal sigma -> constr -> constr
+[@@ocaml.deprecated "Use the version in Tacmach.New"]
val pf_unfoldn : (occurrences * evaluable_global_reference) list
-> Goal.goal sigma -> constr -> constr
+[@@ocaml.deprecated "Use Tacred.unfoldn"]
val pf_const_value : Goal.goal sigma -> pconstant -> constr
+[@@ocaml.deprecated "Use Environ.constant_value_in"]
val pf_conv_x : Goal.goal sigma -> constr -> constr -> bool
+[@@ocaml.deprecated "Use the version in Tacmach.New"]
(** {6 Pretty-printing functions (debug only). } *)
val pr_gls : Goal.goal sigma -> Pp.t
diff --git a/theories/micromega/ZifyPow.v b/theories/micromega/ZifyPow.v
new file mode 100644
index 0000000000..d208696c0f
--- /dev/null
+++ b/theories/micromega/ZifyPow.v
@@ -0,0 +1 @@
+Require Export ZifyInst.
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 626dcd5d34..c13e884736 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -251,43 +251,22 @@ let get_prg_info_map () = !from_prg
let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m []
-let close sec =
+let check_can_close sec =
if not (ProgMap.is_empty !from_prg) then
let keys = map_keys !from_prg in
CErrors.user_err ~hdr:"Program"
Pp.(
str "Unsolved obligations when closing "
- ++ str sec ++ str ":" ++ spc ()
+ ++ Id.print sec ++ str ":" ++ spc ()
++ prlist_with_sep spc (fun x -> Id.print x) keys
++ ( str (if Int.equal (List.length keys) 1 then " has " else " have ")
++ str "unsolved obligations" ))
-let input : ProgramDecl.t CEphemeron.key ProgMap.t -> Libobject.obj =
- let open Libobject in
- declare_object
- { (default_object "Program state") with
- cache_function = (fun (na, pi) -> from_prg := pi)
- ; load_function = (fun _ (_, pi) -> from_prg := pi)
- ; discharge_function =
- (fun _ ->
- close "section";
- None )
- ; classify_function =
- (fun _ ->
- close "module";
- Dispose ) }
-
-let map_replace k v m =
- ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m)
-
-let progmap_remove prg =
- Lib.add_anonymous_leaf (input (ProgMap.remove prg.prg_name !from_prg))
-
-let progmap_add n prg =
- Lib.add_anonymous_leaf (input (ProgMap.add n prg !from_prg))
-
-let progmap_replace prg' =
- Lib.add_anonymous_leaf (input (map_replace prg'.prg_name prg' !from_prg))
+let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m)
+let prgmap_op f = from_prg := f !from_prg
+let progmap_remove prg = prgmap_op (ProgMap.remove prg.prg_name)
+let progmap_add n prg = prgmap_op (ProgMap.add n prg)
+let progmap_replace prg = prgmap_op (map_replace prg.prg_name prg)
let obligations_solved prg = Int.equal prg.prg_obligations.remaining 0
diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli
index 4e20c7c192..16c0413caf 100644
--- a/vernac/declareObl.mli
+++ b/vernac/declareObl.mli
@@ -139,6 +139,9 @@ val update_obls :
(** { 2 Util } *)
+(** Check obligations are properly solved before closing a section *)
+val check_can_close : Id.t -> unit
+
val get_prg_info_map : unit -> ProgramDecl.t CEphemeron.key ProgMap.t
val program_tcc_summary_tag :
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index f449cb02f1..a29ba44907 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -17,11 +17,8 @@ open Printf
- Apply term prefixed by quantification on "existentials".
*)
-open Term
open Constr
-open Vars
open Names
-open Evd
open Pp
open CErrors
open Util
@@ -41,7 +38,7 @@ let check_evars env evm =
(fun key evi ->
if Evd.is_obligation_evar evm key then ()
else
- let (loc,k) = evar_source key evm in
+ let (loc,k) = Evd.evar_source key evm in
Pretype_errors.error_unsolvable_implicit ?loc env evm key None)
(Evd.undefined_map evm)
@@ -133,14 +130,14 @@ let etype_of_evar evm evs hyps concl =
| LocalDef (id,c,_) ->
let c', s'', trans'' = subst_evar_constr evm evs n EConstr.mkVar c in
let c' = subst_vars acc 0 c' in
- mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest,
+ Term.mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest,
Int.Set.union s'' s',
Id.Set.union trans'' trans'
| LocalAssum (id,_) ->
- mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans')
+ Term.mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans')
| [] ->
- let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar concl in
- subst_vars acc 0 t', s, trans
+ let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar concl in
+ subst_vars acc 0 t', s, trans
in aux [] 0 (List.rev hyps)
let trunc_named_context n ctx =
@@ -152,14 +149,14 @@ let rec chop_product n t =
if Int.equal n 0 then Some t
else
match Constr.kind t with
- | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (pop b) else None
+ | Prod (_, _, b) -> if Vars.noccurn 1 b then chop_product (pred n) (pop b) else None
| _ -> None
let evar_dependencies evm oev =
let one_step deps =
Evar.Set.fold (fun ev s ->
let evi = Evd.find evm ev in
- let deps' = evars_of_filtered_evar_info evm evi in
+ let deps' = Evd.evars_of_filtered_evar_info evm evi in
if Evar.Set.mem oev deps' then
invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ Pp.string_of_ppcmds @@ Evar.print oev)
else Evar.Set.union deps' s)
@@ -215,13 +212,13 @@ let eterm_obligations env name evm fs ?status t ty =
(fun (id, (n, nstr), ev) l ->
let hyps = Evd.evar_filtered_context ev in
let hyps = trunc_named_context nc_len hyps in
- let evtyp, deps, transp = etype_of_evar evm l hyps ev.evar_concl in
+ let evtyp, deps, transp = etype_of_evar evm l hyps ev.Evd.evar_concl in
let evtyp, hyps, chop =
match chop_product fs evtyp with
| Some t -> t, trunc_named_context fs hyps, fs
| None -> evtyp, hyps, 0
in
- let loc, k = evar_source id evm in
+ let loc, k = Evd.evar_source id evm in
let status = match k with
| Evar_kinds.QuestionMark { Evar_kinds.qm_obligation=o } -> o
| _ -> match status with
@@ -282,7 +279,7 @@ let assumption_message = Declare.assumption_message
let default_tactic = ref (Proofview.tclUNIT ())
-let evar_of_obligation o = make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type)
+let evar_of_obligation o = Evd.make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type)
let subst_deps expand obls deps t =
let osubst = DeclareObl.obl_substitution expand obls deps in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 8a4522296f..d273573270 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -983,7 +983,7 @@ let vernac_begin_section ~poly ({v=id} as lid) =
to its current value ie noop. *)
set_bool_option_value_gen ~locality:OptLocal ["Universe"; "Polymorphism"] poly
-let vernac_end_section {CAst.loc} =
+let vernac_end_section {CAst.loc; v} =
Dumpglob.dump_reference ?loc
(DirPath.to_string (Lib.current_dirpath true)) "<>" "sec";
Lib.close_section ()
@@ -993,6 +993,7 @@ let vernac_name_sec_hyp {v=id} set = Proof_using.name_set id set
(* Dispatcher of the "End" command *)
let vernac_end_segment ({v=id} as lid) =
+ DeclareObl.check_can_close lid.v;
match Lib.find_opening_node id with
| Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid
| Lib.OpenedModule (true,_,_,_) -> vernac_end_modtype lid
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 03:33:05 +0000