aboutsummaryrefslogtreecommitdiff
path: root/pretyping/detyping.mli
AgeCommit message (Expand)Author
2021-01-12Change the case representation of patterns.Pierre-Marie Pédrot
2020-04-06Clean and fix definitions of options.Théo Zimmermann
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
2019-06-25Merge PR #10284: Expose set interface to option tablesPierre-Marie Pédrot
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-03Expose set interface to option tablesGaëtan Gilbert
2019-05-13Make detyping robust w.r.t. indexed anonymous variablesMaxime Dénès
2019-04-10Remove calls to global env in InductiveopsMaxime Dénès
2019-04-10Remove one call to Global.env in DetypingMaxime Dénès
2018-06-18Remove reference name type.Maxime Dénès
2018-05-08[api] Move universe syntax to `Glob_term`Emilio Jesus Gallego Arias
2018-03-28Detyping: Adding a variant of share_names for patterns.Hugo Herbelin
2018-02-27Update headers following #6543.Théo Zimmermann
2017-12-12In printing, factorizing "match" clauses with same right-hand side.Hugo Herbelin
2017-11-06[api] Move structures deprecated in the API to the 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-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-04-25[location] [ast] Port module AST to CAstEmilio Jesus Gallego Arias
2017-04-24[location] Switch glob_constr to Loc.locatedEmilio Jesus Gallego Arias
2017-02-14Namegen primitives now apply on evar constrs.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-01-18Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-13Fix issue in printing due to de Bruijn bug when constructing compatibilityMatthieu 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-17Revert specific syntax for primitive projections, avoiding uglyMatthieu Sozeau
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-03-03Goptions do not rely anymore on generic equality.Pierre-Marie Pédrot
2013-11-27Adding generic solvers to term holes. For now, no resolution mechanism norPierre-Marie Pédrot
2013-04-29Merging Context and Sign.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2012-12-18Modulification of nameppedrot
2012-12-14Modulification of identifierppedrot
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29No more Univ in grammar.cmaletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-03-02Glob_term.predicate_pattern: No number of parameters with letins.pboutill
2012-03-02Noise for nothingpboutill
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:08:52 +0000