| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Previously, they were using a map that was different from the one used
by the real lookup, leading to confusing information (number of
instances could be wrong, etc).
|
|
Ack-by: Zimmi48
Reviewed-by: herbelin
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
|
* filter_app (moved from MSets/MSetRBT.v)
* filter_map
* filter_ext_in
* ext_in_filter
* filter_ext_in_iff
* filter_ext
* concat_filter_map
* combine_nil
* combine_firstn_l
* combine_firstn_r
* combine_firstn
* nodup_fixed_point
|
|
Ack-by: Zimmi48
Reviewed-by: vbgl
Reviewed-by: SkySkimmer
|
|
Reviewed-by: gares
|
|
Reviewed-by: maximedenes
|
|
Reviewed-by: maximedenes
|
|
Reviewed-by: ppedrot
|
|
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: herbelin
Ack-by: mattam82
Reviewed-by: ppedrot
|
|
This is step 1 on removing library state from the lower layers.
Here we move library loading to the vernacular layer; few things
depend on it:
- printers: we add a parameter for those needing to access on-disk data,
- coqlib: indeed a few tactics do try to check that a particular
library is loaded; this is a tricky part. I've replaced that for a
module name check, but indeed this is fully equivalent due to
side-effects of `Require`. We may want to think what to do here.
A few other minor code movements were needed, but there are
self-explanatory.
|
|
|
|
Reviewed-by: ppedrot
|
|
Matthieu Sozeau explained how to fix this.
|
|
|
|
Reviewed-by: ejgallego
Reviewed-by: maximedenes
|
|
It will take a bit more to clean up the mess with entries in the
`indfun` plugin [quite a few PRs in the queue], but thanks to recent
refactoring the tricky parts are self-contained now in `gen_principle`
so we can remove the duplicated `save` function from the public API.
|
|
proof data on top of declare.
Reviewed-by: ppedrot
|
|
exception names
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: herbelin
Reviewed-by: ppedrot
|
|
flags.
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: herbelin
|
|
makefile fixes
Reviewed-by: ejgallego
Reviewed-by: vbgl
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
|
|
Non-delayed entries can be done with the current constructor, delayed
ones will require more work.
|
|
Reviewed-by: ppedrot
|
|
top of declare.
This PR is a follow up to #10406 , moving the then introduced
`proof_entry` type to `Declare`.
This makes sense as `Declare` is the main consumer of the entry type,
and already provides the constructors for it.
This is a step towards making the entry type private, which will allow
us to enforce / handle invariants on entry data better.
A side-effect of this PR is that now `Proof_global` does depend on
`Declare`, not the other way around, but that makes sense given that
closing an interactive proof will be a client of declare.
Indeed, all `Declare` / `Pfedit` / and `Proof_global` are tied into
tactics due to `abstract`, at some point we may be able to unify all
them into a single file in `vernac`.
|
|
We replace some uses of `raise (UserError ...)` with
`CErrors.user_err`, ideally we would like to make the error raising
API not depend on the exception themselves, but that's still a long
way to go.
We also rename the `Timeout` exception as to clarify purpose in the
codebase, given that it has 3 different ones as of today.
cc: #7560
|
|
Reviewed-by: ppedrot
|
|
And add links to UI in the browser.
|
|
|
|
Fix changelog entry
Fix build of the user manual
Markup fixes from Théo Zimmermann
Update doc and changelog and improve error messages.
|
|
This could be Prop (for compat with usual Coq), Set (for HoTT),
or actually an arbitrary "i".
Take lower bound of universes into account in pretyping/engine
Reinstate proper elaboration of SProp <= l constraints:
replacing is_small with equality with lbound is _not_ semantics preserving!
lbound = Set
Elaborate template polymorphic inductives with lower bound Prop
This will make more constraints explicit
Check univ constraints with Prop as lower bound for template inductives
Restrict template polymorphic universes to those not bounded from below
Fixes #9294
fix suggested by Matthieu
Try second fix suggested by Matthieu
Take care of modifying elaboration for record declarations as well.
Rebase and export functions for debug
Remove exported functions used while debugging
Add a new typing flag "check_template" and option "-no-template-checl"
This parameterizes the new criterion on template polymorphic inductives
to allow bypassing it (necessary for backward compatibility).
Update checker to the new typing flags structure
Switch on the new template_check flag to allow old unsafe behavior in
indTyping.
This is the only change of code really impacting the kernel, together
with the commit implementing unbounded from below and parameterization
by the lower bound on universes.
Add deprecated option `Unset Template Check` allowing to make proof
scripts work with both 8.9 and 8.10 for a while
Fix `Template Check` option name and test it
Add `Unset Template Check` to Coq89.v
Cooking of inductives and template-check tests
Cleanup test-suite file for template check / universes(template) flags
cookind tests
Move test of `Unset Template Check` to the failure/ dir, but comment it
for now
Template test-suite test explanation
Overlays for PR 9918
Overlay for paramcoq
Add overlay for fiat_parsers (-no-template-check)
Add overlay for fiat_crypto_legacy
Update fiat-crypto legacy overlay
Now it points at the version that I plan on merging; I am hoping that doing this will guard against mistakes by adding an extra check that the target tested by Coq's CI on this branch works with the change I made.
Remove overlay that should no longer be necessary
The setting in the compat file should handle it
Remove now-merged fiat-crypto-legacy overlay
Update `Print Assumptions` to reflect the typing flag for template checking
Fix About and Print Assumptions for template poly, giving info on which
variables are actually polymorphic
Fix pretty printing to print global universe levels properly
Fix printing of template polymorphic universes
Fix pretty printing for template polymorphism on no universe
Fix interaction of template check and universes(template) flag
Fix indTyping to really check if there is any point in polymorphism: the
conclusion sort should be parameterized over at least one local universe
Indtyping fixes for template polymorphic Props
Allow explicit template polymorphism again
Adapt to new indTyping interface
Handle the case of template-polymorphic on no universes
correctly (morally Type0m univ represented as Prop).
Fix check of meaningfullness of template polymorphism in the kernel.
It is now done w.r.t the min_univ, the minimal universe inferred for the
inductive/record type, independently of the user-written annotation
which must only be larger than min_univ. This preserves compatibility
with UniMath and template-polymorphism as it has been implemented up-to
now.
Comment on identity non-template-polymorphism
Remove incorrect universes(template) attributes from ssr
simpl_fun can be meaningfully template-poly, as well as
pred_key (although the use is debatable: it could just
as well be in Prop).
Move `fun_of_simpl` coercion declaration out of section to respect
uniform inheritance
Remove incorrect uses of #[universes(template)] from the stdlib
Extraction of micromega changes due to moving an ind decl out of a section
Remove incorrect uses of #[universes(template)] from plugins
Fix test-suite files, removing incorrect #[universes(template)] attributes
Remove incorrect #[universes(template)] attributes in test-suite
Fix test-suite
Remove overlays as they have been merged upstream.
|
|
|
|
check_constant_declaration
Reviewed-by: ppedrot
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Fixes #10640
We remove the `StdOut` dump target, so now dump will only happen if a
file is specified. Indeed, we make the default no to dump, and enable
dump only in coqc, moving the option to the `Coqcargs` module.
No need for a changes entry as this feature was undocumented, and no
use case was given when introduced.
Output to feedback must be explicitly enabled by clients / coqidetop,
and we have thus also removed the undocumented option `-feedback-glob`.
|
|
|
|
|
|
|
|
sig_not_dec
Reviewed-by: herbelin
|
|
|
|
- remove the architecture component (we don't do anything
arch-specific so it was just a rewording of int_size)
- have configure tell the make build system about int_size instead of
reimplementing cp
As a bonus, add the copyright header to uint63.mli.
|
|
Reviewed-by: Zimmi48
|
|
This improves error reporting. Addendum to #10515
|
|
Instead of doing (simplified code)
~~~ocaml
let check env kn cb =
let flags = env.flags in
let env' = set_flags env cb.flags in
...
let env = add_constant cb kn (if poly then env else env') in
set_flags env flags
~~~
(NB: when not poly env' has only the typing flags different from env)
we do
~~~ocaml
let check env kn cb =
let env = set_flags env cb.flags in
...
()
let check env kn cb =
let () = check env kn cb in
add_constant cb kn env
~~~
|
|
Reviewed-by: SkySkimmer
|
