| Age | Commit message (Collapse) | Author |
|---|
|
cf "If this is implemented, long names might cause a printing
problem:" in #11852
|
|
|
|
- Provide new helper functions in `Goptions` on the model of
`declare_bool_option_and_ref`;
- Use these helper functions in many parts of the code base
(encapsulates the corresponding references);
- Move almost all options from `declare_string_option` to
`declare_stringopt_option` (only "Warnings" continue to use the
former). This means that these options now support `Unset` to get
back to the default setting. Note that there is a naming
misalignment since `declare_int_option` is similar to
`declare_stringopt_option` and supports `Unset`. When "Warning" is
eventually migrated to support `Unset` as well, we can remove
`declare_string_option` and rename `declare_stringopt_option` to
`declare_string_option`.
- For some vernac options and flags that have an equivalent
command-line option or flag, implement it like the standard `-set`
and `-unset`.
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
Ack-by: ppedrot
|
|
Latest refactorings allow us to make the signature Coq parser a
standard `Grammar.S` one; the only bit needed is to provide the extra
capabilities to the `Lexer` signature w.r.t. to comments state.
The handling of Lexer state is still a bit ad-hoc, in particular it is
global whereas it should be fully attached to the parsable. This may
work ok in batch mode but the current behavior may be buggy in the
interactive context.
This PR doesn't solve that but it is a step towards a more functional
solution.
|
|
Four types of numerals are introduced:
- positive natural numbers (may include "_", e.g. to separate thousands, and leading 0)
- integer numbers (may start with a minus sign)
- positive numbers with mantisse and signed exponent
- signed numbers with mantisse and signed exponent
In passing, we clarify that the lexer parses only positive numerals,
but the numeral interpreters may accept signed numerals.
Several improvements and fixes come from Pierre Roux. See
https://github.com/coq/coq/pull/11703 for details. Thanks to him.
|
|
Ack-by: herbelin
|
|
Add headers to a few files which were missing them.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Also renamed it to relative_entry_level.
Correspondence between old and new representation is:
(n,L) -> LevelLt n
(n,E), (n,Prec n) -> LevelLe n
(n,Any) -> LevelSome
(n,Prec p) when n<>p was unused
Should not change global semantics (except error message in pr_arg).
|
|
information may impact the display of coercion and implicit arguments.
Reviewed-by: ejgallego
|
|
We do two changes:
- We distinguish between a notion of format generically attached to
notations and a new notion of format attached to interpreted
notations. "Reserved Notation" attaches a format
generically. "Notation" attaches the format specifically to the given
interpretation, and additionally, attaches it generically if it is the
first time the notation is defined.
- We warn before overriding an explicitly reserved generic format, or
a specific format.
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
The standard use is to repeat the option keywords in lowercase, which
is basically useless.
En passant add doc entry for Dump Arith.
|
|
and cofix
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
|
|
Set Printing Width 20.
Check fix my_long_fix
(my_induction_variable y z t u v w x' y' z' t' u' v' w' : nat)
(a b c d e f a' b' c' d' e' f' : bool) :=
match my_induction_variable with
| 0 => 0
| S my_recursive_variable => my_recursive_variable
end.
gives:
fix my_long_fix
(my_induction_variable
y z t u v w x'
y' z' t' u' v'
w' : nat)
(a b c d e f a'
b' c' d' e'
f' : bool)
{struct
my_induction_variable} :
nat :=
match
my_induction_variable
with
| 0 => 0
| S
my_recursive_variable =>
my_recursive_variable
end
instead of:
fix
my_long_fix (my_induction_variable
y z t u
v w x'
y' z'
t' u'
v'
w' : nat)
(a b c
d e f
a' b'
c' d'
e'
f' : bool)
{struct
my_induction_variable} :
nat :=
match
my_induction_variable
with
| 0 => 0
| S
my_recursive_variable =>
my_recursive_variable
end
|
|
Set Implicit Arguments.
Set Contextual Implicit.
Inductive option A := None | Some (a:A).
Coercion some_nat := @Some nat.
Check fix f x := match x with 0 => None | n => some_nat n end.
gives:
fix f (x : nat) : option nat :=
match x with
| 0 => None (A:=nat)
| S _ => some_nat x
end
See discussion at
https://github.com/coq/coq/pull/11142/files/718c1422954794e0e33a87cf4c9111c00cc186dd#r377054717
|
|
|
|
|
|
Reviewed-by: ejgallego
Reviewed-by: herbelin
|
|
clauses in pattern matching decompilation algorithm
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
Namely, Evd.evar_env and Evd.evar_filtered_env now take an additional
environment instead of querying the imperative global one. We percolate
this change as higher up as possible.
|
|
This governs the printing of the explicitation of implicit arguments
and the removal of coercions.
E.g., "Check coe foo." where coe is a coercion with codomain B will show:
foo
: B
instead of
coe foo
: B
|
|
|
|
This allows to give access to all printing options (e.g. a scope or
being-in-context) to every printer w/o increasing the numbers of
functions.
|
|
|
|
We also remove trailing whitespace.
Script used:
```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
|
|
- only one space instead of two when printing "{| |}"
- removing a redundant clause in the grammar of record_patterns
|
|
|
|
Add experimental "Show Proof" command to the toplevel that shadows
the current command in the parser (in coqtop and PG only).
Apply existing code to highlight diffs in the output
|
|
There are no more users.
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: hendriktews
Reviewed-by: herbelin
Ack-by: mattam82
|
|
|
|
We move `Declaremods` to the vernac layer as it implement
vernac-specific logic to manipulate modules which moreover is highly
imperative.
This forces code [such as printing] to manipulate the _global
imperative_ state which is a bit fishy.
The key improvement in this PR is that now `Global` is not used
anymore in `library`, so we can proceed to move it upwards.
This move is a follow-up of #10562 and a step towards moving `Global`
upper, likely to `interp` in the short term.
|
|
`Import` does not actually need to register an object, only `Export`
does. So we specialize and rename the object into `ExportObject`.
|
|
Reviewed-by: maximedenes
|
|
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.
|
|
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.
|
|
Reviewed-by: SkySkimmer
|
|
We move `binder_kind` to the pretyping AST, removing the last data
type in the now orphaned file `Decl_kinds`.
This seems a better fit, as this data is not relevant to the lower
layers but only used in `Impargs`.
We also move state keeping to `Impargs`, so now implicit declaration
must include the type. We also remove a duplicated function.
|
