index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
engine
/
evarutil.mli
Commit message (
Expand
)
Author
Age
*
Make the Constr.kind_of_term type parametric in sorts and universes.
Pierre-Marie Pédrot
2017-03-31
*
Namegen primitives now apply on evar constrs.
Pierre-Marie Pédrot
2017-02-14
*
Definining EConstr-based contexts.
Pierre-Marie Pédrot
2017-02-14
*
Evar-normalizing functions now act on EConstrs.
Pierre-Marie Pédrot
2017-02-14
*
Removing some return type compatibility layers in Termops.
Pierre-Marie Pédrot
2017-02-14
*
Proofview.Goal primitive now return EConstrs.
Pierre-Marie Pédrot
2017-02-14
*
Rewrite API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Hints API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Leminv API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Equality API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Tactics API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Refine API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Making judgment type generic over the type of inner constrs.
Pierre-Marie Pédrot
2017-02-14
*
Pretyping API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Evarconv API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Evarsolve API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Merge remote-tracking branch 'gforge/v8.5' into v8.6
Matthieu Sozeau
2016-10-21
*
Using a dedicated kind of substitutions in evar name generation.
Pierre-Marie Pédrot
2016-08-06
*
Using the extended contexts in pretyping.
Pierre-Marie Pédrot
2016-08-05
*
Use sets instead of lists for names to avoid in evar generation.
Pierre-Marie Pédrot
2016-08-04
*
Simplifying code in evar generation.
Pierre-Marie Pédrot
2016-08-04
*
Exporting the renaming API for evar declaration.
Pierre-Marie Pédrot
2016-08-04
*
Adding a bit of documentation in the mli.
Pierre-Marie Pédrot
2016-06-09
*
Moving Evarutil and Proofview to engine/
Pierre-Marie Pédrot
2016-03-20
Pierre-Marie Pédrot
Matthieu Sozeau