| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| |
|
|
| |
(revealed by contribution PTSF).
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
NoOccurenceFound when only typeclass resolution failed. Might break
some scripts relying on backtracking on typeclass resolution failures
to find other terms to rewrite, which can be fixed using occurrences
or directly setoid_rewrite.
|
| |
|
|
| |
instead of the normalized one at the end of the proof. Fixes bug #3517.
|
| | |
|
| | |
|
| |
|
|
| |
when conversion in the goal failed.
|
| |
|
|
|
|
| |
test-suite
file HoTT_coq_089.v).
|
| |
|
|
| |
projections.
|
| | |
|
| |
|
|
| |
for typeclass errors.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
output/Arguments.v
output/ArgumentsScope.v
output/Arguments_renaming.v
output/Cases.v
output/Implicit.v
output/PrintInfos.v
output/TranspModType.v
Main changes: monomorphic -> not universe polymorphic, Peano vs Nat
|
| | |
|
| |
|
|
|
| |
(AFAIU, it is the table of supported unicode characters which has to
be upgraded anyway.)
|
| |
|
|
| |
died" when coqtop or coqtopide.cmxs are in inconsistent state.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
The lexer parses bullets only at the beginning of sentence. In
particular, the lexer recognizes sentences (this feature was
introduced for the translator and it is still used for the
beautifier). It recognized "." but not "...'. I added "..." followed
by space or eol as a terminator of sentences. I hope this is
compatible with the rest of the code dealing with end of
sentences.
Fixed also parse_to_dot which was not aware of "...".
Maybe there are similar things to do with coqide or PG?
|
| |
|
|
| |
change of printing format of forall (need more thinking).
|
| |
|
|
|
| |
projections and their expansion, allowing unfolding when it fails.
Cleanup code in reductionops.ml
|
| |
|
|
| |
its expansion if it could reduce (fixes bug #3480).
|
| |
|
|
| |
applications, solving part of bug #3503.
|
| | |
|
| | |
|
| |
|
|
| |
of the argument is smaller than the other one.
|
| |
|
|
|
| |
Names and arguments were uniformized, and some functions were redesigned to
take their typical use-case into account.
|
| |
|
|
|
|
| |
The levels added by the context are in general much fewer than the size of the
evarmap, so it is better to add them to the latter rather than doing it the
other way around.
|
| |
|
|
|
|
|
| |
a primitive application only if all parameters of [p] are implicit, falling
back to the internalization of the eta-expanded version otherwise. This makes
apply [p] succeed even if its record argument is not implicit, ensuring better
compatibility.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
| |
Fixes PTSF (though I have no idea what caused this bug to show up just yesterday).
|
| |
|
| |
In theory [Proofview.Goal.env] should be, itself, marked as requiring a normalised goals (as it includes [hyps] which does). However, it is impractical as it is very common to pass a goal environment to a function reasoning modulo evars. So I guess we are bound to mark the appropriate functions by hand.
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
all the tactics using the constructor keyword in one entry. This has the
side-effect to also remove the other variant of constructor from the AST.
I also needed to hack around the "tauto" tactic to make it work, by
calling directly the ML tactic through a TacExtend node. This may be
generalized to get rid of the intermingled dependencies between this
tactic and the infamous Ltac quotation mechanism.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
My previous optimization of guard checking (f1280889) made it slightly stricter,
in the presence of dependent pattern matching and nested inductive types whose
toplevel types are mutually recursive.
The following (cooked-up) example illustrates this:
Inductive list (A B : Type) := nil : list A B | cons : A -> list A B -> list
A B.
Inductive tree := Node : list tree tree -> tree.
Lemma foo : tree = tree. exact eq_refl. Qed.
Fixpoint id (t : tree) :=
match t with
| Node l =>
let l := match foo in (_ = T) return list tree T with eq_refl => l end
in
match l with
| nil => Node (nil _ _)
| cons x tl => Node (cons _ _ (id x) tl)
end
end.
is accepted, but changing tree to:
Inductive tree := Node : list tree tree -> tree.
with tree2 := .
made id be rejected after the optimization.
The same problem occurred in Paco, and is now fixed.
Note that in the example above, list cannot be mutually recursive because of the
current strict positivity condition for tree.
|
| |
|
|
|
|
|
| |
to Ltac's value."
It was commit 52247f50fa9aed83cc4a9a714b6b8f779479fd9b.
The closure in uconstr renders these changes (pertaining to substitution of ltac variables during internalisation) obsolete.
|
| |
|
|
|
| |
This avoids relying on detyping. As Matthieu Sozeau pointed out to me, [understand∘detyping] has no reason to be the identity. This may create surprising behaviour some times (when a detyped term loses its relations to the current context, in particular in terms of universes), and downright incompatibilities in the case of refine.
As a bonus this should be a faster implementation of [uconstr] with a leaner memory profile.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
with possible further use of token "[]" + slight restructuration.
|
| | |
|
| | |
|
Pierre-Marie Pédrot
Hugo Herbelin
Matthieu Sozeau
Matthieu Sozeau
Arnaud Spiwack
Maxime Dénès