| Commit message (Collapse) | Author | Age |
|---|
| |\
| |
| |
| | |
#3125)
|
| | |
| |
| |
| |
| |
| |
| | |
In particular singleton inductive types are considered injectable,
even in the absence of the option "Set Keep Proof Equalities".
This fixes #3125 (and #4560, #6273).
|
| | |
| |
| |
| |
| |
| | |
This reduces conversions between ContextSet/UContext and encodes
whether we are polymorphic by which constructor we use rather than
using some boolean.
|
| | |
| |
| |
| |
| |
| |
| |
| | |
Also use constant_universes_entry instead of a bool flag to indicate
polymorphism in ParameterEntry.
There are a few places where we convert back to ContextSet because
check_univ_decl returns a UContext, this could be improved.
|
| | |
| |
| |
| |
| |
| | |
We can enforce properties through check_univ_decl, or get an arbitrary
ordered context with UState.context / Evd.to_universe_context (the
later being a new wrapper of the former).
|
| |/ |
|
| |\
| |
| |
| | |
constructs.
|
| | |
| |
| |
| | |
Was actually forgotten in native-coq.
|
| | |
| |
| |
| |
| |
| | |
Extending terms is notoriously difficult. We try to get more help from
the compiler by making sure such an extension will trigger non
exhaustive pattern matching warnings.
|
| |/
|
|
|
|
|
| |
We mirror the structure of EConstr and move the destructors from `Term`
to `Constr`.
This is a step towards having a single module for `Constr`.
|
| |
|
|
|
|
|
|
|
|
|
| |
We'd like to handle proofs functionally we thus recommend not to use
printing functions without an explicit context.
We also adapt most of the code, making more explicit where the
printing environment is coming from.
An open task is to refactor some code so we gradually make the
`Pfedit.get_current_context ()` disappear.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
I followed what seems to be the intention of the code, with the
original intention of remove the global imperative proof state.
However, I fully fail to see why the new API is better than the old
one. In fact the opposite seems the contrary.
Still big parts of the "new proof engine" seem unfinished, and I'm
afraid I am not the right person to know what direction things should
take.
|
| | |
|
| | |
|
| |
|
|
| |
We do up to `Term` which is the main bulk of the changes.
|
| |
|
|
| |
This will allow to merge back `Names` with `API.Names`
|
| |
|
|
| |
This is a first step towards some of the solutions proposed in #6008.
|
| |
|
| |
fix spelling mistake. reword message to be in the Present Perfect tense instead of the 3rd person present because action is completed with respect to the theorem not some unknown third person.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
ML level can set the flags themselves.
In particular, using injection and discriminate with option "Keep
Proofs Equalities" when called from "decide equality" and "Scheme
Equality".
This fixes bug #5281.
|
| | | |
|
| |/
|
|
|
| |
To this extent we factor out the relevant bits to a new file,
ltac_pretype.
|
| |
|
|
|
| |
Compared to the original proposition (01f848d in #960), this commit
only changes files containing bug numbers that are also PR numbers.
|
| |\ |
|
| |\ \ |
|
| | | | |
|
| | | | |
|
| | |/
|/|
| |
| |
| | |
The old algorithm was relying on list membership, which is O(n). This was
nefarious for terms with many binders. We use instead sets in O(log n).
|
| |\ \ |
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | | |
It was introduced in 8.5 for compatibility with a 8.4 bug.
|
| |/ / /
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
As was questioned on Stack Overflow and discussed on Gitter, reduction
of the conclusion of the goal was done up to n+1 times for a failing
call to "constructor" on an inductive type of n constructors. We do it
at most once.
Reworking the layout of the code at the same time.
|
| | |/
|/|
| |
| | |
The bug was introduced in 1559f73.
|
| |\ \ |
|
| | |/
|/|
| |
| |
| | |
We dont care about the order of the binder map ([map] in the code) so
no need to do tricky things with it.
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
Inductive-keyworded record failing even on non-dependent goal)
|
| | |_|_|/
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This changes the implementation of "constructor" from
constructor 1 + ... + constructor n + fail
to
constructor 1 + ... + constructor n.
|
| | |_|/
|/| | |
|
| | |/
|/|
| |
| |
| | |
When we used to parse to a glob_sort but always give an empty list in
the GType case we can now parse directly to Sorts.family.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The internal detype function takes an additional arguments dictating
whether it should be eager or lazy.
We introduce a new type of delayed `DAst.t` AST nodes and use it for
`glob_constr`.
Such type, instead of only containing a value, it can contain a lazy
computation too. We use a GADT to discriminate between both uses
statically, so that no delayed terms ever happen to be
marshalled (which would raise anomalies).
We also fix a regression in the test-suite:
Mixing laziness and effects is a well-known hell. Here, an exception
that was raised for mere control purpose was delayed and raised at a
later time as an anomaly. We make the offending function eager.
|
| | |
| |
| |
| |
| |
| | |
The fix covers the case of a non-dependent goal with unavailable
dependent case analysis: destruct was not seeing that it could still
use non-dependent case analysis.
|
| | |
| |
| |
| |
| | |
The code generating the projection was unconditionally generating
pattern-matchings, although this is incorrect for primitive records.
|
| |\ \ |
|
| |\ \ \
| |_|/
|/| | |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| | | | | | | |
|
Maxime Dénès
Hugo Herbelin
Gaëtan Gilbert
Emilio Jesus Gallego Arias
Farzon Lotfi
Théo Zimmermann
Pierre-Marie Pédrot
Guillaume Melquiond
Paul Steckler
amblaf