aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitlab-ci.yml23
-rw-r--r--Makefile.ci2
-rwxr-xr-xdev/ci/ci-fiat_crypto.sh4
-rwxr-xr-xdev/ci/ci-fiat_crypto_ocaml.sh8
-rw-r--r--doc/changelog/02-specification-language/12422-master+fix-12418-cases-anomaly.rst5
-rw-r--r--doc/changelog/04-tactics/12399-rm-prolog.rst4
-rw-r--r--doc/changelog/08-tools/12389-coq_makefile.rst5
-rw-r--r--doc/sphinx/practical-tools/utilities.rst4
-rw-r--r--plugins/ltac/g_auto.mlg5
-rw-r--r--plugins/ssrsearch/g_search.mlg2
-rw-r--r--pretyping/cases.ml2
-rw-r--r--tactics/eauto.ml25
-rw-r--r--tactics/eauto.mli2
-rw-r--r--test-suite/bugs/closed/bug_12418.v29
-rw-r--r--tools/CoqMakefile.in28
-rw-r--r--user-contrib/Ltac2/g_ltac2.mlg2
-rw-r--r--vernac/comFixpoint.ml2
-rw-r--r--vernac/declare.ml130
-rw-r--r--vernac/declare.mli14
-rw-r--r--vernac/mltop.ml3
-rw-r--r--vernac/obligations.mli1
21 files changed, 181 insertions, 119 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 87101ecae7..e8244fafc8 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -6,6 +6,7 @@ stages:
- stage-2 # Only dependencies in stage 1
- stage-3 # Only dependencies in stage 1 and 2
- stage-4 # Only dependencies in stage 1, 2 and 3
+ - stage-5 # Only dependencies in stage 1, 2, 3, and 4
- deploy
# When a job has no dependencies, it goes to stage 1. Otherwise, we
@@ -704,12 +705,13 @@ library:ci-engine_bench:
library:ci-fcsl_pcm:
extends: .ci-template
-# We cannot use flambda due to
-# https://github.com/ocaml/ocaml/issues/7842, see
-# https://github.com/coq/coq/pull/11916#issuecomment-609977375
library:ci-fiat_crypto:
- extends: .ci-template
+ extends: .ci-template-flambda
stage: stage-4
+ artifacts:
+ name: "$CI_JOB_NAME"
+ paths:
+ - _build_ci
needs:
- build:edge+flambda
- library:ci-coqprime
@@ -720,6 +722,19 @@ library:ci-fiat_crypto:
- library:ci-coqprime
- plugin:ci-rewriter
+# We cannot use flambda due to
+# https://github.com/ocaml/ocaml/issues/7842, see
+# https://github.com/coq/coq/pull/11916#issuecomment-609977375
+library:ci-fiat_crypto_ocaml:
+ extends: .ci-template
+ stage: stage-5
+ needs:
+ - build:edge+flambda
+ - library:ci-fiat_crypto
+ dependencies:
+ - build:edge+flambda
+ - library:ci-fiat_crypto
+
library:ci-flocq:
extends: .ci-template-flambda
artifacts:
diff --git a/Makefile.ci b/Makefile.ci
index 9b7008f765..9231fa6fed 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -28,6 +28,7 @@ CI_TARGETS= \
ci-equations \
ci-fcsl_pcm \
ci-fiat_crypto \
+ ci-fiat_crypto_ocaml \
ci-fiat_parsers \
ci-flocq \
ci-geocoq \
@@ -72,6 +73,7 @@ ci-corn: ci-math_classes
ci-mtac2: ci-unicoq
ci-fiat_crypto: ci-coqprime ci-rewriter
+ci-fiat_crypto_ocaml: ci-fiat_crypto
ci-simple_io: ci-ext_lib
ci-quickchick: ci-ext_lib ci-simple_io
diff --git a/dev/ci/ci-fiat_crypto.sh b/dev/ci/ci-fiat_crypto.sh
index 811fefda35..3ecdb32a51 100755
--- a/dev/ci/ci-fiat_crypto.sh
+++ b/dev/ci/ci-fiat_crypto.sh
@@ -15,8 +15,8 @@ fiat_crypto_CI_STACKSIZE=32768
# bedrock2, so we use the pinned version of bedrock2, but the external
# version of other developments
fiat_crypto_CI_MAKE_ARGS="EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1"
-fiat_crypto_CI_TARGETS1="${fiat_crypto_CI_MAKE_ARGS} standalone-ocaml c-files rust-files printlite lite"
-fiat_crypto_CI_TARGETS2="${fiat_crypto_CI_MAKE_ARGS} all"
+fiat_crypto_CI_TARGETS1="${fiat_crypto_CI_MAKE_ARGS} pre-standalone-extracted printlite lite"
+fiat_crypto_CI_TARGETS2="${fiat_crypto_CI_MAKE_ARGS} all-except-compiled"
( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \
ulimit -s ${fiat_crypto_CI_STACKSIZE} && \
diff --git a/dev/ci/ci-fiat_crypto_ocaml.sh b/dev/ci/ci-fiat_crypto_ocaml.sh
new file mode 100755
index 0000000000..20d3deb14f
--- /dev/null
+++ b/dev/ci/ci-fiat_crypto_ocaml.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+fiat_crypto_CI_MAKE_ARGS="EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1"
+
+( cd "${CI_BUILD_DIR}/fiat_crypto" && make ${fiat_crypto_CI_MAKE_ARGS} standalone-ocaml lite-generated-files )
diff --git a/doc/changelog/02-specification-language/12422-master+fix-12418-cases-anomaly.rst b/doc/changelog/02-specification-language/12422-master+fix-12418-cases-anomaly.rst
new file mode 100644
index 0000000000..8f126c5b6f
--- /dev/null
+++ b/doc/changelog/02-specification-language/12422-master+fix-12418-cases-anomaly.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+ Case of an anomaly in trying to infer the return clause of an ill-typed :g:`match`
+ (`#12422 <https://github.com/coq/coq/pull/12422>`_,
+ fixes `#12418 <https://github.com/coq/coq/pull/12418>`_,
+ by Hugo Herbelin).
diff --git a/doc/changelog/04-tactics/12399-rm-prolog.rst b/doc/changelog/04-tactics/12399-rm-prolog.rst
new file mode 100644
index 0000000000..afde7db370
--- /dev/null
+++ b/doc/changelog/04-tactics/12399-rm-prolog.rst
@@ -0,0 +1,4 @@
+- **Removed:**
+ The deprecated and undocumented "prolog" tactic was removed
+ (`#12399 <https://github.com/coq/coq/pull/12399>`_,
+ by Pierre-Marie Pédrot).
diff --git a/doc/changelog/08-tools/12389-coq_makefile.rst b/doc/changelog/08-tools/12389-coq_makefile.rst
new file mode 100644
index 0000000000..74e3a68170
--- /dev/null
+++ b/doc/changelog/08-tools/12389-coq_makefile.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+ Adding the possibility in coq_makefile to directly set the installation folders,
+ through the :n:`COQLIBINSTALL` and :n:`COQDOCINSTALL` variables.
+ See :ref:`coqmakefilelocal`.
+ (`#12389 <https://github.com/coq/coq/pull/12389>`_, by Martin Bodin, review of Enrico Tassi).
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 408f8fc3ec..33ebbce640 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -170,6 +170,10 @@ Here we describe only few of them.
override the flags passed to ``coqdoc``. By default ``-interpolate -utf8``.
:COQDOCEXTRAFLAGS:
extend the flags passed to ``coqdoc``
+:COQLIBINSTALL, COQDOCINSTALL:
+ specify where the Coq libraries and documentation will be installed.
+ By default a combination of ``$(DESTDIR)`` (if defined) with
+ ``$(COQLIB)/user-contrib`` and ``$(DOCDIR)/user-contrib``.
**Rule extension**
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index b4527694ae..2e72ceae5a 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -114,11 +114,6 @@ END
(** Eauto *)
-TACTIC EXTEND prolog DEPRECATED { Deprecation.make ~note:"Use eauto instead" () }
-| [ "prolog" "[" uconstr_list(l) "]" int_or_var(n) ] ->
- { Eauto.prolog_tac (eval_uconstrs ist l) n }
-END
-
{
let make_depth n = snd (Eauto.make_dimension n None)
diff --git a/plugins/ssrsearch/g_search.mlg b/plugins/ssrsearch/g_search.mlg
index 6d68cc13ab..f5cbf2005b 100644
--- a/plugins/ssrsearch/g_search.mlg
+++ b/plugins/ssrsearch/g_search.mlg
@@ -2,6 +2,8 @@
(* Main prefilter *)
+DECLARE PLUGIN "ssrsearch_plugin"
+
{
module CoqConstr = Constr
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 5e3fb9dae3..25353b7c12 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1716,7 +1716,7 @@ let abstract_tycon ?loc env sigma subst tycon extenv t =
let flags = (default_flags_of TransparentState.full) in
match solve_simple_eqn evar_unify flags !!env sigma (None,ev,substl inst ev') with
| Success evd -> evdref := evd
- | UnifFailure _ -> assert false
+ | UnifFailure _ -> evdref := add_conv_pb (Reduction.CONV,!!env,substl inst ev',t) sigma
end;
ev'
| _ ->
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 710e0a6808..7d8620468d 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -77,31 +77,6 @@ let apply_tac_list tac glls =
re_sig (pack.it @ rest) pack.sigma
| _ -> user_err Pp.(str "apply_tac_list")
-let one_step l gl =
- [Proofview.V82.of_tactic Tactics.intro]
- @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) (List.map mkVar (pf_ids_of_hyps gl)))
- @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) l)
- @ (List.map (fun c -> Proofview.V82.of_tactic (assumption c)) (pf_ids_of_hyps gl))
-
-let rec prolog l n gl =
- if n <= 0 then user_err Pp.(str "prolog - failure");
- let prol = (prolog l (n-1)) in
- (tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl
-
-let prolog_tac l n =
- Proofview.V82.tactic begin fun gl ->
- let map c =
- let (sigma, c) = c (pf_env gl) (project gl) in
- (* Dropping the universe context is probably wrong *)
- let (c, _) = pf_apply (prepare_hint false) gl (sigma, c) in
- c
- in
- let l = List.map map l in
- try (prolog l n gl)
- with UserError (Some "Refiner.tclFIRST",_) ->
- user_err ~hdr:"Prolog.prolog" (str "Prolog failed.")
- end
-
open Auto
(***************************************************************************)
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index e6f2c1a8e2..5fb038a767 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -18,8 +18,6 @@ val registered_e_assumption : unit Proofview.tactic
val e_give_exact : ?flags:Unification.unify_flags -> constr -> unit Proofview.tactic
-val prolog_tac : delayed_open_constr list -> int -> unit Proofview.tactic
-
val gen_eauto : ?debug:debug -> bool * int -> delayed_open_constr list ->
hint_db_name list option -> unit Proofview.tactic
diff --git a/test-suite/bugs/closed/bug_12418.v b/test-suite/bugs/closed/bug_12418.v
new file mode 100644
index 0000000000..cf11ea627b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12418.v
@@ -0,0 +1,29 @@
+(* The second "match" below used to raise an anomaly *)
+
+Class Monad@{d c} (m : Type@{d} -> Type@{c}) : Type :=
+ { ret : forall {t : Type@{d}}, t -> m t }.
+
+Record state {S : Type} (t : Type) : Type := mkState { runState : t }.
+
+Global Declare Instance Monad_state : forall S, Monad (@state S).
+
+Class Cava := {
+ constant : bool -> unit;
+ constant_vec : unit;
+}.
+
+Axiom F : forall {A : Type}, (bool -> A) -> Datatypes.unit.
+
+Fail Instance T : Cava := {
+
+ constant b := match b with
+ | true => ret tt
+ | false => ret tt
+ end;
+
+ constant_vec := @F _ (fun b => match b with
+ | true => tt
+ | false => tt
+ end);
+
+}.
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index a26eb9dfbe..e2ed2db728 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -146,6 +146,21 @@ TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line
TGTS ?=
+# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not)
+ifdef DSTROOT
+DESTDIR := $(DSTROOT)
+endif
+
+# Substitution of the path by appending $(DESTDIR) if needed.
+# The variable $(COQMF_WINDRIVE) can be needed for Cygwin environments.
+windrive_path = $(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(1)),$(1))
+destination_path = $(if $(DESTDIR),$(DESTDIR)/$(call windrive_path,$(1)),$(1))
+
+# Installation paths of libraries and documentation.
+COQLIBINSTALL ?= $(call destination_path,$(COQLIB)/user-contrib)
+COQDOCINSTALL ?= $(call destination_path,$(DOCDIR)/user-contrib)
+COQTOPINSTALL ?= $(call destination_path,$(COQLIB)/toploop) # FIXME: Unused variable?
+
########## End of parameters ##################################################
# What follows may be relevant to you only if you need to
# extend this Makefile. If so, look for 'Extension point' here and
@@ -227,17 +242,6 @@ else
TIMING_ARG=
endif
-# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not)
-ifdef DSTROOT
-DESTDIR := $(DSTROOT)
-endif
-
-concat_path = $(if $(1),$(1)/$(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(2)),$(2)),$(2))
-
-COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/user-contrib)
-COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)/user-contrib)
-COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/toploop)
-
# Files #######################################################################
#
# We here define a bunch of variables about the files being part of the
@@ -577,7 +581,7 @@ uninstall::
instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\
rm -f "$$instf" &&\
echo RM "$$instf" &&\
- (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" 2>/dev/null || true); \
+ (rmdir "$(COQLIBINSTALL)/$$df/" 2>/dev/null || true); \
done
.PHONY: uninstall
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 8979170026..3af39ec59a 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -8,6 +8,8 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+DECLARE PLUGIN "ltac2_plugin"
+
{
open Pp
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 80ca85e9a6..0b75e7f410 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -285,7 +285,7 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt
let fix_kind = Decls.IsDefinition fix_kind in
let _ : GlobRef.t list =
Declare.declare_mutually_recursive ~scope ~opaque:false ~kind:fix_kind ~poly ~uctx
- ~possible_indexes:indexes ~restrict_ucontext:true ~udecl ~ntns ~rec_declaration
+ ~possible_indexes:indexes ~udecl ~ntns ~rec_declaration
fixitems
in
()
diff --git a/vernac/declare.ml b/vernac/declare.ml
index c77d4909da..6ed7a9e39d 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -138,7 +138,9 @@ type 'a proof_entry = {
let default_univ_entry = Entries.Monomorphic_entry Univ.ContextSet.empty
-let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types
+(** [univsbody] are universe-constraints attached to the body-only,
+ used in vio-delayed opaque constants and private poly universes *)
+let definition_entry_core ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types
?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) ?(univsbody=Univ.ContextSet.empty) body =
{ proof_entry_body = Future.from_val ?fix_exn ((body,univsbody), eff);
proof_entry_secctx = section_vars;
@@ -148,6 +150,9 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?sect
proof_entry_feedback = feedback_id;
proof_entry_inline_code = inline}
+let definition_entry =
+ definition_entry_core ?fix_exn:None ?eff:None ?univsbody:None ?feedback_id:None ?section_vars:None
+
type proof_object =
{ name : Names.Id.t
(* [name] only used in the STM *)
@@ -173,11 +178,17 @@ let prepare_proof ~unsafe_typ { proof } =
let evd = Evd.minimize_universes evd in
let to_constr_body c =
match EConstr.to_constr_opt evd c with
- | Some p -> p
- | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain")
+ | Some p ->
+ Vars.universes_of_constr p, p
+ | None ->
+ CErrors.user_err Pp.(str "Some unresolved existential variables remain")
in
let to_constr_typ t =
- if unsafe_typ then EConstr.Unsafe.to_constr t else to_constr_body t
+ if unsafe_typ
+ then
+ let t = EConstr.Unsafe.to_constr t in
+ Vars.universes_of_constr t, t
+ else to_constr_body t
in
(* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
side-effects... This may explain why one need to uniquize side-effects
@@ -194,6 +205,40 @@ let prepare_proof ~unsafe_typ { proof } =
let proofs = List.map (fun (body, typ) -> (to_constr_body body, eff), to_constr_typ typ) initial_goals in
proofs, Evd.evar_universe_context evd
+let make_univs_deferred ~poly ~initial_euctx ~uctx ~udecl
+ (used_univs_typ, typ) (used_univs_body, body) =
+ let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
+ let utyp = UState.univ_entry ~poly initial_euctx in
+ let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in
+ (* 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 uctx_body = UState.restrict uctx used_univs in
+ let ubody = UState.check_mono_univ_decl uctx_body udecl in
+ utyp, ubody
+
+let make_univs_private_poly ~poly ~uctx ~udecl (used_univs_typ, typ) (used_univs_body, body) =
+ let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
+ let universes = UState.restrict uctx used_univs in
+ let typus = UState.restrict universes used_univs_typ in
+ let utyp = UState.check_univ_decl ~poly typus udecl in
+ let ubody = Univ.ContextSet.diff
+ (UState.context_set universes)
+ (UState.context_set typus)
+ in
+ utyp, ubody
+
+let make_univs ~poly ~uctx ~udecl (used_univs_typ, typ) (used_univs_body, body) =
+ let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
+ (* Since the proof is computed now, we can simply have 1 set of
+ constraints in which we merge the ones for the body and the ones
+ for the typ. We recheck the declaration after restricting with
+ the actually used universes.
+ TODO: check if restrict is really necessary now. *)
+ let ctx = UState.restrict uctx used_univs in
+ let utyp = UState.check_univ_decl ~poly ctx udecl in
+ utyp, Univ.ContextSet.empty
+
let close_proof ~opaque ~keep_body_ucst_separate ps =
let { section_vars; proof; udecl; initial_euctx } = ps in
@@ -202,46 +247,19 @@ let close_proof ~opaque ~keep_body_ucst_separate ps =
let elist, uctx = prepare_proof ~unsafe_typ ps in
let opaque = match opaque with Opaque -> true | Transparent -> false in
- let make_entry ((body, eff), typ) =
-
- let allow_deferred =
- not poly &&
- (keep_body_ucst_separate
- || not (Safe_typing.is_empty_private_constants eff.Evd.seff_private))
- in
- let used_univs_body = Vars.universes_of_constr body in
- let used_univs_typ = Vars.universes_of_constr typ in
- let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
+ let make_entry ((((_ub, body) as b), eff), ((_ut, typ) as t)) =
let utyp, ubody =
- if allow_deferred then
- let utyp = UState.univ_entry ~poly initial_euctx in
- let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in
- (* 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 uctx_body = UState.restrict uctx used_univs in
- let ubody = UState.check_mono_univ_decl uctx_body udecl in
- utyp, ubody
- else if poly && opaque && private_poly_univs () then
- let universes = UState.restrict uctx used_univs in
- let typus = UState.restrict universes used_univs_typ in
- let utyp = UState.check_univ_decl ~poly typus udecl in
- let ubody = Univ.ContextSet.diff
- (UState.context_set universes)
- (UState.context_set typus)
- in
- utyp, ubody
- else
- (* Since the proof is computed now, we can simply have 1 set of
- constraints in which we merge the ones for the body and the ones
- for the typ. We recheck the declaration after restricting with
- the actually used universes.
- TODO: check if restrict is really necessary now. *)
- let ctx = UState.restrict uctx used_univs in
- let utyp = UState.check_univ_decl ~poly ctx udecl in
- utyp, Univ.ContextSet.empty
+ (* allow_deferred case *)
+ if not poly &&
+ (keep_body_ucst_separate
+ || not (Safe_typing.is_empty_private_constants eff.Evd.seff_private))
+ then make_univs_deferred ~initial_euctx ~poly ~uctx ~udecl t b
+ (* private_poly_univs case *)
+ else if poly && opaque && private_poly_univs ()
+ then make_univs_private_poly ~poly ~uctx ~udecl t b
+ else make_univs ~poly ~uctx ~udecl t b
in
- definition_entry ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body
+ definition_entry_core ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body
in
let entries = CList.map make_entry elist in
{ name; entries; uctx }
@@ -734,7 +752,7 @@ let return_partial_proof { proof } =
let return_proof ps =
let p, uctx = prepare_proof ~unsafe_typ:false ps in
- List.map fst p, uctx
+ List.map (fun (((_ub, body),eff),_) -> (body,eff)) p, uctx
let update_global_env =
map_proof (fun p ->
@@ -889,7 +907,7 @@ module Hook = struct
end
(* Locality stuff *)
-let declare_entry ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ~uctx entry =
+let declare_entry_core ~name ~scope ~kind ?hook ~obls ~impargs ~uctx entry =
let should_suggest = entry.proof_entry_opaque &&
Option.is_empty entry.proof_entry_secctx in
let ubind = UState.universe_binders uctx in
@@ -910,6 +928,8 @@ let declare_entry ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ~uctx entry =
Option.iter (fun hook -> Hook.call ~hook { Hook.S.uctx; obls; scope; dref }) hook;
dref
+let declare_entry = declare_entry_core ~obls:[]
+
let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes =
match possible_indexes with
| Some possible_indexes ->
@@ -936,7 +956,7 @@ module Recthm = struct
}
end
-let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems =
+let declare_mutually_recursive_core ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems =
let vars, fixdecls, indexes =
mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in
let uctx, univs =
@@ -962,6 +982,8 @@ let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~re
List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
csts
+let declare_mutually_recursive = declare_mutually_recursive_core ~restrict_ucontext:true
+
let warn_let_as_axiom =
CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++
@@ -998,14 +1020,16 @@ let prepare_definition ?opaque ?inline ?fix_exn ~poly ~udecl ~types ~body sigma
sigma (fun nf -> nf body, Option.map nf types)
in
let univs = Evd.check_univ_decl ~poly sigma udecl in
- let entry = definition_entry ?fix_exn ?opaque ?inline ?types ~univs body in
+ let entry = definition_entry_core ?fix_exn ?opaque ?inline ?types ~univs body in
let uctx = Evd.evar_universe_context sigma in
entry, uctx
-let declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook
- ?obls ~poly ?inline ~types ~body ?fix_exn sigma =
+let declare_definition_core ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook
+ ~obls ~poly ?inline ~types ~body ?fix_exn sigma =
let entry, uctx = prepare_definition ?fix_exn ~opaque ~poly ~udecl ~types ~body ?inline sigma in
- declare_entry ~name ~scope ~kind ~impargs ?obls ?hook ~uctx entry
+ declare_entry_core ~name ~scope ~kind ~impargs ~obls ?hook ~uctx entry
+
+let declare_definition = declare_definition_core ~obls:[]
let prepare_obligation ~name ~types ~body sigma =
let env = Global.env () in
@@ -1255,8 +1279,8 @@ let not_transp_msg =
++ spc ()
++ str "Use 'Defined' instead.")
-let pperror cmd = CErrors.user_err ~hdr:"Program" cmd
-let err_not_transp () = pperror not_transp_msg
+let err_not_transp () =
+ CErrors.user_err ~hdr:"Program" not_transp_msg
module ProgMap = Id.Map
@@ -1445,7 +1469,7 @@ let declare_definition prg =
let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in
(* XXX: This is doing normalization twice *)
let kn =
- declare_definition ~name ~scope ~kind ~impargs ?hook ~obls
+ declare_definition_core ~name ~scope ~kind ~impargs ?hook ~obls
~fix_exn ~opaque ~poly ~udecl ~types ~body sigma
in
let pm = progmap_remove !State.prg_ref prg in
@@ -1531,7 +1555,7 @@ let declare_mutual_definition l =
(* Declare the recursive definitions *)
let udecl = UState.default_univ_decl in
let kns =
- declare_mutually_recursive ~scope ~opaque ~kind ~udecl ~ntns
+ declare_mutually_recursive_core ~scope ~opaque ~kind ~udecl ~ntns
~uctx:first.prg_ctx ~rec_declaration ~possible_indexes ~poly
~restrict_ucontext:false fixitems
in
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 647896e2f5..5339f4702b 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -144,17 +144,10 @@ val declare_variable
for removal from the public API, use higher-level declare APIs
instead *)
val definition_entry
- : ?fix_exn:Future.fix_exn
- -> ?opaque:bool
+ : ?opaque:bool
-> ?inline:bool
- -> ?feedback_id:Stateid.t
- -> ?section_vars:Id.Set.t
-> ?types:types
-> ?univs:Entries.universes_entry
- -> ?eff:Evd.side_effects
- -> ?univsbody:Univ.ContextSet.t
- (** Universe-constraints attached to the body-only, used in
- vio-delayed opaque constants and private poly universes *)
-> constr
-> Evd.side_effects proof_entry
@@ -295,7 +288,6 @@ val declare_entry
-> scope:locality
-> kind:Decls.logical_kind
-> ?hook:Hook.t
- -> ?obls:(Id.t * Constr.t) list
-> impargs:Impargs.manual_implicits
-> uctx:UState.t
-> Evd.side_effects proof_entry
@@ -315,7 +307,6 @@ val declare_definition
-> impargs:Impargs.manual_implicits
-> udecl:UState.universe_decl
-> ?hook:Hook.t
- -> ?obls:(Id.t * Constr.t) list
-> poly:bool
-> ?inline:bool
-> types:EConstr.t option
@@ -359,9 +350,6 @@ val declare_mutually_recursive
-> ntns:Vernacexpr.decl_notation list
-> rec_declaration:Constr.rec_declaration
-> possible_indexes:lemma_possible_guards option
- -> ?restrict_ucontext:bool
- (** XXX: restrict_ucontext should be always true, this seems like a
- bug in obligations, so this parameter should go away *)
-> Recthm.t list
-> Names.GlobRef.t list
diff --git a/vernac/mltop.ml b/vernac/mltop.ml
index d276a1ac35..c33b3d29f8 100644
--- a/vernac/mltop.ml
+++ b/vernac/mltop.ml
@@ -309,6 +309,9 @@ type ml_module_object = {
}
let add_module_digest m =
+ if not has_dynlink then
+ m, NoDigest
+ else
try
let file = file_of_name m in
let path, file = System.where_in_path ~warn:false !coq_mlpath_copy file in
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 102a17b216..c21951373b 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -132,5 +132,4 @@ val show_obligations : ?msg:bool -> Names.Id.t option -> unit
val show_term : Names.Id.t option -> Pp.t
val admit_obligations : Names.Id.t option -> unit
-val explain_no_obligations : Names.Id.t option -> Pp.t
val check_program_libraries : unit -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 20:27:38 +0000