| Age | Commit message (Collapse) | Author |
|---|
|
Following Bruno's suggestion, we check if the tree expected for the recursive
argument is included in the one which is inferred. This check is probably
not necessary in the current state of affairs, but might become so after
further extensions of the guard condition.
|
|
extensions.
|
|
|
|
|
|
|
|
instantiated in the return predicate are now taken into account. The resulting
recargs tree is the intersection between the one of the branches and the
appearing in the return predicate. Both the domain and co-domain are filtered.
|
|
Some fixpoints are now rejected in the standard library, but that's probably
because we compare trees for equality instead of intersecting them.
|
|
pattern matching.
This patch should be improved in two ways:
(1) Implement the same checks for the commutative cut subterm rule.
(2) When checking safe recursive subterms for each of the branches in a match,
instanciated parameters in the return predicate should be taken into account.
Step (1) should be enough to restore a correct guard condition, but (2) will
be required if we don't want to rule out some legitimate and practical examples.
|
|
|
|
and disable hashconsing of substituted instances which had a huge performance
penalty in general. They are hashconsed when put in the environment only now.
|
|
|
|
unification, speeding it up considerably
Revert backwards-incompatible commit 77df7b1283940d979d3e14893d151bc544f41410
|
|
more than one constructor.
|
|
a primitive projection impossible.
|
|
|
|
|
|
MathClasses).
|
|
kernel in library/universes.ml.
|
|
generated by a mutual inductive definition (bug found in CFGV). Actually this
code can move out of the kernel.
|
|
cleanly when called
on partially applied constructors. Also protect evar_conv from that case.
|
|
|
|
a global reference that the current (goal) env contains all the
section variables that the global reference expects to be present.
Note that the test for inclusion might be costly: everytime a
conversion happens in a section variable copied in a goal, this
conversion has to be redone when referring to a constant dependent on
this section variable.
It is unclear to me whether we should not instead give global names to
section variables so that they exist even if they are not listed in
the context of the current goal.
Here are two examples which are still problematic:
Section A.
Let B := True : Type.
Definition C := eq_refl : B = True.
Theorem D : Type.
clearbody B.
set (x := C).
unfold C in x.
(* inconsistent context *)
or
Section A.
Let B : Type.
exact True.
Qed.
Definition C := eq_refl : B = True. (* Note that this violated the Qed. *)
Theorem D : Type.
set (x := C).
unfold C in x.
(* inconsistent context *)
|
|
lib/interface split into:
- lib/feedback
subscribe-based feedback bus (also used by coqidetop)
- ide/interface
definition of coqide protocol messages
lib/pp
structured info/err/warn messages
lib/serialize split into:
- lib/serialize
generic xml serialization (list, pairs, int, loc, ...)
used by coqide but potentially useful to other interfaces
- ide/xmlprotocol
serialization of protocol messages as in ide/interface
the only drawback is that coqidetop needs -thread
and I had to pass that option to all files in ide/
|
|
univ_depends.
Also add a missing constraint when generating a fresh universe for a template polymorphic
inductive in that case.
|
|
Every time you use abstract a kitten dies, please stop.
|
|
|
|
Fixes bug #3346.
|
|
|
|
|
|
|
|
- Fix HoTT coq bug #80, implicit arguments with primitive projections were
wrongly automatically infered.
|
|
|
|
a projection constant only of the form
λ params (r : I params), match r with BuildR args => args_i end, without any
other user input and relies on it being typable (no more primitive projections
escaping this).
|
|
Ocaml does not remove the .cmi file if compilation fails, thus causing
subsequent native compilations to fail due to mismatching interfaces.
For the sake of homogeneity, also remove the .cmo/.cmxs file along the way.
|
|
|
|
|
|
conclusion, and results of
unifying the lemma with subterms. Using Retyping.get_type_of instead results in 3x
speedup in Ncring_polynom.
|
|
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.
|
|
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.
|
|
- 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.
|
|
|
|
|
|
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.
|
|
|
