| Age | Commit message (Collapse) | Author |
|---|
|
Currently, `.v` under the `Coq.` prefix are found in both `theories`
and `plugins`. Usually these two directories are merged by special
loadpath code that allows double-binding of the prefix.
This adds some complexity to the build and loadpath system; and in
particular, it prevents from handling the `Coq.*` prefix in the
simple, `-R theories Coq` standard way.
We thus move all `.v` files to theories, leaving `plugins` as an
OCaml-only directory, and modify accordingly the loadpath / build
infrastructure.
Note that in general `plugins/foo/Foo.v` was not self-contained, in
the sense that it depended on files in `theories` and files in
`theories` depended on it; moreover, Coq saw all these files as
belonging to the same namespace so it didn't really care where they
lived.
This could also imply a performance gain as we now effectively
traverse less directories when locating a library.
See also discussion in #10003
|
|
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.
|
|
|
|
To prevent confusion, forbidding a mix of the "injection term as pat1
... patn" and of the "injection term as [= pat1 ... patn]" syntax: If
a "[= ...]" occurs, this should be a singleton list of patterns.
|
|
(warn if bar is a nonprimitive projection)
|
|
|
|
|
|
The manual has long stated that these forms are deprecated. We add a
warning for them, as indeed `Add Morphism` is an "proof evil" [*]
command, and we may want to remove it in the future.
We've also fixed the stdlib not to emit the warning.
[*] https://ncatlab.org/nlab/show/principle+of+equivalence
|
|
|
|
There were three versions of injection:
1. "injection term" without "as" clause:
was leaving hypotheses on the goal in reverse order
2. "injection term as ipat", first version:
was introduction hypotheses using ipat in reverse order without
checking that the number of ipat was the size of the injection
(activated with "Unset Injection L2R Pattern Order")
3. "injection term as ipat", second version:
was introduction hypotheses using ipat in left-to-right order
checking that the number of ipat was the size of the injection
and clearing the injecting term by default if an hypothesis
(activated with "Set Injection L2R Pattern Order", default one from 8.5)
There is now:
4. "injection term" without "as" clause, new version:
introducing the components of the injection in the context in
left-to-right order using default intro-patterns "?"
and clearing the injecting term by default if an hypothesis
(activated with "Set Structural Injection")
The new versions 3. and 4. are the "expected" ones in the sense that
they have the following good properties:
- introduction in the context is in the natural left-to-right order
- "injection" behaves the same with and without "as", always
introducing the hypotheses in the goal what corresponds to the
natural expectation as the changes I made in the proof scripts for
adaptation confirm
- clear the "injection" hypothesis when an hypothesis which is the
natural expectation as the changes I made in the proof scripts for
adaptation confirm
The compatibility can be preserved by "Unset Structural Injection" or
by calling "simple injection".
The flag is currently off.
|
|
|
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15545 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
rewrite_db fails if nothing has been rewritten, and it only performs
*one* top-down pass. For the moment, use (repeat rewrite_db) for
emulating more closely autorewrite.
Btw, let's make Himsg.explain_ltac_call_trace robust wrt TacExtend
with fun(ny) parts
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15522 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15521 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- For instance, refl_equal --> eq_refl
- Npos, Zpos, Zneg now admit more uniform qualified aliases
N.pos, Z.pos, Z.neg.
- A new module BinInt.Pos2Z with results about injections from
positive to Z
- A result about Z.pow pushed in the generic layer
- Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l}
- Using tactic Z.le_elim instead of Zle_lt_or_eq
- Some cleanup in ring, field, micromega
(use of "Equivalence", "Proper" ...)
- Some adaptions in QArith (for instance changed Qpower.Qpower_decomp)
- In ZMake and ZMake, functor parameters are now named NN and ZZ
instead of N and Z for avoiding confusions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
BinPos now contain a sub-module Pos, in which are placed functions
like add (ex-Pplus), mul (ex-Pmult), ... and properties like
add_comm, add_assoc, ...
In addition to the name changes, the organisation is changed quite
a lot, to try to take advantage more of the orders < and <= instead
of speaking only of the comparison function.
The main source of incompatibilities in scripts concerns this compare:
Pos.compare is now a binary operation, expressed in terms of the
ex-Pcompare which is ternary (expecting an initial comparision as 3rd arg),
this ternary version being called now Pos.compare_cont. As for everything
else, compatibility notations (only parsing) are provided. But notations
"_ ?= _" on positive will have to be edited, since they now point to
Pos.compare.
We also make the sub-module Pos to be directly an OrderedType,
and include results about min and max.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14098 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13568 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
user contribs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
|
