| Commit message (Expand) | Author | Age |
... | |
* | | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod... | Pierre Letouzey | 2016-07-03 |
* | | Adding ability to put any pattern in binders, prefixed by a quote. | Daniel de Rauglaudre | 2016-06-27 |
* | | Being defensive in printing implicit arguments also with manual | Hugo Herbelin | 2016-06-16 |
* | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-06-09 |
|\| |
|
| * | Fix bug #4777: Printing time is impacted by large terms that don't print. | Pierre-Marie Pédrot | 2016-06-07 |
* | | A slight phase of documentation and uniformization of names of | Hugo Herbelin | 2016-06-02 |
* | | Revert "Being defensive in printing implicit arguments also with manual" | Hugo Herbelin | 2016-04-27 |
* | | Being defensive in printing implicit arguments also with manual | Hugo Herbelin | 2016-04-27 |
* | | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into... | Matthieu Sozeau | 2016-04-04 |
|\ \ |
|
* | | | Supporting "(@foo) args" in patterns, where "@foo" has no arguments. | Hugo Herbelin | 2016-03-13 |
* | | | A more explicit name to the asymmetric boolean flag. | Hugo Herbelin | 2016-03-12 |
* | | | merging conflicts with the original "trunk__CLEANUP__Context__2" branch | Matej Kosik | 2016-02-15 |
|\ \ \ |
|
* \ \ \ | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-02-13 |
|\ \ \ \
| | |_|/
| |/| | |
|
| * | | | Do not give a name to anonymous evars anymore. See bug #4547. | Pierre-Marie Pédrot | 2016-02-13 |
| | * | | CLEANUP: Context.{Rel,Named}.Declaration.t | Matej Kosik | 2016-02-09 |
| |/ /
|/| | |
|
* | | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-01-21 |
|\| | |
|
| * | | Update copyright headers. | Maxime Dénès | 2016-01-20 |
* | | | CLEANUP: removing unused field | Matej Kosik | 2016-01-11 |
* | | | Remove some unused functions. | Guillaume Melquiond | 2016-01-02 |
* | | | CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified | Matej Kosik | 2015-12-18 |
|/ / |
|
* | | Fix a bug in externalisation which prevented printing of projections | Matthieu Sozeau | 2015-12-02 |
* | | Make the pretty printer resilient to incomplete nametab (progress on #4363). | Enrico Tassi | 2015-11-26 |
| * | Move type_scope into user space, fix some output logs | Jason Gross | 2015-08-14 |
|/ |
|
* | Continuing experimentation on what part of the instance of an evar | Hugo Herbelin | 2015-02-21 |
* | Univs: proper printing of global and local universe names (only | Matthieu Sozeau | 2015-01-17 |
* | Update headers. | Maxime Dénès | 2015-01-12 |
* | Reactivating option "Set Printing Existential Instances" for asking printing ... | Hugo Herbelin | 2014-12-04 |
* | Printing function for [uconstr]. | Arnaud Spiwack | 2014-11-19 |
* | A patch for printing "match" when constructors are defined with let-in | Hugo Herbelin | 2014-10-20 |
* | Add syntax for naming new goals in refine: writing ?[id] instead of _ | Hugo Herbelin | 2014-09-30 |
* | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau | 2014-09-27 |
* | Fix debug printing with primitive projections. | Matthieu Sozeau | 2014-09-18 |
* | Revert specific syntax for primitive projections, avoiding ugly | Matthieu Sozeau | 2014-09-17 |
* | More on printing references applied to implicit arguments. | Hugo Herbelin | 2014-09-16 |
* | Parsing evar instances. | Hugo Herbelin | 2014-09-12 |
* | Referring to evars by names. Added a parser for evars (but parsing of | Hugo Herbelin | 2014-09-12 |
* | Parsing and printing of primitive projections, fix buggy behavior when | Matthieu Sozeau | 2014-09-10 |
* | - Fix printing and parsing of primitive projections, including the Set | Matthieu Sozeau | 2014-09-09 |
* | Fix bug #3591: print differently eta-expanded projection implicit application... | Matthieu Sozeau | 2014-09-08 |
* | Parsing of Type@{max(i,j)}. | Matthieu Sozeau | 2014-09-08 |
* | Spotted a source of failure of the constr printer in debugger. | Hugo Herbelin | 2014-08-18 |
* | Fix non-printing of coercions for primitive projections (fixes bug #3433). | Matthieu Sozeau | 2014-08-14 |
* | Change internalization of primitive projections to allow parsing [p t] as | Matthieu Sozeau | 2014-08-08 |
* | A tentative uniform naming policy in module Inductiveops. | Hugo Herbelin | 2014-08-01 |
* | Consistent pretty-printing of primitive projections and their expanded forms. | Matthieu Sozeau | 2014-07-31 |
* | Fix printing of projections with implicits. | Matthieu Sozeau | 2014-05-06 |
* | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
* | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey | 2014-03-05 |
* | Never suppress the typing constraint of bound variables whose name was | Pierre-Marie Pédrot | 2014-03-01 |
* | Adding generic solvers to term holes. For now, no resolution mechanism nor | Pierre-Marie Pédrot | 2013-11-27 |