| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | | | |
|
| | | |/
| |/| |
|
| | | | |
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| |\| | |
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
In particular, a proof of the equivalence of excluded-middle and an
unrestricted principle of minimization.
Credits to Arnaud Spiwack for the ideas and formalizations of the proofs.
|
| | | | |
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | | |
| | |
| | |
| | | |
introduction pattern by default.
|
| | | | |
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This reverts 18796b6aea453bdeef1ad12ce80eeb220bf01e67 (Slight change
in the semantics of arguments scopes: scopes can no longer be bound to
Funclass or Sortclass (this does not seem to be useful)). It is
useful to have function_scope for, e.g., function composition. This
allows users to, e.g., automatically interpret ∘ as morphism
composition when expecting a morphism of categories, as functor
composition when expecting a functor, and as function composition when
expecting a function.
Additionally, it is nicer to have fewer special cases in the OCaml
code, and give more things a uniform syntax. (The scope type_scope
should not be special-cased; this change is coming up next.)
Also explicitly define [function_scope] in theories/Init/Notations.v.
This closes bug #3080, Build a [function_scope] like [type_scope], or allow
[Bind Scope ... with Sortclass] and [Bind Scope ... with Funclass]
We now mention Funclass and Sortclass in the documentation of [Bind Scope]
again.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Sorry so much.
Reverted:
707bfd5719b76d131152a258d49740165fbafe03.
164637cc3a4e8895ed4ec420e300bd692d3e7812.
b9c96c601a8366b75ee8b76d3184ee57379e2620.
21e41af41b52914469885f40155702f325d5c786.
7532f3243ba585f21a8f594d3dc788e38dfa2cb8.
27fb880ab6924ec20ce44aeaeb8d89592c1b91cd.
fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c.
d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962.
6737055d165c91904fc04534bee6b9c05c0235b1.
342fed039e53f00ff8758513149f8d41fa3a2e99.
21525bae8801d98ff2f1b52217d7603505ada2d2.
b78d86d50727af61e0c4417cf2ef12cbfc73239d.
979de570714d340aaab7a6e99e08d46aa616e7da.
f556da10a117396c2c796f6915321b67849f65cd.
d8226295e6237a43de33475f798c3c8ac6ac4866.
fdab811e58094accc02875c1f83e6476f4598d26.
|
| | | |
|
| | | |
|
| |\| |
|
| | | |
|
| |\|
| |
| |
| |
| |
| |
| | |
Conflicts:
tactics/eauto.ml4
(merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | | |
|
| | |
| |
| |
| | |
(see #3695).
|
| |\| |
|
Matthieu Sozeau
Jason Gross
Pierre-Marie Pédrot
Enrico Tassi
Maxime Dénès
Hugo Herbelin
Guillaume Melquiond
Jason Gross
Matthieu Sozeau
Pierre Boutillier
Cyprien Mangin
Pierre Letouzey