aboutsummaryrefslogtreecommitdiff
path: root/interp/constrextern.ml
AgeCommit message (Expand)Author
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-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
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-03-01Never suppress the typing constraint of bound variables whose name wasPierre-Marie Pédrot
2013-11-27Adding generic solvers to term holes. For now, no resolution mechanism norPierre-Marie Pédrot
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-05-05Now printing body of abbreviations (i.e. notation with a name) withherbelin
2013-03-21Robust display of NotConvertibleTypeField errors (fix #3008, #2995)letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 8)letouzey
2013-01-28Uniformization of the "anomaly" command.ppedrot
2013-01-07Fixup notation printing in patternspboutill
2012-12-14Modulification of identifierppedrot
2012-12-14Implemented a full-fledged equality on [constr_expr]. By the way,ppedrot
2012-12-13Using library string functions.ppedrot
2012-12-13Renamed Option.Misc.compare to the more uniform Option.equal.ppedrot
2012-11-28Fix ocamldebug constr printerpboutill
2012-11-26Fixed a monomorphization error.ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 13:31:34 +0000