aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrextern.ml
Commit message (Expand)AuthorAge
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-17
|\
| * Merge PR #310 into v8.6Gravatar Pierre-Marie Pédrot2016-10-17
| |\
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-12
|\| |
| * | Fixing a few confusions on the name of the beautify flag.Gravatar Hugo Herbelin2016-10-12
| | * Revert "Make the pretty printer resilient to incomplete nametab (progress on ...Gravatar Théo Zimmermann2016-10-06
* | | Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Gravatar Maxime Dénès2016-09-22
* | | Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.Gravatar Maxime Dénès2016-09-20
* | | Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
* | | Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/ /
* | Some extra fixes in printing patterns in binders.Gravatar Hugo Herbelin2016-07-19
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* | Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
* | Being defensive in printing implicit arguments also with manualGravatar Hugo Herbelin2016-06-16
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-09
|\|
| * Fix bug #4777: Printing time is impacted by large terms that don't print.Gravatar Pierre-Marie Pédrot2016-06-07
* | A slight phase of documentation and uniformization of names ofGravatar Hugo Herbelin2016-06-02
* | Revert "Being defensive in printing implicit arguments also with manual"Gravatar Hugo Herbelin2016-04-27
* | Being defensive in printing implicit arguments also with manualGravatar Hugo Herbelin2016-04-27
* | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Gravatar Matthieu Sozeau2016-04-04
|\ \
* | | Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Gravatar Hugo Herbelin2016-03-13
* | | A more explicit name to the asymmetric boolean flag.Gravatar Hugo Herbelin2016-03-12
* | | merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\ \ \
* \ \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-13
|\ \ \ \ | | |_|/ | |/| |
| * | | Do not give a name to anonymous evars anymore. See bug #4547.Gravatar Pierre-Marie Pédrot2016-02-13
| | * | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
| |/ / |/| |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\| |
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | | CLEANUP: removing unused fieldGravatar Matej Kosik2016-01-11
* | | Remove some unused functions.Gravatar Guillaume Melquiond2016-01-02
* | | CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedGravatar Matej Kosik2015-12-18
|/ /
* | Fix a bug in externalisation which prevented printing of projectionsGravatar Matthieu Sozeau2015-12-02
* | Make the pretty printer resilient to incomplete nametab (progress on #4363).Gravatar Enrico Tassi2015-11-26
| * Move type_scope into user space, fix some output logsGravatar Jason Gross2015-08-14
|/
* Continuing experimentation on what part of the instance of an evarGravatar Hugo Herbelin2015-02-21
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
* Update headers.Gravatar Maxime Dénès2015-01-12
* Reactivating option "Set Printing Existential Instances" for asking printing ...Gravatar Hugo Herbelin2014-12-04
* Printing function for [uconstr].Gravatar Arnaud Spiwack2014-11-19
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Fix debug printing with primitive projections.Gravatar Matthieu Sozeau2014-09-18
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
* More on printing references applied to implicit arguments.Gravatar Hugo Herbelin2014-09-16
* Parsing evar instances.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Parsing and printing of primitive projections, fix buggy behavior whenGravatar Matthieu Sozeau2014-09-10
* - Fix printing and parsing of primitive projections, including the SetGravatar Matthieu Sozeau2014-09-09
* Fix bug #3591: print differently eta-expanded projection implicit application...Gravatar Matthieu Sozeau2014-09-08
* Parsing of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08