| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
| |
These options no longer have any impact on the way proofs are loaded. In
other words, loading is always lazy, whatever the options. Keeping them
just so that coqc dies when the user prints some opaque symbol does not
seem worth it.
|
| |
|
|
|
|
|
| |
restriction, after last fix commit which precisely possibly restricts
evars of a term "t" in "apply t in H" without resolving them.
|
|
|
|
| |
name of replaced hypothesis.
|
|
|
|
| |
in case prefix 'e' of "apply" and co is not given.
|
|
|
|
| |
in unification.ml in case prefix 'e' of "apply" and co is not given.
|
| |
|
|
|
|
| |
primitive projections obey the Arguments command.
|
| |
|
| |
|
| |
|
| |
|
| |
|
|\ |
|
| |
| |
| |
| |
| | |
- Monomorphize Cst_stack to 'a = constr.
- Add corresponding debug printer.
|
| |
| |
| |
| |
| |
| |
| | |
conclusion, and results of
unifying the lemma with subterms. Using Retyping.get_type_of instead results in 3x
speedup in Ncring_polynom.
|
| |
| |
| |
| |
| | |
The right fix should probably be to remove the build_constant_by_tactic
function and only use the build_by_tactic one
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
I'd add more, but I'm tired and it's late and I should sleep. Maybe
I'll pick up at 3279 (working down) another day.
Bug 3344 is broken; [Fail Defined.] says that [Defined] has not failed,
even though it raises an anomaly. So there's no way I can think of to
test it. I've left it in the [opened] directory anyway.
|
| | |
|
|/ |
|
|
|
|
| |
redundant in canonical arcs.
|
|
|
|
| |
by the printing options (i.e. when "Print Universes" is set).
|
|
|
|
| |
by the printer anyway.
|
|
|
|
| |
to recover the trace of a universe inconsistency. Changed its name too btw.
|
| |
|
|
|
|
| |
were never used and were responsible for code duplication.
|
|
|
|
|
|
| |
a O(1) check, contrasting with the previous O(n) behaviour that rendered
universe constraint checking prohibitive on big files. I expect a 20% speedup
on such files.
|
|
|
|
|
| |
I also took the opportunity to remove a lot of code not used by
the checker.
|
|
|
|
| |
- More cleanup. remove unneeded functions in universes
|
| |
|
|
|
|
|
|
| |
handling from
the instance/contexts and substitution code.
|
| |
|
|
|
|
|
|
|
|
| |
Universes.
Needed to exponse compare_head_gen(_leq) so that it could be reused in Universes.
Remove unused functions from univ as well and refactor a little bit.
Changed the syntax to Type@{} for explicit universe level specs, following the WG decision.
|
| |
|
|\
| |
| |
| | |
into trunk
|
| | |
|
| |
| |
| |
| |
| |
| | |
I've marked new failing commands that I'm confused about with "???"; I'm
not sure whether or not they should fail there, but we should keep the
test-suite compiling, probably.
|
|/
|
|
| |
reduction.
|
|
|
|
| |
the checker, and it was not used before that anyway.
|
| |
|
| |
|
|
|
|
|
|
|
| |
This should finally get rid of the following class of bugs:
Qed fails, STM undoes to the beginning of the proof because the
exception is not annotated with the correct state, PG gets out of
sync because errors always refer to the last command in PGIP.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
declare takes care of ignoring side effects that are available in the
global environment. This is yet another instance of what the "abominion"
(aka abstract) can do: the code was checking for the existence in the
environment of the elimination principle, and not regenerating it (nor
declaring the corresponding side effect) if the elimination principle
is used twice.
Of course to functionalize the imperative actions on the environment
when two proofs generated by abstract use the same elim principle,
such elim principle has to be inlined twice, once in each abstracted
proof. In other words, a side effect generated by a tactic inside
an abstract is *global* but will be made local, si it must always
be declared, no matter what.
Now the system works like this:
- side effects are always declared, even if a caching mechanism thinks
the constant is already there (it can be there, no need to regenerate it
but the intent to generate it *must* be declared anyhow)
- at Qed time, we filter the list of side effects and decide which ones are
really needed to be inlined.
bottom line: STOP using abstract.
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
| |
as "forall x:nat*nat, x=x", which resulted in
"forall n n0 : nat, (n, n0) = (n, n0)" before commit
37f68259ab0a33c3b5b41de70b08422d9bcd3bec on "Fixing introduction
patterns * and ** ".
|
| |
|