aboutsummaryrefslogtreecommitdiff
path: root/pretyping/glob_ops.mli
AgeCommit message (Expand)Author
2020-11-25Separate interning and pretyping of universesGaëtan Gilbert
2020-04-06Fix #11934 equality on constrexpr ignores instances of explicit applicationsGaëtan Gilbert
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-12-03Printing: Interleaving search for notations and removal of coercions.Hugo Herbelin
2019-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-01Allowing Set to be part of universe expressions.Hugo Herbelin
2019-04-10Remove calls to global env in InductiveopsMaxime Dénès
2019-04-10Remove calls to Global.env in Glob_opsMaxime Dénès
2019-03-18Fix constr_matching on SPropGaëtan Gilbert
2019-02-19Notations: Enforce strong evaluation of cases_pattern_of_glob_constr.Hugo Herbelin
2018-09-10Moving part of pretyping dealing with ltac and renaming in new module GlobEnv.Hugo Herbelin
2018-09-10Files pretyping.ml, glob_obs.ml, evarutil.ml: rewording/typos in some comments.Hugo Herbelin
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-20Using an "as" clause when needed for printing irrefutable patterns.Hugo Herbelin
2018-02-20Adding patterns in the category of binders for notations.Hugo Herbelin
2018-02-20Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.Hugo Herbelin
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-10-25[general] Remove Econstr dependency from `intf`Emilio Jesus Gallego Arias
2017-09-28Efficient fresh name generation relying on sets.Pierre-Marie Pédrot
2017-09-04Making detyping potentially lazy.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-09A fix to #5414 (ident bound by ltac names now known for "match").Hugo Herbelin
2017-06-08Merge branch 'v8.6'Pierre-Marie Pédrot
2017-05-31Fixing #5523 (missing support for complex constructions in recursive notations).Hugo Herbelin
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-04-13Adding a fold_glob_constr_with_binders combinator.Hugo Herbelin
2017-04-07Better support for printing constructors with let-ins.Hugo Herbelin
2016-07-18A new step on using alpha-conversion in printing notations.Hugo Herbelin
2016-07-17Partial fix to #4592 (notation requiring alpha-conversion for printing).Hugo Herbelin
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-04-19Fixing #4677 (collision of a global variable and of a local variableHugo Herbelin
2016-01-20Update copyright headers.Maxime Dénès
2015-10-11Fixing untimely unexpected warning "Collision between bound variables" (#4317).Hugo Herbelin
2015-03-24Fixing equality of notation_constrs. Fixes bug #4136.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-11-19Printing function for [uconstr].Arnaud Spiwack
2014-11-19Glob-ops: a name-mapping operation for pattern-matching binders.Arnaud Spiwack
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-03-02Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codePierre Letouzey
2014-03-02Adding an equality function over glob_constrPierre-Marie Pédrot
2013-04-29Merging Context and Sign.ppedrot
2012-12-18Modulification of nameppedrot
2012-12-14Modulification of identifierppedrot
2012-11-23Added a constr_pattern_eqppedrot
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:08:40 +0000