| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: ppedrot
|
|
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.
|
|
and cofix
Reviewed-by: SkySkimmer
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
|
|
Reviewed-by: ejgallego
|
|
|
|
- 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.
|
|
Reviewed-by: herbelin
Reviewed-by: jfehrle
Ack-by: maximedenes
|
|
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: SkySkimmer
|
|
|
|
|
|
Commit auto-generated by running dev/tools/update-compat.py --release.
As per release doc this must be run at some point before branching
(not necessarily close to the branching date).
|
|
Reviewed-by: herbelin
Ack-by: jfehrle
|
|
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: ppedrot
|
|
|
|
notations (+ a fix about locations)
Reviewed-by: ppedrot
|
|
- Add a `--fuzz` option to `make-both-single-timing-files.py`
Passing `--fuzz=N` allows differences in character locations of up to
`N` characters when matching lines in per-line timing diffs.
The corresponding variable for `coq_makefile` is `TIMING_FUZZ=N`.
See also the discussion at
https://github.com/coq/coq/pull/11076#pullrequestreview-324791139
- Allow passing `--real` to per-file timing scripts and `--user` to
per-line timing script.
This allows easily comparing real times instead of user ones (or vice
versa).
- Support `TIMING_SORT_BY` and `TIMING_FUZZ` in Coq's own build
- We also now use argparse rather than a hand-rolled argument parser;
there were getting to be too many combinations of options.
- Fix the ordering of columns in Coq's build system; this is the
equivalent of #8167 for Coq's build system.
Fixes #11301
Supersedes / closes #11022
Supersedes / closes #11230
|
|
+ tests in the test-suite for non max local implicit arguments
|
|
|
|
termination checker.
Reviewed-by: SkySkimmer
|
|
There was an evar leak due to an evarmap not being threaded correctly
when computing open terms.
|
|
Reviewed-by: fajb
|
|
|
|
Fixes #5617.
|
|
- The cutting plane has been (sometimes) improved to generate stronger
cuts.
- There is now some support for profiling the Simplex
see documentation for Show Lia Profile.
|
|
This is probably a bit overkill but users are tempted to experiment
it, so we accept that both ends of a recursive notation are surrounded
with boxes which contain printing hints.
The alternative would have been to forbid the ends of a recursive
notation to be in boxes, but strictly speaking it is a bit more
restricting, even if I don't see a realistic use of the general form.
|
|
This shows a few bugs and even anomalies. See issue #11091.
See further commits for some fixes.
|
|
Reviewed-by: ppedrot
|
|
notations in R)
Reviewed-by: erikmd
Reviewed-by: ppedrot
|
|
Related: https://github.com/coq/coq/pull/8630
|
|
'e' was not displayed when printing decimal notations in R :
Require Import Reals.
Check (1.23e1, 32e+1, 0.1)%R.
was giving
< (123-1%R, 321%R, 1-1%R)
instead of
< (123e-1%R, 32e1%R, 1e-1%R)
This was introduced in #8764 (in Coq 8.10).
|
|
And enable related test.
|
|
so for instance
~~~coq
Set Printing All. Set Printing Universes.
Polymorphic Inductive foo@{u v|u<=v} : Type@{u}:= .
Lemma bla@{u v|u < v} : foo@{u v} -> False.
Proof. induction 1. Qed.
~~~
works.
|
|
|
|
Ack-by: Zimmi48
Reviewed-by: herbelin
Ack-by: maximedenes
|
|
Ack-by: maximedenes
Reviewed-by: ppedrot
|
|
Reviewed-by: maximedenes
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
|
|
decorations
Ack-by: Zimmi48
Reviewed-by: herbelin
|
|
|
|
OCaml's string type
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: herbelin
Ack-by: maximedenes
Reviewed-by: pi8027
|
|
type of h.
Reviewed-by: ppedrot
|
|
(and not just…
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
The type of h is reconstructed to look as much as the initial type of
h as possible.
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: ppedrot
|
