aboutsummaryrefslogtreecommitdiff
path: root/interp/constrintern.ml
AgeCommit message (Expand)Author
2016-07-19Removing a source of clash with multiple recursive patterns in notations.Hugo Herbelin
2016-07-17Fixing #4932 (anomaly when using binders as terms in recursive notations).Hugo Herbelin
2016-07-16Fixing a collision about the meta-variable ".." in recursive notations.Hugo Herbelin
2016-07-07Merge remote-tracking branch 'github/bug4653' into v8.6Matthieu Sozeau
2016-07-07Do not use implicit type info for (x := t) bindingsMatthieu Sozeau
2016-07-07Program: fix #4873: transparency option not usedMatthieu Sozeau
2016-07-06Univs: fix internalization of (x := T) and castsMatthieu Sozeau
2016-07-04Merge branch 'v8.5' into trunkMaxime Dénès
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-06-27Univs: allowing notations to take univ instancesMatthieu Sozeau
2016-06-27Forbidding silently dropped universes instances inMatthieu Sozeau
2016-06-27minor: comment on the meaning of the 'boolean' variableGabriel Scherer
2016-06-27minor: documentation comment for constrintern.ml:sort_fieldsGabriel Scherer
2016-06-27minor: interp/constrintern.ml, clarify field completionGabriel Scherer
2016-06-27minor: in constrintern.ml:sort_fields, clarify sfGabriel Scherer
2016-06-27minor: in constrintern.ml:sort_fields, clarify build_pattGabriel Scherer
2016-06-27whitespace: untabity constrinternl.ml:sort_fieldsGabriel Scherer
2016-06-27minor clarifications in constrintern.ml:sort_fieldsGabriel Scherer
2016-06-27Adding ability to put any pattern in binders, prefixed by a quote.Daniel de Rauglaudre
2016-06-16Not taking arguments given by name or position into account whenHugo Herbelin
2016-06-02A slight phase of documentation and uniformization of names ofHugo Herbelin
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-03Fix bug #3825: Universe annotations on notations should pass through or be re...Pierre-Marie Pédrot
2016-04-27Revert "Not taking arguments given by name or position into account when"Hugo Herbelin
2016-04-27Revert "Warn about possible shadowing of a name occurring in a "in" clause."Hugo Herbelin
2016-04-27Warn about possible shadowing of a name occurring in a "in" clause.Hugo Herbelin
2016-04-27Not taking arguments given by name or position into account whenHugo Herbelin
2016-04-27Fixing a "This clause is redundant" error when interpreting the "in"Hugo Herbelin
2016-04-27Reformatting + removal of some useless data + some cut-eliminationHugo Herbelin
2016-04-04Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Matthieu Sozeau
2016-03-13Adopting the same rules for interpreting @, abbreviations andHugo Herbelin
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-28Printing notations: Cleaning in anticipation of fixing #4592.Hugo Herbelin
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-11mergeMatej Kosik
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2016-01-02Remove some unused functions.Guillaume Melquiond
2015-12-31Do not compose List.length with List.filter.Guillaume Melquiond
2015-12-18CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedMatej Kosik
2015-11-11Fixing bug #3554: Anomaly: Anonymous implicit argument.Pierre-Marie Pédrot
2015-09-16Properly handle {|...|} patterns when patterns are not asymmetric. (Fix bug #...Guillaume Melquiond
2015-08-21Fixing #4318 (anomaly when applying args to a recursive notation in patterns).Hugo Herbelin
2015-08-14Move type_scope into user space, fix some output logsJason Gross
2015-07-27Fixing #4305 (compatibility wrt 8.4 in not interpreting anHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 06:58:04 +0000