index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
Commit message (
Expand
)
Author
Age
*
Compute the trace of a universe inconsistency only when explicitly required
Pierre-Marie Pédrot
2014-06-10
*
Made explanations for universe inconsistencies optional. They are only used
Pierre-Marie Pédrot
2014-06-10
*
- Fix substitution of universes which needlessly hashconsed existing universes.
Matthieu Sozeau
2014-06-10
*
Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...
Matthieu Sozeau
2014-06-10
*
Fix canonical structure resolution in unification (bug found in Ssreflect).
Matthieu Sozeau
2014-06-08
*
Make kernel reduction code parametric over the handling of universes,
Matthieu Sozeau
2014-06-06
*
Collecting in Namegen those conventional default names that are used in diffe...
Hugo Herbelin
2014-06-04
*
Fix canonical structure resolution (makes test-suite files go through again).
Matthieu Sozeau
2014-06-04
*
- Allow parsing of @const@{instance} for specifying universe instances of pol...
Matthieu Sozeau
2014-06-04
*
- Force every universe level to be >= Prop, so one cannot "go under" it anymore.
Matthieu Sozeau
2014-06-04
*
- Fix hashing of levels to get the "right" order in universe contexts etc...
Matthieu Sozeau
2014-06-04
*
- Keep all <= constraints during refinement, otherwise we might miss collapse...
Matthieu Sozeau
2014-06-04
*
cbn understand ! Arguments directive
Pierre Boutillier
2014-06-04
*
Use of "H"-based names for propositional hypotheses obtained by
Hugo Herbelin
2014-06-01
*
Dead code + typo.
Hugo Herbelin
2014-05-31
*
- Fix for commit 15999903f875f4b5dbb3d5240d2ca39acc3cd777 which disallowed some
Matthieu Sozeau
2014-05-28
*
Cbn reduces Pos.compare p~1 q~1 to Pos.compare p q
Pierre Boutillier
2014-05-26
*
Reduction.Stack.Fix/Case stores Cst_stack.t
Pierre Boutillier
2014-05-26
*
Cst_stack before stack (abstraction leak in whd_gen)
Pierre Boutillier
2014-05-26
*
cbn: args list instead of arg number
Pierre Boutillier
2014-05-26
*
Reductionops.Stack.map & Reduction.iterate_whd_gen
Pierre
2014-05-26
*
- Fix in kernel conversion not folding the universe constraints
Matthieu Sozeau
2014-05-26
*
More fixes of unification with primitive projections (missed cases during the...
Matthieu Sozeau
2014-05-16
*
Fix unification of non-unfoldable primitive projections in evarconv.
Matthieu Sozeau
2014-05-16
*
Refresh universes for Ltac's type_of, as the term can be used anywhere,
Matthieu Sozeau
2014-05-09
*
Fix second-order matching to properly check that the predicate found by
Matthieu Sozeau
2014-05-09
*
Reuse universe level substitutions for template polymorphism, fixing performance
Matthieu Sozeau
2014-05-09
*
Cleanup code in pretyping/evarutil
Matthieu Sozeau
2014-05-08
*
Fix performance problem with unification in presence of universes (bug #3302)...
Matthieu Sozeau
2014-05-08
*
- Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ...
Matthieu Sozeau
2014-05-08
*
Moving Dnet-related code to tactics/.
Pierre-Marie Pédrot
2014-05-08
*
- Fix treatment of global universe constraints which should be passed along
Matthieu Sozeau
2014-05-06
*
Find a more efficient fix for dealing with template universes:
Matthieu Sozeau
2014-05-06
*
Try a new way of handling template universe levels
Matthieu Sozeau
2014-05-06
*
- Add back some compatibility functions to avoid rewriting plugins.
Matthieu Sozeau
2014-05-06
*
Keep track of universes on coercion applications even if they're not polymorp...
Matthieu Sozeau
2014-05-06
*
Refresh some universes in cases.ml as they might appear in the term.
Matthieu Sozeau
2014-05-06
*
Correct universe handling in program coercions (bug #2378).
Matthieu Sozeau
2014-05-06
*
Fix set_leq_sort refusing max(u,Set) <= Set when u is flexible.
Matthieu Sozeau
2014-05-06
*
- Fix arity handling in retyping (de Bruijn bug!)
Matthieu Sozeau
2014-05-06
*
Allow records whose sort is defined by a constant.
Matthieu Sozeau
2014-05-06
*
- Fixes for canonical structure resolution (check that the initial term indee...
Matthieu Sozeau
2014-05-06
*
- Fix eq_constr_universes restricted to Sorts.equal
Matthieu Sozeau
2014-05-06
*
Remove postponed constraints (unused)
Matthieu Sozeau
2014-05-06
*
- Fix bug preventing apply from unfolding Fixpoints.
Matthieu Sozeau
2014-05-06
*
Adapt universe polymorphic branch to new handling of futures for delayed proofs.
Matthieu Sozeau
2014-05-06
*
Honor the Opaque flag for projections in simpl.
Matthieu Sozeau
2014-05-06
*
In case two constants/vars/rels are _not_ defined, force unification of unive...
Matthieu Sozeau
2014-05-06
*
Adapt Y. Bertot's path on private inductives (now the keyword is "Private").
Yves Bertot
2014-05-06
*
- Fix comparison of universes.
Matthieu Sozeau
2014-05-06
[next]