| Commit message (Collapse) | Author | Age |
... | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
We'd like to cleanup the `proof_end` type so we can have a smaller
path in proof save. Note that the construction:
```
Goal Type.
⋮
Save id.
```
has to be handled by the STM in the same path as Defined (but with an
opaque flag), as `Save id` will alter the environment and cannot be
processed in parallel.
We thus try to simply such paths a bit, as complexity of `lemmas.ml`
seems like an issue these days. The form `Save Theorem id` doesn't
really seem used, and moreover we should really add a type of "Goal",
and unify syntax.
It is often the case that beginners try `Goal addnC n : n + 0 = n."
etc...
|
| |_|_|_|_|_|_|/ / / / / / /
|/| | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
It has been deprecated for a while in favor of `Qed`.
|
| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
We benefit from the fact that we normalize now *all* hypotheses
even the one defining the "stated" variable: it is produced as
...def of v... = v
and normalized as
-v + ...def of v... = 0
which is precisely what we should add to the initial equation during
a O_STATE.
|
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
Now that O_SUM is properly optimized (cf. the [fusion] function),
we could use it to encode CONTRADICTION and NEGATE_CONTRADICT(_INV).
This way, the trace has almost the same size, but ReflOmegaCore.v
is shorter and easier to maintain.
|
| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
In this variant, the proof term produced by romega isn't verified at
the tactic run-time (no vm_compute). In theory, [unsafe_romega] should
behave exactly as [romega], but faster. Now, if there's a bug in romega,
we'll be notified only at the following Qed. This could be interesting
for debugging purpose : you could inspect the produced buggish term
via a Show Proof.
|
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
This is a major change :
- Generated proofs are quite shorter, since only the resolution trace remains.
- No time penalty mesured (it even tends to be slightly faster this way).
- Less infrastructure in ReflOmegaCore and refl_omega.
- Warning: the normalization functions in ML and in Coq should be kept
in sync, as well as the variable order.
- Btw: get rid of ML constructor Oufo
|
| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
In a coming commit, we'll normalize terms by a Coq function
that will compare Tvar's instead of blindly applying a trace,
so let's speed-up these comparisons.
|
| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
For the bug, see new test test_romega10 in test-suite/success/ROmega0.v.
|
| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | |
|
| |_|_|_|_|_|_|_|_|_|_|_|/
|/| | | | | | | | | | | | |
|
| | | | | | | | | | | | | |
|
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
We do that by using constr_with_bindings rather than
open_constr_with_bindings (+ extra call to typeclasses in
"specialize"). If my understanding is right, the only effect would be
to succeed more in cases where it was failing (in
inh_conv_coerce_to_gen). In particular, "specialize" and
"contradiction" already have a WITHHOLES test for rejecting pending
holes.
Incidentally, this answers enhancement #5153.
|
| |_|_|_|_|_|_|_|_|/ / /
|/| | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
This fixes an inconsistency introduced in 554a6c806 (svn r12603) where
both interp_constr_with_bindings and interp_open_constr_with_bindings
were going through interp_open_constr (no type classes so as to not to
commit too early on irreversible choices, accepting unresolved holes).
We fix this by having interp_constr_with_bindings going to
interp_constr (using type classes and failing on unresolved evars).
The external impact is that any TACTIC EXTEND which refers to
constr_with_binding has now to decide whether it intends it to use
what the name suggest (using type classes and to fail if evars remain
unresolved), thus keeping constr_with_binding, or the actual behavior
which requires to use open_constr_with_bindings for strict
compatibility.
|
| |_|_|_|_|/ / / / / /
|/| | | | | | | | | | |
|
| | | | | | | | | | | |
|
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
Remove a space before colon.
Remove the use of term mandatory
(this closes https://coq.inria.fr/bugs/show_bug.cgi?id=3994).
|
| |_|/ / / / / / / /
|/| | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
Namely: Replacing (currently deactivated) warning on illegal ident by
an error in strict mode and nothing in soft mode.
|
|\ \ \ \ \ \ \ \ \ \ |
|
| | | | |/ / / / / /
| | | |/| | | | | |
| | | | | | | | | |
| | | | | | | | | | |
As prompted in https://coq.inria.fr/bugs/show_bug.cgi?id=2831
|
|\ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
masked).
|
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
- https://coq.inria.fr/bugs/show_bug.cgi?id=5529
- https://coq.inria.fr/bugs/show_bug.cgi?id=5537
See also PR #640
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|/ / / / / /
|/| | | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
all_stdlib.v.
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|_|_|_|_|/ / / / / /
|/| | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | |
This allows to use a cast in subst_of_rel_context_instance.
Also added more cast functions for further use.
|
| | | | | | | | | | | | | | | | | |
|
| |_|_|_|_|_|_|_|/ / / / / / / /
|/| | | | | | | | | | | | | | | |
|
| |/ / / / / / / / / / / / / /
|/| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | |
Was working when calling test-suite from main Makefile but not when
calling directly from the test-suite Makefile.
The dependency was mistakenly dropped in 98a927aef.
|