aboutsummaryrefslogtreecommitdiff
path: root/interp/constrextern.ml
AgeCommit message (Expand)Author
2016-10-17Merge PR #310 into v8.6Pierre-Marie Pédrot
2016-10-12Fixing a few confusions on the name of the beautify flag.Hugo Herbelin
2016-10-06Revert "Make the pretty printer resilient to incomplete nametab (progress on ...Théo Zimmermann
2016-07-19Some extra fixes in printing patterns in binders.Hugo Herbelin
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-27Adding ability to put any pattern in binders, prefixed by a quote.Daniel de Rauglaudre
2016-06-16Being defensive in printing implicit arguments also with manualHugo Herbelin
2016-06-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-07Fix bug #4777: Printing time is impacted by large terms that don't print.Pierre-Marie Pédrot
2016-06-02A slight phase of documentation and uniformization of names ofHugo Herbelin
2016-04-27Revert "Being defensive in printing implicit arguments also with manual"Hugo Herbelin
2016-04-27Being defensive in printing implicit arguments also with manualHugo Herbelin
2016-04-04Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Matthieu Sozeau
2016-03-13Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Hugo Herbelin
2016-03-12A more explicit name to the asymmetric boolean flag.Hugo Herbelin
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
2016-02-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-13Do not give a name to anonymous evars anymore. See bug #4547.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: removing unused fieldMatej Kosik
2016-01-02Remove some unused functions.Guillaume Melquiond
2015-12-18CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedMatej Kosik
2015-12-02Fix a bug in externalisation which prevented printing of projectionsMatthieu Sozeau
2015-11-26Make the pretty printer resilient to incomplete nametab (progress on #4363).Enrico Tassi
2015-08-14Move type_scope into user space, fix some output logsJason Gross
2015-02-21Continuing experimentation on what part of the instance of an evarHugo Herbelin
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-12-04Reactivating option "Set Printing Existential Instances" for asking printing ...Hugo Herbelin
2014-11-19Printing function for [uconstr].Arnaud Spiwack
2014-10-20A patch for printing "match" when constructors are defined with let-inHugo Herbelin
2014-09-30Add syntax for naming new goals in refine: writing ?[id] instead of _Hugo Herbelin
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-18Fix debug printing with primitive projections.Matthieu Sozeau
2014-09-17Revert specific syntax for primitive projections, avoiding uglyMatthieu Sozeau
2014-09-16More on printing references applied to implicit arguments.Hugo Herbelin
2014-09-12Parsing evar instances.Hugo Herbelin
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-09-10Parsing and printing of primitive projections, fix buggy behavior whenMatthieu Sozeau
2014-09-09- Fix printing and parsing of primitive projections, including the SetMatthieu Sozeau
2014-09-08Fix bug #3591: print differently eta-expanded projection implicit application...Matthieu Sozeau
2014-09-08Parsing of Type@{max(i,j)}.Matthieu Sozeau
2014-08-18Spotted a source of failure of the constr printer in debugger.Hugo Herbelin
2014-08-14Fix non-printing of coercions for primitive projections (fixes bug #3433).Matthieu Sozeau
2014-08-08Change internalization of primitive projections to allow parsing [p t] asMatthieu Sozeau
2014-08-01A tentative uniform naming policy in module Inductiveops.Hugo Herbelin
2014-07-31Consistent pretty-printing of primitive projections and their expanded forms.Matthieu Sozeau
2014-05-06Fix printing of projections with implicits.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 20:32:50 +0000