aboutsummaryrefslogtreecommitdiff
path: root/vernac/comProgramFixpoint.ml
AgeCommit message (Expand)Author
2018-11-02Fixing one instance of bug #8224 (grounding term w/o knowing if it has evars).Hugo Herbelin
2018-10-30Switch to using the obligation_evar flag instead of the evar sourceMatthieu Sozeau
2018-10-15Correct some spelling errorsBenjamin Barenblat
2018-10-11[vernac] Remove unused abstraction from declaration_hook type.Emilio Jesus Gallego Arias
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-07-17change into QuestionMark defaultSiddharth Bhat
2018-07-17Change QuestionMark for better record field missing error message.Siddharth Bhat
2018-06-18Remove reference name type.Maxime Dénès
2018-05-31[api] Move `Constrexpr` to the `interp` module.Emilio Jesus Gallego Arias
2018-05-17Split off Universes functions dealing with names.Gaëtan Gilbert
2018-05-14Deprecate Typing.e_* functionsGaëtan Gilbert
2018-03-31[econstr] Forbid calling `to_constr` in open terms.Emilio Jesus Gallego Arias
2018-03-09[located] Push inner locations in `reference` to a CAst.t node.Emilio Jesus Gallego Arias
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-01-31 13:06:29 +0000