aboutsummaryrefslogtreecommitdiff
path: root/vernac/himsg.mli
AgeCommit message (Expand)Author
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-07-07[error] Remove special error printing pre-processingEmilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-11Fix #10225 (Instance := {} accepts duplicate fields)Gaëtan Gilbert
2019-05-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
2019-02-25Fix #9631: Instance: anomaly grounding non evar-free termGaëtan Gilbert
2019-02-11Fix #9527: unknown evar in nonterminating [fix] error.Gaëtan Gilbert
2019-01-21Move inductive_error to Type_errorsGaëtan Gilbert
2018-11-28Factor out common code in numeral/string notationsJason Gross
2018-11-28Add `String Notation` vernacular like `Numeral Notation`Jason Gross
2018-09-28Functionalizing calls to the environment in Himsg.Hugo Herbelin
2018-09-19Fix Numeral Notations (2/4 - exceptions, usr_err)Jason Gross
2018-06-27Swapping Context and Constr: defining declarations on constr in Constr.Hugo Herbelin
2018-05-31[api] Move `Constrexpr` to the `interp` module.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-11-21[printing] Deprecate all printing functions accessing the global proof.Emilio Jesus Gallego Arias
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-02-15[stm] Break stm/toplevel dependency loop.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:06:51 +0000