| Age | Commit message (Expand) | Author |
|---|
| 2013-05-12 | Use the Hook module here and there. | ppedrot |
| 2013-05-09 | A uniformization step around understand_* and interp_* functions. | herbelin |
| 2013-05-08 | Declaration of multiple hypotheses or parameters now share typing | herbelin |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-03-13 | 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-12 | invalid_arg instead of raise (Invalid_argement ...) | letouzey |
| 2013-03-11 | Added a Local Definition vernacular command. This type of definition | ppedrot |
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
| 2012-12-18 | Modulification of name | ppedrot |
| 2012-12-18 | Modulification of Label | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-12-08 | Finish patch for Hint Resolve, stopping to generate new constant names for | msozeau |
| 2012-11-26 | Monomorphization (toplevel) | ppedrot |
| 2012-10-26 | Change Hint Resolve, Immediate to take a global reference as argument | msozeau |
| 2012-10-02 | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey |
| 2012-09-14 | This patch removes unused "open" (automatically generated from | regisgia |
| 2012-08-24 | Assumption commands are now displayed as unsafe in Coqide. | aspiwack |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-06-22 | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot |
| 2012-06-21 | Fix bug #2808: wrong handling of evars in Instance command. | msozeau |
| 2012-06-04 | Forward-port fixes from 8.4 (15358, 15353, 15333). | msozeau |
| 2012-05-30 | Getting rid of Pp.msg | ppedrot |
| 2012-05-29 | 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-03-20 | Fix interface of resolve_typeclasses: onlyargs -> with_goals: | msozeau |
| 2012-03-19 | Fix bugs related to Program integration. | msozeau |
| 2012-03-14 | Final part of moving Program code inside the main code. Adapted add_definitio... | msozeau |
| 2012-03-14 | Everything compiles again. | msozeau |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-12-12 | Proof using ... | gareuselesinge |
| 2011-11-17 | Merge subinstances branch by me and Tom Prince. | msozeau |
| 2011-10-07 | Fix bug #2557 and an issue with Propers for complement | msozeau |
| 2011-06-30 | Keep obligation source information in Program | msozeau |
| 2011-05-05 | Merge branch 'subclasses' into coq-trunk | msozeau |
| 2011-04-18 | Add a flag to control betaiota reduction during unification to maintain backw... | msozeau |
| 2011-04-13 | Revert "Add [Polymorphic] flag for defs" | msozeau |
| 2011-04-13 | - Make typeclass transparency information directly available | msozeau |
| 2011-04-13 | Add [Polymorphic] flag for defs | msozeau |
| 2011-03-23 | - Fix solve_simpl_eqn which was cheking instances types in the wrong environm... | msozeau |
| 2011-03-13 | - Add modulo_delta_types flag for unification to allow full | msozeau |
| 2011-03-11 | Keep information on which fields are subclasses in class declarations, | msozeau |
| 2011-02-14 | - Fix treatment of globality flag for typeclass instance hints (they | msozeau |
| 2011-02-10 | Interp a definition with the implicit arguments of its local context | pboutill |
| 2011-01-31 | A fine-grain control of inlining at functor application via priority levels | letouzey |
| 2011-01-28 | Remove the "Boxed" syntaxes and the const_entry_boxed field | letouzey |
| 2010-12-23 | Rename rawterm.ml into glob_term.ml | glondu |
| 2010-10-07 | Fix bug# 2392 | msozeau |
| 2010-09-28 | Fix bug #2321, allowing "_" named projections in classes. Not realizing | msozeau |
