| Age | Commit message (Expand) | Author |
|---|---|---|
| 2013-09-18 | At least made the evar type opaque! There are still 5 remaining unsafe | ppedrot |
| 2013-07-17 | Declaremods: major refactoring, stop duplicating libobjects in modules | letouzey |
| 2013-07-09 | Revising r16550 about providing intro patterns for applying injection: | herbelin |
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-10-02 | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey |
| 2012-10-02 | avoid referring to Term in constrexpr.mli and glob_term.mli | letouzey |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-08-07 | Avoid Pp.std_ppcmds in Misctypes.sort_info | letouzey |
| 2012-06-22 | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot |
| 2012-05-29 | No more Univ in grammar.cma | letouzey |
| 2012-05-29 | Glob_term now mli-only, operations now in Glob_ops | letouzey |
| 2012-05-29 | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |