| Commit message (Expand) | Author | Age |
|---|
| * | CLEANUP: Context.{Rel,Named}.Declaration.t |  Matej Kosik | 2016-02-09 |
| * | Update copyright headers. |  Maxime Dénès | 2016-01-20 |
| * | Fix some typos. |  Guillaume Melquiond | 2015-10-13 |
| * | Fixing bug #3811: "Universe annotations confused inside generalizing binders". |  Pierre-Marie Pédrot | 2015-07-29 |
| * | Update headers. | Maxime Dénès | 2015-01-12 |
| * | Remove many superfluous 'open' indicated by ocamlc -w +33 |  Pierre Letouzey | 2014-03-05 |
| * | Merging Context and Sign. |  ppedrot | 2013-04-29 |
| * | Modulification of name | ppedrot | 2012-12-18 |
| * | Modulification of identifier | ppedrot | 2012-12-14 |
| * | Updating headers. |  herbelin | 2012-08-08 |
| * | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot | 2012-06-22 |
| * | 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 |
| * | Noise for nothing |  pboutill | 2012-03-02 |
| * | More comments and less doublons in some mli | pboutill | 2011-02-10 |
| * | More {raw => glob} changes for consistency |  glondu | 2010-12-24 |
| * | Rename rawterm.ml into glob_term.ml | glondu | 2010-12-23 |
| * | Change of nomenclature: rawconstr -> glob_constr | glondu | 2010-12-23 |
| * | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
| * | New script dev/tools/change-header to automatically update Coq files headers. | herbelin | 2010-06-22 |
| * | Fix bug #2262: bad implicit argument number by avoiding counting |  msozeau | 2010-06-09 |
| * | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
| * | Move from ocamlweb to ocamdoc to generate mli documentation | pboutill | 2010-04-29 |
| * | Use generalizable variables info when internalizing arbitrary bindings, | msozeau | 2009-11-08 |
| * | Add a new vernacular command for controling implicit generalization of | msozeau | 2009-10-27 |
| * | Fix bug #2162 and a name clashing bug in generalized binders. | msozeau | 2009-10-09 |
| * | Rewrite of Program Fixpoint to overcome the previous limitations: | msozeau | 2009-03-28 |
| * | Open notation for declaring record instances. | msozeau | 2008-10-23 |
| * | Generalized implementation of generalization. | msozeau | 2008-10-23 |
| * | A much better implementation of implicit generalization: | msozeau | 2008-10-22 |
| * | Fixes in handling of implicit arguments: | msozeau | 2008-07-04 |
| * | Code cleanup in typeclasses, remove dead and duplicated code. | msozeau | 2008-06-21 |
| * | Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient | herbelin | 2008-04-01 |
| * | Do another pass on the typeclasses code. Correct globalization of class | msozeau | 2008-03-19 |
| * | Move generally useful definition of nf_evar on contexts to evarutil. | msozeau | 2008-02-08 |
| * | Generalize instance declarations to any context, better name handling. Add ho... | msozeau | 2008-01-15 |
| * | Cleaner quantifiers for type classes, breaks clrewrite for the moment but imp... | msozeau | 2008-01-07 |
| * | Fix a naming bug reported by Arnaud Spiwack, allow instance search to create ... | msozeau | 2008-01-05 |
| * | Fix name capture bug and call the right pretyper in subtac. | msozeau | 2007-12-31 |
| * | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau | 2007-12-31 |
Matej Kosik
Maxime Dénès
Guillaume Melquiond
Pierre-Marie Pédrot
Pierre Letouzey
ppedrot
herbelin
letouzey
pboutill
glondu
msozeau