aboutsummaryrefslogtreecommitdiff
path: root/engine/evarutil.mli
AgeCommit message (Expand)Author
2017-02-14Evar-normalizing functions now act on EConstrs.Pierre-Marie Pédrot
2017-02-14Removing some return type compatibility layers in Termops.Pierre-Marie Pédrot
2017-02-14Proofview.Goal primitive now return EConstrs.Pierre-Marie Pédrot
2017-02-14Rewrite API using EConstr.Pierre-Marie Pédrot
2017-02-14Hints API using EConstr.Pierre-Marie Pédrot
2017-02-14Leminv API using EConstr.Pierre-Marie Pédrot
2017-02-14Equality API using EConstr.Pierre-Marie Pédrot
2017-02-14Tactics API using EConstr.Pierre-Marie Pédrot
2017-02-14Refine API using EConstr.Pierre-Marie Pédrot
2017-02-14Making judgment type generic over the type of inner constrs.Pierre-Marie Pédrot
2017-02-14Pretyping API using EConstr.Pierre-Marie Pédrot
2017-02-14Evarconv API using EConstr.Pierre-Marie Pédrot
2017-02-14Evarsolve API using EConstr.Pierre-Marie Pédrot
2016-10-21Merge remote-tracking branch 'gforge/v8.5' into v8.6Matthieu Sozeau
2016-08-06Using a dedicated kind of substitutions in evar name generation.Pierre-Marie Pédrot
2016-08-05Using the extended contexts in pretyping.Pierre-Marie Pédrot
2016-08-04Use sets instead of lists for names to avoid in evar generation.Pierre-Marie Pédrot
2016-08-04Simplifying code in evar generation.Pierre-Marie Pédrot
2016-08-04Exporting the renaming API for evar declaration.Pierre-Marie Pédrot
2016-06-09Adding a bit of documentation in the mli.Pierre-Marie Pédrot
2016-03-20Moving Evarutil and Proofview to engine/Pierre-Marie Pédrot