coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Restore reasonable performance by not allocating during universe checks,	Matthieu Sozeau	2014-05-06
*	- Rename eq to equal in Univ, document new modules, set interfaces.	Matthieu Sozeau	2014-05-06
*	Fix interface for template polymorphism, cleaning up code in all typing algor...	Matthieu Sozeau	2014-05-06
*	Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.	Matthieu Sozeau	2014-05-06
*	Initial work on reintroducing old-style polymorphism for compatibility (the s...	Matthieu Sozeau	2014-05-06
*	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Fixing #3293 (eta-expansion at "match" printing time was failing	Hugo Herbelin	2014-04-28
*	Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to	Hugo Herbelin	2014-04-28
*	Fix a second, trickier, typo in Termops.eta_reduce_head.	Arnaud Spiwack	2014-04-25
*	Fix a small typo in Termops.eta_reduce_head.	Arnaud Spiwack	2014-04-25
*	Better representation of evar filters: we represent the vacuous filters of	Pierre-Marie Pédrot	2014-04-23
*	Removing dead code, thanks to new OCaml warnings and a bit of scripting.	Pierre-Marie Pédrot	2014-04-23
*	Readback for int31 values from native compiler.	Maxime Dénès	2014-04-09
*	Fixing bug #3228 (fixing precedence of ltac variables over variables in env).	Hugo Herbelin	2014-04-05
*	Fixing #3262 which revealed a non-progressing, hence looping,	Hugo Herbelin	2014-04-04
*	Propagating conversion_problem towards (postponed) evar/evar problems.	Hugo Herbelin	2014-04-01
*	Fixing bug #2900 (evar/evar unif was supposed to be treated in	Hugo Herbelin	2014-04-01
*	Evarconv: exact_ise_stack looks to stack head before bodies or branches	Pierre Boutillier	2014-03-17
*	consider_remaining_unif_problems respects Conv_oracle	Pierre Boutillier	2014-03-16
*	Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it had	Pierre-Marie Pédrot	2014-03-14
*	Evarconv unification respects Conv_oracle	Pierre Boutillier	2014-03-10