index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
engine
/
evd.mli
Age
Commit message (
Expand
)
Author
2017-07-04
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-15
Merge PR#713: Bump year in headers.
Maxime Dénès
2017-06-05
Univs: fix bug #5365, generation of u+k <= v constraints
Matthieu Sozeau
2017-06-01
Bump year in headers.
Maxime Dénès
2017-05-30
Support for using type information to infer more precise evar sources.
Hugo Herbelin
2017-04-25
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-04-07
Merge branch 'master' into econstr
Pierre-Marie Pédrot
2017-03-23
Ensuring static invariants about handling of pending evars in Pretyping.
Pierre-Marie Pédrot
2017-02-14
Merge branch 'master'.
Pierre-Marie Pédrot
2017-02-14
Making Evd independent from Namegen.
Pierre-Marie Pédrot
2017-02-14
Moving printing code from Evd to Termops.
Pierre-Marie Pédrot
2017-02-14
Chasing a few unsafe constr coercions.
Pierre-Marie Pédrot
2017-02-14
Removing various compatibility layers of tactics.
Pierre-Marie Pédrot
2017-02-14
Ltac now uses evar-based constrs.
Pierre-Marie Pédrot
2016-12-07
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-12-02
Document changes
Matthieu Sozeau
2016-11-30
Fix UGraph.check_eq!
Matthieu Sozeau
2016-10-30
Reordering Termops w.r.t. Evd and Namegen in engine folder.
Pierre-Marie Pédrot
2016-09-01
Short documentation, filling TODO's in evd.mli.
Hugo Herbelin
2016-08-10
Remove unused optional "predicative" argument.
Guillaume Melquiond
2016-06-29
Univs: add source locations of levels
Matthieu Sozeau
2016-06-09
Adding a bit of documentation in the mli.
Pierre-Marie Pédrot
2016-02-19
Allowing to attach location to universes in UState.
Pierre-Marie Pédrot
2016-02-13
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-29
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-11
merge
Matej Kosik
2016-01-11
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-01
Remove duplicate declarations.
Guillaume Melquiond
2015-11-20
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-05
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-30
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-29
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-17
Clarifying and documenting the UState API.
Pierre-Marie Pédrot
2015-10-17
Dedicated file for universe unification context manipulation.
Pierre-Marie Pédrot
2015-10-09
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-06
Splitting kernel universe code in two modules.
Pierre-Marie Pédrot
2015-10-02
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-09-27
Removing meta_with_name from Evd.
Pierre-Marie Pédrot
2015-09-27
Removing subst_defined_metas_evars from Evd.
Pierre-Marie Pédrot
2015-09-27
Removing uselessly duplicated function in Evd.
Pierre-Marie Pédrot
2015-09-26
Hardening the API of evarmaps.
Pierre-Marie Pédrot
2015-09-17
Merge branch 'v8.5' into trunk
Maxime Dénès
2015-06-01
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-05-05
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-03-23
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-02-27
Adding a new folder corresponding to the low-level part of the pretyper
Pierre-Marie Pédrot