aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evardefine.mli
Commit message (Collapse)AuthorAge
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| | | | We do up to `Term` which is the main bulk of the changes.
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print <unknown> anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed <unknown> and other times it printed nothing as the caller checked for `is_ghost` upstream.
* Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Pretyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Evarconv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Evardefine API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Splitting Evarutil in two distinct files.Gravatar Pierre-Marie Pédrot2016-03-20
Some parts of Evarutils were related to the management of evars under constraints. We put them in the Evardefine file.