| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | Lazy interpretation of patterns so that expressions such as "intros H H'/H" |  Hugo Herbelin | 2014-08-18 |
| * | Adding a new intro-pattern for "apply in" on the fly. Using syntax | Hugo Herbelin | 2014-08-18 |
| * | Reorganisation of intropattern code | Hugo Herbelin | 2014-08-18 |
| * | Remove many superfluous 'open' indicated by ocamlc -w +33 |  Pierre Letouzey | 2014-03-05 |
| * | Added an indirection with respect to Loc in Compat. As many [open Compat] |  ppedrot | 2012-06-22 |
| * | remove many excessive open Util & Errors in mli's |  letouzey | 2012-05-29 |
| * | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey | 2012-05-29 |
| * | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey | 2012-05-29 |
| * | Noise for nothing |  pboutill | 2012-03-02 |
| * | Rename rawterm.ml into glob_term.ml |  glondu | 2010-12-23 |
| * | Using vernac parsing for Function |  jforest | 2010-06-08 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |