| Age | Commit message (Collapse) | Author |
|---|
|
Local Ltac definitions do not register their name in the nametab anymore,
thus elegantly solving the bug. The tactic body remains accessible from
the tactic engine, but the name is rendered meaningless to the userside.
|
|
|
|
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.
|
|
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.
|
|
|
|
|
|
|
|
|
|
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.
|
|
- Distinguish between primitive and non-primitive records in the kernel
declaration, so as to try eta-conversion on primitive records only.
|
|
|
|
and disable hashconsing of substituted instances which had a huge performance
penalty in general. They are hashconsed when put in the environment only now.
|
|
any prefix of the given qualid.
|
|
The new Term version has essentially the same behaviour as the old "Locate",
while the new raw searches for all types of objects. Also code merging with
the "Locate Ltac".
Fixes bug #3380.
|
|
command.
|
|
LoadedFile is generated when a .vo is loaded
Goals is generated when -feedback-goals
|
|
kernel in library/universes.ml.
|
|
|
|
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/
|
|
polymorphic variables of the section as they might incur universe constraints that
were used to typecheck the body of the definition, even if the variable
itself was not used. For "Monomorphic" variables, their constraints are already
always pushed to the global context. This fixes bug # 3330.
|
|
universe instance.
|
|
and avoiding explicit substitutions and merging of contexts, e.g. in obligations.ml.
The context produced by typechecking a statement is passed in the proof, allowing the
universe name context to be correctly folded as well. Mainly an API cleanup.
|
|
|
|
- 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).
|
|
Fixes bug #3333.
|
|
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.
|
|
|
|
- More cleanup. remove unneeded functions in universes
|
|
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.
|
|
|
|
- Add a tentative syntax for specifying universes: Type{"i"} and foo@{Type{"i"},Type{"j"}}.
These are always rigid.
- Use level-to-level substitutions where the more general level-to-universe substitutions
were previously used.
|
|
The call to the native compiler can fail due to the sheer amounts of -I
options passed to it. Indeed, it is easy to get the command line to exceed
512KB, thus causing various operating systems to reject it. This commit
avoids the issue by only passing the -I options that matter for the
currently compiled code.
Note that, in the worst case, this commit is still not sufficient on
Windows (32KB max), but this worst case should be rather uncommon and thus
can be ignored for now.
For the record, the command-line size mandated by Posix is 4KB.
|
|
|
|
|
|
instead of lists to test if a library has already been encountered.
|
|
Fix restriction of universe contexts to not forget about potentially useful
constraints.
|
|
minimization.
|
|
- Fix in canonical structure inferce, we have to check that the heads
are convertible and keep universe information around.
|
|
- Enforce that no u <= Prop/Set can be added for u introduced by the user in Evd.process_constraints.
(Needs to be enforced in the kernel as well, but that's the main entry point).
- Fix a test-suite script and remove a regression comment, it's just as before now.
|
|
term.
|
|
|
|
- Remove Universe Polymorphism flags everywhere.
- Properly infer, discharge template arities and fix substitution inside them
(kernel code to check for correctness).
- Fix tactics that were supposing universe polymorphic constants/inductives to
be parametric on that status. Required to make interp_constr* return the whole evar
universe context now.
- Fix the univ/level/instance hashconsing to respect the fact that marshalling doesn't preserve sharing,
sadly losing most of its benefits.
Short-term solution is to add hashes to these for faster comparison, longer term requires rewriting
all serialization code.
Conflicts:
kernel/univ.ml
tactics/tactics.ml
theories/Logic/EqdepFacts.v
|
|
|
|
constraints,
and keeping spurious equalities. simplify_universe_context is correct, although
it might keep unused universes around (it's the responsibility of the tactics to
not produce unused universes then).
Add printer for future universe contexts for debugging.
|
|
A quick and dirty approach to private inductive types
Types for which computable functions are provided, but pattern-matching is disallowed.
This kind of type can be used to simulate simple forms of higher inductive types, with
convertibility for applications of the inductive principle to 0-constructors
Conflicts:
intf/vernacexpr.mli
kernel/declarations.ml
kernel/declarations.mli
kernel/entries.mli
kernel/indtypes.ml
library/declare.ml
parsing/g_vernac.ml4
plugins/funind/glob_term_to_relation.ml
pretyping/indrec.ml
pretyping/tacred.mli
printing/ppvernac.ml
toplevel/vernacentries.ml
Conflicts:
kernel/declarations.mli
kernel/declareops.ml
kernel/indtypes.ml
kernel/modops.ml
|
|
|
|
- Avoid generation of dummy universes for unsafe_global*
- Handle side effects better for polymorphic definitions.
Conflicts:
kernel/term_typing.ml
tactics/tactics.ml
|
|
|
