aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/evarutil.mli
Commit message (Expand)AuthorAge
* [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* Make the Constr.kind_of_term type parametric in sorts and universes.Gravatar Pierre-Marie Pédrot2017-03-31
* Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Removing some return type compatibility layers in Termops.Gravatar Pierre-Marie Pédrot2017-02-14
* Proofview.Goal primitive now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Rewrite API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Hints API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Leminv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Equality API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Refine API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Making judgment type generic over the type of inner 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
* Evarsolve API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-10-21
* Using a dedicated kind of substitutions in evar name generation.Gravatar Pierre-Marie Pédrot2016-08-06
* Using the extended contexts in pretyping.Gravatar Pierre-Marie Pédrot2016-08-05
* Use sets instead of lists for names to avoid in evar generation.Gravatar Pierre-Marie Pédrot2016-08-04
* Simplifying code in evar generation.Gravatar Pierre-Marie Pédrot2016-08-04
* Exporting the renaming API for evar declaration.Gravatar Pierre-Marie Pédrot2016-08-04
* Adding a bit of documentation in the mli.Gravatar Pierre-Marie Pédrot2016-06-09
* Moving Evarutil and Proofview to engine/Gravatar Pierre-Marie Pédrot2016-03-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 02:54:41 +0000