| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | | |
|
| |\|
| |
| |
| |
| |
| |
| | |
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).
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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
|
| | | |
|
| |\| |
|
| | | |
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
NB: this is work-in-progress, there is currently only one
provided implementation (MMapWeakList).
In the same spirit as MSets w.r.t FSets, the main difference between
MMaps and former FMaps is the use of a new version of OrderedType
(see Orders.v instead of obsolete OrderedType.v).
We also try to benefit more from recent notions such as Proper.
For most function specifications, the style has changed : we now use
equations over "find" instead of "MapsTo" predicates, whenever possible
(cf. Maps in Compcert for a source of inspiration). Former specs are
now derived in FMapFacts, so this is mostly a matter of taste.
Two changes inspired by the current Maps of OCaml:
- "elements" is now "bindings"
- "map2" is now "merge" (and its function argument also receives a key).
We now use a maximal implicit argument for "empty".
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
NB: this is work-in-progress, there is currently only one
provided implementation (MMapWeakList).
In the same spirit as MSets w.r.t FSets, the main difference between
MMaps and former FMaps is the use of a new version of OrderedType
(see Orders.v instead of obsolete OrderedType.v).
We also try to benefit more from recent notions such as Proper.
For most function specifications, the style has changed : we now use
equations over "find" instead of "MapsTo" predicates, whenever possible
(cf. Maps in Compcert for a source of inspiration). Former specs are
now derived in FMapFacts, so this is mostly a matter of taste.
Two changes inspired by the current Maps of OCaml:
- "elements" is now "bindings"
- "map2" is now "merge" (and its function argument also receives a key).
We now use a maximal implicit argument for "empty".
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
This reverts commit 4e6c9891140932f452bb5ac8960d597b0b5fde1d, which was
breaking compatibility because one could no longer use names of foralls in
the goal without introducting them. Probably not good style, but it did
break many existing developments including CompCert.
Closes #4093 but reopens #4035.
|
| | |
| |
| |
| |
| |
| |
| | |
Due to the way it was laid out, the tactic could prove neither
(Zle x x) nor (P /\ Q -> P) nor (P |- P /\ True)
yet it could prove
(Zle x x /\ True) and (P /\ Q |- P).
|
| |\| |
|
| | | |
|
| |\| |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| | |
generalizing * which was broken since 8.4.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
definitions. Instead of failing with an anomaly when trying to do
conversion or computation with the vm's, consider polymorphic constants
as being opaque and keep instances around. This way the code is still
correct but (obviously) incomplete for polymorphic definitions and we
avoid introducing an anomaly. The patch does nothing clever, it only
keeps around instances with constants/inductives and compile constant
bodies only for non-polymorphic definitions.
|
| | |
| |
| |
| | |
being transparent
|
| | |
| |
| |
| |
| |
| | |
Off by default as it can be backwards-incompatible (e.g. produces
loop in the library without an additional Typeclasses Opaque directive
in RelationPairs).
|
| | |
| |
| |
| |
| |
| | |
non-universe-polymorphic
ID, fixing the script results in 3 universes for the stdlib again.
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| | |
More results on set_remove, in particular explicit the NoDup
pre-condition. Show that NoDup is preserved by other operations.
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
definitions. Instead of failing with an anomaly when trying to do
conversion or computation with the vm's, consider polymorphic constants
as being opaque and keep instances around. This way the code is still
correct but (obviously) incomplete for polymorphic definitions and we
avoid introducing an anomaly. The patch does nothing clever, it only
keeps around instances with constants/inductives and compile constant
bodies only for non-polymorphic definitions.
|
| | |
| |
| |
| | |
being transparent
|
| |/
|
|
|
|
| |
Off by default as it can be backwards-incompatible (e.g. produces
loop in the library without an additional Typeclasses Opaque directive
in RelationPairs).
|
| | |
|
| |
|
|
|
| |
section variable.
For some reason, the subproofs solved by [auto] had started using [Hfinjective] from the section context.
|
Pierre Boutillier
Cyprien Mangin
Hugo Herbelin
Pierre Letouzey
Guillaume Melquiond
Pierre-Marie Pédrot
Nickolai Zeldovich
Matthieu Sozeau
Matěj Grabovský
Enrico Tassi
Maxime Dénès
Sébastien Hinderer
Arnaud Spiwack