| Age | Commit message (Expand) | Author |
|---|
| 2014-10-10 | Add debug printers for projections, fix printing of evar constraints | Matthieu Sozeau |
| 2014-10-09 | Adding printer for named_context_val and Goal.goal in debugger. | Hugo Herbelin |
| 2014-10-07 | Adding a printer for hints. | Hugo Herbelin |
| 2014-10-02 | Fixing interpretation of constr under binders which was broken after | Hugo Herbelin |
| 2014-09-27 | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau |
| 2014-09-18 | Fix debug printing with primitive projections. | Matthieu Sozeau |
| 2014-09-12 | Referring to evars by names. Added a parser for evars (but parsing of | Hugo Herbelin |
| 2014-09-10 | VernacExtend does not dispatch on type anymore. | Pierre-Marie Pédrot |
| 2014-08-26 | Debug RAKAM | Pierre Boutillier |
| 2014-06-11 | - Fix bug #3368, due to wrong use of the Cst_stack for projections. | Matthieu Sozeau |
| 2014-06-10 | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau |
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau |
| 2014-05-06 | Fix issue #88: restrict_universe_context was wrongly forgetting about constra... | Matthieu Sozeau |
| 2014-05-06 | 'Pretty' printer for wf_paths | Pierre |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-04-25 | Adding a debug printer for futures. | Pierre-Marie Pédrot |
| 2014-04-23 | Better representation of evar filters: we represent the vacuous filters of | Pierre-Marie Pédrot |
| 2014-04-05 | Printers for ltac environments. | Hugo Herbelin |
| 2014-04-02 | A debug printer for Evd.Filter.t | Pierre Boutillier |
| 2014-02-26 | Lazyconstr -> Opaqueproof | Enrico Tassi |
| 2014-02-24 | app_node, stack, state printers | Pierre Boutillier |
| 2014-01-11 | 'Pretty' printer for wf_paths | Pierre |
| 2013-11-30 | Adding printing of ltac envs to debugger. | Pierre-Marie Pédrot |
| 2013-09-24 | Adding evar printing to debugger. | ppedrot |
| 2013-09-18 | At least made the evar type opaque! There are still 5 remaining unsafe | ppedrot |
| 2013-08-04 | Small cleaning of printing coercion failures in Ltac interpretation. | ppedrot |
| 2013-07-05 | Removing SortArgType. | ppedrot |
| 2013-07-05 | Expurgating the useless difference between List0 and List1 at the | ppedrot |
| 2013-06-27 | Getting rid of IntroPatternArgType. | ppedrot |
| 2013-06-21 | Cutting the dependency of Genarg in constr_expr, glob_constr | ppedrot |
| 2013-06-19 | Adding genarg printer to debugger. | ppedrot |
| 2013-06-18 | Proof-of-concept: moved four easy-to-handle generic arguments to | ppedrot |
| 2013-06-12 | Added Genarg as generic argument type. | ppedrot |
| 2013-06-06 | Uniformizing generic argument types. | ppedrot |
| 2013-05-14 | Removing useless uses of Gmap. | ppedrot |
| 2013-03-21 | Robust display of NotConvertibleTypeField errors (fix #3008, #2995) | letouzey |
| 2013-02-26 | kernel/declarations becomes a pure mli | letouzey |
| 2013-02-19 | Dir_path --> DirPath | letouzey |
| 2013-02-18 | use List.rev_map whenever possible | letouzey |
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
| 2012-12-18 | Modulification of mod_bound_id | ppedrot |
| 2012-12-18 | Modulification of Label | ppedrot |
| 2012-12-14 | Modulification of dir_path | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-12-14 | Moved Intset and Intmap to Int namespace. | ppedrot |
| 2012-10-06 | still some more dead code removal | letouzey |
| 2012-10-06 | Clean-up : no more Proof_type.proof_tree | letouzey |
| 2012-09-14 | The new ocaml compiler (4.00) has a lot of very cool warnings, | regisgia |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-08-05 | Revert "Fixing include printers" | pboutill |
