aboutsummaryrefslogtreecommitdiff
path: root/pretyping/detyping.ml
AgeCommit message (Expand)Author
2021-02-22Merge PR #13836: Make detyping more resistent in the debuggerPierre-Marie Pédrot
2021-02-17Merge PR #13734: Fix #13732: Implicit Type vs universesPierre-Marie Pédrot
2021-02-08Make detyping more resistent in the debuggerGaëtan Gilbert
2021-01-12Change the case representation of patterns.Pierre-Marie Pédrot
2021-01-11Respect print_universes in detype_instanceGaëtan Gilbert
2021-01-04Make detyping more robust w.r.t. case representation.Pierre-Marie Pédrot
2021-01-04Remove redundant univ and parameter info from CaseInvertGaëtan Gilbert
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
2020-11-25Separate interning and pretyping of universesGaëtan Gilbert
2020-10-13Merge PR #13099: Locating pattern identifiers (?id) by default at parsing tim...Pierre-Marie Pédrot
2020-10-10Add location in existential variable names (CEvar/GEvar).Hugo Herbelin
2020-10-10Adding and using locations on identifiers in constr_expr where they were miss...Hugo Herbelin
2020-10-09Update pretyping/detyping.mlEnrico Tassi
2020-10-09improve commentEnrico Tassi
2020-10-09[printing] make detyping resilient to "let x : _ := t in"Enrico Tassi
2020-07-06Primitive persistent arraysMaxime Dénès
2020-07-01UIP in SPropGaëtan Gilbert
2020-05-13Fixes #12233 (wrong printing env in presence of match branches eta-expansion).Hugo Herbelin
2020-04-21Merge PR #11896: Use lists instead of arrays in evar instances.Maxime Dénès
2020-04-06Clean and fix definitions of options.Théo Zimmermann
2020-04-06Use lists instead of arrays in evar instances.Pierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2020-01-27Small API additions to kernel/univGaëtan Gilbert
2019-12-03Fixes #11231 (missing dependency in pattern-matching decompilation).Hugo Herbelin
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
2019-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
2019-07-08[api] Deprecate GlobRef constructors.Emilio 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-06-01Allowing Set to be part of universe expressions.Hugo Herbelin
2019-06-01Towards unifying parsing/printing for universe instances and Type's argument.Hugo Herbelin
2019-05-13Make detyping robust w.r.t. indexed anonymous variablesMaxime Dénès
2019-04-16Clean the representation of recursive annotation in ConstrexprMaxime 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
2019-04-02Fast name generation in detyping.Pierre-Marie Pédrot
2019-04-02Abstract away the name generation algorithm in Detyping.Pierre-Marie Pédrot
2019-04-02Pass flags through a record in Detyping.Pierre-Marie Pédrot
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-02-18Merge PR #9306: Remove Printing Primitive Projection CompatibilityMaxime Dénès
2019-02-04Merge PR #6914: Primitive integersPierre-Marie Pédrot
2019-02-04Primitive integersMaxime Dénès
2019-01-10Remove Printing Primitive Projection CompatibilityGaëtan Gilbert
2019-01-06Renaming pr_evar_suggested_name into -> evar_suggested_name.Hugo Herbelin
2018-12-12Merge PR #8974: Fix mod_subst wrt universe polymorphismMaxime Dénès
2018-12-12Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix comme...Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:51:47 +0000