index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
...
*
|
- Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ...
Matthieu Sozeau
2014-05-08
*
|
Avoid allocations in type_of_inductive
Matthieu Sozeau
2014-05-08
*
|
Fast-path equality of sorts in compare_constr*
Matthieu Sozeau
2014-05-08
*
|
Adapt the checker to polymorphic universes and projections (untested).
Matthieu Sozeau
2014-05-08
*
|
Moving Dnet-related code to tactics/.
Pierre-Marie Pédrot
2014-05-08
*
|
Fixing test-suite for bug #3043.
Pierre-Marie Pédrot
2014-05-08
*
|
Fixing output test-suite: since universe polymorphism, the Print command
Pierre-Marie Pédrot
2014-05-08
*
|
Code cleaning in Tacinterp: factorizing some uses of tclEVARS.
Pierre-Marie Pédrot
2014-05-08
*
|
Removing comment outdated since eta holds in conversion rule (this
Hugo Herbelin
2014-05-07
*
|
Adding test-suite for bug #3242.
Pierre-Marie Pédrot
2014-05-06
|
*
Add regression tests for univ. poly. and prim proj
Jason Gross
2014-05-06
|
/
*
Remove Lemmas from base_include, it's not linked in dev/printers anymore
Matthieu Sozeau
2014-05-06
*
Cleanup before merge with the trunk
Matthieu Sozeau
2014-05-06
*
Use new tactic combinators in tclABSTRACT, to avoid blowup when using V82.tac...
Matthieu Sozeau
2014-05-06
*
Add missing case for primitive projection in fold_map.
Matthieu Sozeau
2014-05-06
*
Fix after merge.
Matthieu Sozeau
2014-05-06
*
Add incompatibilities paragraph in doc about universe polymorphism.
Matthieu Sozeau
2014-05-06
*
- Fix treatment of global universe constraints which should be passed along
Matthieu Sozeau
2014-05-06
*
Fix extraction taking a type in the wrong environment.
Matthieu Sozeau
2014-05-06
*
Fix Field_tac to get fast reification again, with the fix on template univers...
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
*
Print universes in module printing
Matthieu Sozeau
2014-05-06
*
Fix funind w.r.t. universes
Matthieu Sozeau
2014-05-06
*
Fix a pervasive equality use.
Matthieu Sozeau
2014-05-06
*
Avoid u+k <= v constraints, don't take the sup of an algebraic universe during
Matthieu Sozeau
2014-05-06
*
- Add back some compatibility functions to avoid rewriting plugins.
Matthieu Sozeau
2014-05-06
*
Add doc on the new API for universe polymorphism and primitive projections
Matthieu Sozeau
2014-05-06
*
Fix derive plugin to properly treat universes
Matthieu Sozeau
2014-05-06
*
Keep track of universes on coercion applications even if they're not polymorp...
Matthieu Sozeau
2014-05-06
*
Comment in Funind.v test-suite file
Matthieu Sozeau
2014-05-06
*
Proper calculation of constructor levels, forgetting the level of lets.
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
*
Retype application of fix_proto to get the right universes in Program
Matthieu Sozeau
2014-05-06
*
- Fix arity handling in retyping (de Bruijn bug!)
Matthieu Sozeau
2014-05-06
*
Fix restrict_universe_context removing some universes that do appear in the t...
Matthieu Sozeau
2014-05-06
*
Fix declarations of monomorphic assumptions
Matthieu Sozeau
2014-05-06
*
Allow records whose sort is defined by a constant.
Matthieu Sozeau
2014-05-06
*
- Fix RecTutorial, and mutual induction schemes getting the wrong names.
Matthieu Sozeau
2014-05-06
*
Fix program Fixpoint not taking care of universes.
Matthieu Sozeau
2014-05-06
*
- Fixes for canonical structure resolution (check that the initial term indee...
Matthieu Sozeau
2014-05-06
*
Fix restrict_universe_context to not remove useful constraints.
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
*
Fixes after rebase. The use of pf_constr_of_global is problematic in presence...
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
*
Fix issue #88: restrict_universe_context was wrongly forgetting about constra...
Matthieu Sozeau
2014-05-06
[prev]
[next]