aboutsummaryrefslogtreecommitdiff
path: root/vernac/comFixpoint.ml
AgeCommit message (Expand)Author
2018-06-26universes_of_constr don't include universes of monomorphic constantsGaëtan Gilbert
2018-06-12[api] Misctypes removal: miscellaneous aliases.Emilio Jesus Gallego Arias
2018-06-04Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode.Matthieu Sozeau
2018-05-31[api] Move `Constrexpr` to the `interp` module.Emilio Jesus Gallego Arias
2018-05-25Remove some occurrences of Evd.emptyMaxime Dénès
2018-05-14Deprecate Typing.e_* functionsGaëtan Gilbert
2018-04-17Deprecate mixing univ minimization and evm normalization functions.Gaëtan Gilbert
2018-03-31[econstr] Forbid calling `to_constr` in open terms.Emilio Jesus Gallego Arias
2018-03-29Fix #6770: fixpoint loses locality info in proof mode.Gaëtan Gilbert
2018-03-05Allow universe declarations for [with Definition].Gaëtan Gilbert
2018-02-28[econstr] Continue consolidation of EConstr API under `interp`.Emilio Jesus Gallego Arias
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2017-12-17[vernac] Split `command.ml` into separate files.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 06:22:43 +0000