| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| |\
| |
| |
| | |
into v8.5
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| | |
Passing `-compat 8.4` now allows the use of `econstructor (tac)`, as in
8.4.
|
| | |
| |
| |
| |
| | |
I introduced this bug in 4c078b0362542908eb2fe1d63f0d867b339953fd;
Coq.Init.Notations.constructor does not take any arguments.
|
| | |
| |
| |
| | |
We no longer need to redefine `refine` (it now shelves by default). Also clean up `constructor` a bit.
|
| | | |
|
| | |
| |
| |
| | |
The user-provided sort was ignored for them.
|
| | | |
|
| | |
| |
| |
| | |
variables and definitions in sections is unsupported.
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
enough
In particular, its interface might still change (in interaction with interested
colleagues). So let's not give it too much visibility yet. Instead, I'll turn
it as an opam packages for now.
|
| | | |
|
| |/ |
|
| |
|
|
|
|
| |
The option is still there, but not documented since it is too
dangerous. Hints and type classes instances are not taking cleared
variables into account.
|
| |
|
|
|
|
| |
The unshelve tactical can be used to get the shelved holes. This changes the
proper ordering of holes though, so expect some broken scripts. Also, the
test-suite is not fixed yet.
|
| | |
|
| |
|
|
| |
Marking it as experimental.
|
| | |
|
| |
|
|
|
|
|
|
|
| |
Prop levels.
As they are typed assuming all variables are >= Set now, and this was
breaking an invariant in typing. Only one instance in the standard
library was used in Hurkens, which can be avoided easily. This also
avoids displaying unnecessary >= Set constraints everywhere.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
Now doing
```coq
Tactic Notation "left" "~" := left.
Tactic Notation "left" "*" := left.
```
will no longer break the `left` tactic in Coq 8.4.
List obtained via
```
grep -o '^ \[[^]]*\]' tactics/coretactics.ml4 | sed s'/^ \[ \(.*\) \]/Tactic Notation \1 := \1./g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\) \(constr\|bindings\|constr_with_bindings\|quantified_hypothesis\|ne_hyp_list\)(\([^)]*\))/\1 \3/g'
```
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
This option disallows "declare at first use" semantics for universe
variables (in @{}), forcing the declaration of _all_ universes appearing
in a definition when introducing it with syntax Definition/Inductive
foo@{i j k} .. The bound universes at the end of a definition/inductive
must be exactly those ones, no extras allowed currently.
Test-suite files using the old semantics just disable the option.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
out to me by Pierre B.
Also extending use of bullets in Vectors where relevant.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Sorry so much.
Reverted:
707bfd5719b76d131152a258d49740165fbafe03.
164637cc3a4e8895ed4ec420e300bd692d3e7812.
b9c96c601a8366b75ee8b76d3184ee57379e2620.
21e41af41b52914469885f40155702f325d5c786.
7532f3243ba585f21a8f594d3dc788e38dfa2cb8.
27fb880ab6924ec20ce44aeaeb8d89592c1b91cd.
fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c.
d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962.
6737055d165c91904fc04534bee6b9c05c0235b1.
342fed039e53f00ff8758513149f8d41fa3a2e99.
21525bae8801d98ff2f1b52217d7603505ada2d2.
b78d86d50727af61e0c4417cf2ef12cbfc73239d.
979de570714d340aaab7a6e99e08d46aa616e7da.
f556da10a117396c2c796f6915321b67849f65cd.
d8226295e6237a43de33475f798c3c8ac6ac4866.
fdab811e58094accc02875c1f83e6476f4598d26.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
List.nth_error and List.hd_error were the only remaining places in
the whole stdlib to use type "Exc" instead of "option" directly.
So let's simplify things and use option everywhere. In particular,
during teaching sessions about lists, we won't have anymore to explain
the (lack of) difference between Exc,value,error and option,Some,None.
This might cause a few incompatibilities in proof scripts, if they
syntactically expect "value" or "error" to occur, but this should
hopefully be very rare and quite easy to fix.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
equalities in configurations like
x=y
x=z
===
P(x,y,z)
where it now produces
===
P(z,z,z)
In particular (equations are processed from most ancient to most recent).
Thanks to this, a "repeat subst" can just be a "subst" in List.v.
Incidentally: moved a nf_enter to enter in subst_one, since the latter
is normally called from other tactics having normalized evars.
|
| |
|
|
| |
Since [map_ext_in] is more general, no need to have the same proof twice.
|
| |
|
|
|
|
| |
Slightly broader version of the existing [map_ext]: two [map] expressions
are equal if their respective functions agree on all arguments that are
in the list being mapped.
|
| |
|
|
| |
spurious quantification on unused universes.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
Most of them are backports of improvements already there in
FSetPositive when compared with the original FMapPositive file.
|
| |
|
|
| |
replacement for 8.4's "Require Omega").
|
| |
|
|
| |
Closes #57.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- no more inconsistent Axiom in the Prelude
- STM can now process Admitted proofs asynchronously
- the quick chain can stock "Admitted" jobs in .vio files
- the vio2vo step checks the jobs but does not stock the result
in the opaque tables (they have no slot)
- Admitted emits a warning if the proof is complete
- Admitted uses the (partial) proof term to infer section variables
used (if not given with Proof using), like for Qed
- test-suite: extra line Require TestSuite.admit to each file making
use of admit
- test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to
find TestSuite.admit
|
Pierre Letouzey
Pierre-Marie Pédrot
Hugo Herbelin
Jason Gross
Jason Gross
Matthieu Sozeau
Matthieu Sozeau
Maxime Dénès
Enrico Tassi
Guillaume Melquiond
Cyprien Mangin
Nickolai Zeldovich
Matěj Grabovský