| Age | Commit message (Collapse) | Author |
|---|
|
polymorphic (fixes bug #3043).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
- 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.
|
|
|
|
|
|
Now the universe inconsistency appears at [exact t] instead of the Defined :)
|
|
|
|
indeed unifies
with the projected term, keeping track of universes).
- Fix the [unify] tactic to fail properly.
- Fix unification to disallow lowering a global Type(i) universe to Prop or Set.
|
|
|
|
- Fix passing of universe contexts through definitions/proofs, abstract is ok now, even
in presence of polymorphism
- Correctly mark unresolvable the evars made by the Simple abstraction.
|
|
|
|
presence of side-effects...
|
|
- 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.
|
|
|
|
universes (better semantics
for axioms, opaque constants).
Conflicts:
pretyping/evarconv.ml
|
|
|
|
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
|
|
|
|
- Fix hasheq which didn't have a case for Proj making hashconsing exponentially slower.
Conflicts:
kernel/constr.ml
kernel/univ.ml
proofs/proof_global.ml
|
|
|
|
|
|
- Fix substitution of universes!
- Properly refresh universes in typeclasses exact hints.
Conflicts:
kernel/term_typing.ml
toplevel/obligations.ml
|
|
- Fix declaration of projections to work again with Primitive Projections on.
Conflicts:
kernel/term_typing.ml
|
|
|
|
avoiding doing work twice, better leq not duplicating a Universe.equal
test.
Conflicts:
kernel/univ.ml
|
|
Conflicts:
kernel/univ.ml
|
|
- Shortcut for Set <= x checks, assuming that this is always true except when
x (or rather its canonical representative) is Prop. Invariant to check.
- Uncomment the profiling code and make it depend on a (statically known) boolean.
|
|
Huge slowdown to be tracked in some files, even if no polymorphism is
involved.
Conflicts:
kernel/univ.ml
|
|
|
|
|
|
using a fast_compare_neq.
|
|
A try at hashconsing all universes instances seems to incur a big cost.
- Do hashconsing of universe instances in constr.
- Little fix in obligations w.r.t. non-polymorphic constants.
Conflicts:
kernel/constr.ml
kernel/declareops.ml
kernel/inductive.ml
kernel/univ.mli
|
|
|
|
md5sum check remains not portable.
|
|
|
|
going through a Coq extraction phase.
We use second order quantification through OCaml records, which allows for
a very precise use of low-level application. This results in quite a remarkable
speedup but there is still room for improvement.
This code was written by translating straightforwardly the Coq generated code
in a human-readable dialect.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17068 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
algorithms.
|
|
TODO fix interface on knowing_parameters to avoid useless array allocations.
|
|
stdlib does not compile entirely).
|
|
latent universes. Now the universes in the type of a definition/lemma
are eagerly added to the environment so that later proofs can be checked
independently of the original (delegated) proof body.
- Fixed firstorder, ring to work correctly with universe polymorphism.
- Changed constr_of_global to raise an anomaly if side effects would be lost by
turning a polymorphic constant into a constr.
- Fix a non-termination issue in solve_evar_evar.
-
|
