| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Update headers. |  Maxime Dénès | 2015-01-12 |
| | | |||
| * | Simplification of Genarg unpackers. |  Pierre-Marie Pédrot | 2014-08-29 |
| | | | | | | Instead of having a version of unpackers for each level, we use a dummy argument to force unification of types. | ||
| * | Remove many superfluous 'open' indicated by ocamlc -w +33 |  Pierre Letouzey | 2014-03-05 |
| | | | | | | | | | With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment. | ||
| * | Adding a default object to generic argument registering mechanism. | Pierre-Marie Pédrot | 2014-01-19 |
| | | |||
| * | Splitted up Genarg in four different levels: |  ppedrot | 2013-06-21 |
| 1. Genarg itself which only defines the abstract datatypes needed. 2. Genintern, first file of interp/, defining the intern and subst functions. 3. Geninterp, first file of tactics/, defining the interp function. 4. Genprint, first file of printing/, dealing with the printers. The Genarg file has no dependency and is in lib/, so that we can put generic arguments everywhere, and in particular in ASTs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16601 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |