| Commit message (Expand) | Author | Age |
* | Remove some dead code and add test-suite file. | Matthieu Sozeau | 2015-02-16 |
* | Update headers. | Maxime Dénès | 2015-01-12 |
* | When pretyping [uconstr] closures, don't use the local Ltac variable environm... | Arnaud Spiwack | 2014-12-19 |
* | Getting rid of Exninfo hacks. | Pierre-Marie Pédrot | 2014-12-16 |
* | Tentatively more informative report of failure when inferring | Hugo Herbelin | 2014-12-11 |
* | uconstr: fix bug in interpretation of Ltac-bound name in let-tuple and patter... | Arnaud Spiwack | 2014-11-19 |
* | Fixing bug #3792. | Pierre-Marie Pédrot | 2014-11-09 |
* | Fixing confused code for interpretations of evar instances. | Hugo Herbelin | 2014-11-03 |
* | Fixing inefficiency in typeclass resolution. | Pierre-Marie Pédrot | 2014-11-03 |
* | This commit introduces changes in induction and destruct. | Hugo Herbelin | 2014-10-25 |
* | Build unfolded versions of the primitive projection in let (a, p) := ... | Matthieu Sozeau | 2014-10-07 |
* | Fixing interpretation of constr under binders which was broken after | Hugo Herbelin | 2014-10-02 |
* | Add syntax for naming new goals in refine: writing ?[id] instead of _ | Hugo Herbelin | 2014-09-30 |
* | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau | 2014-09-27 |
* | Fixes in Ltac pattern-matching on primitive projections | Matthieu Sozeau | 2014-09-19 |
* | Revert specific syntax for primitive projections, avoiding ugly | Matthieu Sozeau | 2014-09-17 |
* | Fix: when interpreting a identifier in pretying, use the Ltac identifier subs... | Arnaud Spiwack | 2014-09-15 |
* | Fix a bug in the naming of binders. | Arnaud Spiwack | 2014-09-15 |
* | Providing a -type-in-type option for collapsing the universe hierarchy. | Hugo Herbelin | 2014-09-13 |
* | Checking typability of evar instances. Using ";" to separate bindings | Hugo Herbelin | 2014-09-13 |
* | Uniformisation of the order of arguments env and sigma. | Hugo Herbelin | 2014-09-12 |
* | Parsing evar instances. | Hugo Herbelin | 2014-09-12 |
* | Referring to evars by names. Added a parser for evars (but parsing of | Hugo Herbelin | 2014-09-12 |
* | Parsing of Type@{max(i,j)}. | Matthieu Sozeau | 2014-09-08 |
* | The pretyping of [uconstr] in [refine] uses the identifier of the ltac contex... | Arnaud Spiwack | 2014-09-05 |
* | Adds an identifier context in pretying's Ltac context. | Arnaud Spiwack | 2014-09-05 |
* | Change the way primitive projections are declared to the kernel. | Matthieu Sozeau | 2014-08-28 |
* | Better structure for Ltac pretyping environments. | Pierre-Marie Pédrot | 2014-08-07 |
* | [uconstr]: use a closure instead of eager substitution. | Arnaud Spiwack | 2014-08-06 |
* | Move to a representation of universe polymorphic constants using indices for ... | Matthieu Sozeau | 2014-08-03 |
* | A tentative uniform naming policy in module Inductiveops. | Hugo Herbelin | 2014-08-01 |
* | Add toplevel commands to declare global universes and constraints. | Matthieu Sozeau | 2014-07-01 |
* | Quickly fixing bug #2996: typing functions now check when referring to | Hugo Herbelin | 2014-06-28 |
* | Change interface of refresh universes to get a pbty argument instead of | Matthieu Sozeau | 2014-06-26 |
* | Fix for bug 1951, allowing at least fully-applied inductives types to be used | Matthieu Sozeau | 2014-06-23 |
* | Fixed some HoTT bugs, provide a proper error message when giving an ill-formed | Matthieu Sozeau | 2014-06-20 |
* | Cleanup treatment of template universe polymorphism (thanks to E. Tassi | Matthieu Sozeau | 2014-06-20 |
* | Fixing #3282 (two bugs in the presence of let-in's in "fix"). | Hugo Herbelin | 2014-06-17 |
* | Removing dead code. | Pierre-Marie Pédrot | 2014-06-17 |
* | Fix type inference of the record argument of a projection to catch ill-typed | Matthieu Sozeau | 2014-06-17 |
* | In generalized rewrite, avoid retyping completely and constantly the conclusi... | Matthieu Sozeau | 2014-06-11 |
* | Collecting in Namegen those conventional default names that are used in diffe... | Hugo Herbelin | 2014-06-04 |
* | - Fix hashing of levels to get the "right" order in universe contexts etc... | Matthieu Sozeau | 2014-06-04 |
* | 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 |
* | - Fix bug preventing apply from unfolding Fixpoints. | 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 |
* | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |