| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Reviewed-by: ejgallego
Reviewed-by: gares
|
|
beta versions.
Reviewed-by: ejgallego
|
|
missing them.
Reviewed-by: ejgallego
|
|
Ack-by: gares
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
Reviewed-by: SkySkimmer
Ack-by: maximedenes
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: herbelin
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
|
|
This was already possible manually using "{ _ }" in the type of
declaration. This was also possible for type classes. So, no reason to
forbid in Arguments.
|
|
|
|
Reviewed-by: ejgallego
|
|
No reason to have them in the same .sh
|
|
In previous refactorings `vernac_loop` stopped being tail-recursive,
we refactor code a bit and make it back into tail-recursive form.
|
|
We refactor control loop a bit to make the code more readable:
- the code for unhandled exception is not needed anymore as it cannot
happen.
- we move the processing of toplevel commands to its own function
- we split away diff-specific functions.
|
|
Reviewed-by: herbelin
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.
|
|
Reviewed-by: ppedrot
|
|
and cofix
Reviewed-by: SkySkimmer
|
|
|
|
Instead of various termops and globnames aliases.
|
|
The previous system was from before globref was in the kernel.
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
|
|
The interpreter directive of “doc/stdlib/make-library-index” must be patched.
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: ppedrot
Reviewed-by: vbgl
|
|
Motivations:
- We should have only maintained developments in our CI
- `make ci-fiat-crypto-legacy` takes about 15 mins before the first call
to `coqc`, making it unusable to work on overlays
- The coding style of this development is so fragile that adapting to
any change of behavior requires diffing gigabytes of Ltac traces.
@mattam82 and I have been blocked for 6 months this way, when working on
unifall.
I understand this development was meant to stress-test some components
like printing, but I think the trade-off is bad. We should rather come
up with specialized test suites for these components.
|
|
|
|
- Implicit arguments in the return clause and in the branches
of a match were not checked.
- Implicit arguments in each declaration of intern_context were not
restarted.
- Additionally, in intern_context, we take into account ids from the
env on top of which intern_context is called.
- A better approximation of the check for manual implicit in notations
improved (though not fully correct because the exact context of
interpretation of a binder in a notation with recursive binders is
not known).
We also rename impl_binder_index into binder_block_names in anticipation of
checking redundancies also for non-implicit arguments.
|
|
WithoutTypeConstraint says it can be a term. In particular, if it has
manual implicit arguments, these will be allowed only in leading
lambdas. I.e. it can start with "fun {x}" but not with "forall {x}".
New constructor UnknownIfTermOrType allows to be both a term or a
type. In particular, if it allowed start both with "fun {x}" and
"forall {x}".
|
|
|
|
|
|
Reviewed-by: herbelin
Reviewed-by: jfehrle
Ack-by: maximedenes
|
|
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
|
|
|
|
of made up constant
Reviewed-by: ppedrot
|
|
Reviewed-by: Matafou
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Treat a Set Default Proof Using call the same as having a syntactic
Proof using ... annotation. This ensures that proofs in sections are
skipped in -vos mode when there are enough annotations to determine the
type of the resulting theorem.
Fixes #11342.
|
|
Reviewed-by: SkySkimmer
|
|
|
|
Reviewed-by: JasonGross
Reviewed-by: ejgallego
|
|
Reviewed-by: ppedrot
|
