| Age | Commit message (Collapse) | Author |
|---|
|
|
|
inductive types + deactivate test for equality of sort + deactivate
the check that the constraints Prop/Set <= Type are declared).
|
|
Stop sharing those references across constants of the same
module, which was triggering some bugs when using native_compute
in interactive mode in a functor declaration.
|
|
I'm afraid this fix is a bit heuristic, but it seems to generate correct code in
all cases.
|
|
|
|
|
|
Reestablish completeness in conversion when Opaque primitive
projections are used.
|
|
Was broken accidentally by 5b0769b33, slowing down vm_compute and native_compute
on numeric computations.
|
|
The induced side effects were incompatible with the undo machinery.
|
|
coqide to coqtop.
(Joint work with Pierre)
|
|
but the internal representation dropped let-in.
Ideally, the internal representation of the "match" should use
contexts for the predicate and the branches. This would however be a
rather significant change. In the meantime, just a hack.
To do, there is still an extra @ in the constructor name that does not
need to be there.
|
|
makes"
This makes CatsInZFC explode by expanding constants unnecessarily.
This reverts commit cf36105854c9a42960ee4139c6afdaa75ec8f31a.
|
|
This generalizes the BuildVi flag and lets one choose which
opaque proofs are done and which not.
|
|
Now the seff contains it directly, no need to force the future
or to hope that it is a Direct opaque proof.
|
|
Before this patch opaque tables were only growing, making them unusable
in interactive mode (leak on Undo).
With this patch the opaque tables are functional and part of the env.
I.e. a constant_body can point to the proof term in 2 ways:
1) directly (before the constant is discharged)
2) indirectly, via an int, that is mapped by the opaque table to
the proof term.
This is now consistent in batch/interactive mode
This is step 0 to make an interactive coqtop able to dump a .vo/.vi
|
|
for the record binder of classes. This name is no longer generated
in the kernel but part of the declaration. Also cleanup the interface
to recognize primitive records based on an option type instead of a
dynamic check of the length of an array.
|
|
Thanks to Yves for reporting it!
|
|
inductives).
The implementation constant should have the a universe instance
of the same length, we assume the universes are in the same order
and we check that the definition does not add any constraints
to the expected ones. This fixes bug #3670.
|
|
it closer to evarconv/unification's behavior and it is less prone
to weird failures and successes in case of first-order unification
sending problems where the two terms have different types.
|
|
using whd_state_gen to handle unfolding. Add an isProj/destProj
in term. Use the proper environment everywhere in unification.ml.
|
|
so as to reproduce correctly the reduction behavior of existing
projections, i.e. delta + iota. Make [projection] an abstract datatype
in Names.ml, most of the patch is about using that abstraction.
Fix unification.ml which tried canonical projections too early in
presence of primitive projections.
|
|
Essential for parallel processing of Coq documents.
It is a fairly straightforward change but a tad tedious, I may have introduced some bugs in the process.
|
|
|
|
|
|
Let r.(p) be a strict subterm of r during the guardness check.
|
|
|
|
subst_univs_levels.
|
|
it to the new representation of projections and the new mind_finite
type.
|
|
|
|
introducing constants (e.g. Top.1 is always before Top.2), compatible with the one
used before introduction of hMaps in LMap/LSet.
|
|
Involves changing the [mind_finite] field in the kernel from a bool to the trivalued type [Decl_kinds.recursivity_kind]. This is why so many files are (unfortunately) affected. It would not be very surprising if some bug was introduced.
|
|
This revert somehow f5d7b2b1eda550f5bf0965286d449112acbbadde about "Hypotheses
don't respect Barendregt convention".
|
|
now done entirely using declare_mind, which declares the associated
constants for primitive records. This avoids a hack related to
elimination schemes and ensures that the forward references to constants
in the mutual inductive entry are properly declared just after the
inductive. This also clarifies (and simplifies) the code of term_typing
for constants which does not have to deal with building
or checking projections anymore.
Also fix printing of universes showing the de Bruijn encoding in a few places.
|
|
eta-expanded version of a projection as before.
|
|
Now kernel/indtypes builds the corresponding terms (has to be trusted)
while translate_constant just binds a constant name to the
already entered projection body, avoiding the dubious "check"
of user given terms. "case" Pattern-matching on primitive records is
now disallowed, and the default scheme is implemented using
projections and eta (all elimination tactics now use projections
as well). Elaborate "let (x, y) := p in t" using let bindings
for the projections of p too.
|
|
It's possible that I should have removed more "allows", as many
instances of "foo allows to bar" could have been replaced by "foo bars"
(e.g., "[Qed] allows to check and save a complete proof term" could be
"[Qed] checks and saves a complete proof term"), but not always (e.g.,
"the optional argument allows to ignore universe polymorphism" should
not be "the optional argument ignores universe polymorphism" but "the
optional argument allows the caller to instruct Coq to ignore universe
polymorphism" or something similar).
|
|
larger than Type.1 etc...
|
|
|
|
|
|
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.
|
|
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.
|
|
|
|
In check_one_cofix, we now avoid calling dest_subterms each time we meet a
constructor by storing both the current tree (needed for the new criterion)
and a precomputed array of trees for subterms.
|
|
When dynamically computing the recarg tree, we now prune it according to the
inferred tree. Compilation of CompCert is now ok.
|
|
I had introduced it by mistake due to my OCaml dyslexia :)
Thanks to Enrico and Arnaud for saving my day!
|
|
|
|
for constants that are not unfolded during conversion.
Fix discharge of polymorphic section variables over inductive types.
|
|
- Decomment code in reductionops forgotten after debugging.
|
|
variables.
Simplifies instantiation of constants/inductives, requiring less allocation and Map.find's.
Abstraction by variables is handled mostly inside the kernel but could be moved outside.
|
