| Commit message (Expand) | Author | Age |
* | Proper handling of the polymorphism flag for Context, fixing HoTT bug #98. | Matthieu Sozeau | 2014-06-23 |
* | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau | 2014-06-18 |
* | Fix bug #3289 | Matthieu Sozeau | 2014-06-11 |
* | - Fix substitution of universes which needlessly hashconsed existing universes. | Matthieu Sozeau | 2014-06-10 |
* | Moving hook code from Future to Lemmas. This seemed to disrupt compilation of | Pierre-Marie Pédrot | 2014-06-08 |
* | Enforce a correct exception handling in declaration_hooks | Enrico Tassi | 2014-06-08 |
* | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau | 2014-05-06 |
* | Fix context forgetting universes (temporary, the fix is not exactly right). | Matthieu Sozeau | 2014-05-06 |
* | Various fixes of universe polymorphism and projections when they're set. | 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 |
* | Allowing the "Declare Instance" command anywhere. This was artificially | Pierre-Marie Pédrot | 2014-05-01 |
* | Remove some dead-code (thanks to ocaml warnings) | Pierre Letouzey | 2014-03-05 |
* | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey | 2014-03-05 |
* | Qed: feedback when type checking is done | Enrico Tassi | 2013-12-24 |
* | Adding generic solvers to term holes. For now, no resolution mechanism nor | Pierre-Marie Pédrot | 2013-11-27 |
* | The tactic [admit] exits with the "unsafe" status. | aspiwack | 2013-11-02 |
* | Makes the new Proofview.tactic the basic type of Ltac. | aspiwack | 2013-11-02 |
* | Removing Evd.undefined_evars. | ppedrot | 2013-10-28 |
* | declaration_hooks use Ephemeron | gareuselesinge | 2013-10-18 |
* | get rid of closures in global/proof state | gareuselesinge | 2013-08-08 |
* | State Transaction Machine | gareuselesinge | 2013-08-08 |
* | Granting bug #3098: adding priority to Existing Instances. | ppedrot | 2013-08-01 |
* | Use the Hook module here and there. | ppedrot | 2013-05-12 |
* | A uniformization step around understand_* and interp_* functions. | herbelin | 2013-05-09 |
* | Declaration of multiple hypotheses or parameters now share typing | herbelin | 2013-05-08 |
* | Splitting Term into five unrelated interfaces: | ppedrot | 2013-04-29 |
* | Modules and ppvernac, sequel of Enrico's commit 16261 | letouzey | 2013-03-13 |
* | Restrict (try...with...) to avoid catching critical exn (part 13) | letouzey | 2013-03-13 |
* | invalid_arg instead of raise (Invalid_argement ...) | letouzey | 2013-03-12 |
* | Added a Local Definition vernacular command. This type of definition | ppedrot | 2013-03-11 |
* | New implementation of the conversion test, using normalization by evaluation to | mdenes | 2013-01-22 |
* | Modulification of name | ppedrot | 2012-12-18 |
* | Modulification of Label | ppedrot | 2012-12-18 |
* | Modulification of identifier | ppedrot | 2012-12-14 |
* | Finish patch for Hint Resolve, stopping to generate new constant names for | msozeau | 2012-12-08 |
* | Monomorphization (toplevel) | ppedrot | 2012-11-26 |
* | Change Hint Resolve, Immediate to take a global reference as argument | msozeau | 2012-10-26 |
* | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey | 2012-10-02 |
* | This patch removes unused "open" (automatically generated from | regisgia | 2012-09-14 |
* | Assumption commands are now displayed as unsafe in Coqide. | aspiwack | 2012-08-24 |
* | Updating headers. | herbelin | 2012-08-08 |
* | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot | 2012-06-22 |
* | Fix bug #2808: wrong handling of evars in Instance command. | msozeau | 2012-06-21 |
* | Forward-port fixes from 8.4 (15358, 15353, 15333). | msozeau | 2012-06-04 |
* | Getting rid of Pp.msg | ppedrot | 2012-05-30 |
* | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey | 2012-05-29 |
* | New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr | letouzey | 2012-05-29 |
* | Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd | letouzey | 2012-05-29 |
* | Fix interface of resolve_typeclasses: onlyargs -> with_goals: | msozeau | 2012-03-20 |