index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
engine
/
evarutil.mli
Age
Commit message (
Expand
)
Author
2017-11-21
Experimenting with a fine-grained cache for undefined evars in evinfos.
Pierre-Marie Pédrot
2017-11-06
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-04
[api] Deprecate all legacy uses of Name.Id in core.
Emilio Jesus Gallego Arias
2017-09-27
Moving setting of "cleared" evar flag directly in Evd.restrict.
Hugo Herbelin
2017-08-29
Merge PR #830: Moving assert (the "Cut" rule) to new proof engine
Maxime Dénès
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-25
Adding intermediate entry point to create an evar in empty rel_context.
Hugo Herbelin
2017-06-06
Remove the Sigma (monotonous state) API.
Maxime Dénès
2017-05-30
Support for using type information to infer more precise evar sources.
Hugo Herbelin
2017-04-25
[location] Make location optional in Loc.located
Emilio Jesus Gallego Arias
2017-03-31
Make the Constr.kind_of_term type parametric in sorts and universes.
Pierre-Marie Pédrot
2017-02-14
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
2016-10-21
Merge remote-tracking branch 'gforge/v8.5' into v8.6
Matthieu Sozeau
2016-08-06
Using a dedicated kind of substitutions in evar name generation.
Pierre-Marie Pédrot
2016-08-05
Using the extended contexts in pretyping.
Pierre-Marie Pédrot
2016-08-04
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-06-09
Adding a bit of documentation in the mli.
Pierre-Marie Pédrot
2016-03-20
Moving Evarutil and Proofview to engine/
Pierre-Marie Pédrot
[prev]
