index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
engine
/
evd.ml
Commit message (
Expand
)
Author
Age
...
*
|
|
Ltac now uses evar-based constrs.
Pierre-Marie Pédrot
2017-02-14
|
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-02-01
|
|
\
|
|
|
*
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2017-01-23
|
*
|
Adding a new evar source to remember the name of evars which were
Hugo Herbelin
2017-01-22
|
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-12-07
|
/
|
|
|
|
/
|
*
Fix UGraph.check_eq!
Matthieu Sozeau
2016-11-30
*
|
Reordering Termops w.r.t. Evd and Namegen in engine folder.
Pierre-Marie Pédrot
2016-10-30
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-29
|
\
|
|
*
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-26
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-17
|
\
|
|
*
Fix bug #5145: Anomaly: index to an anonymous variable.
Pierre-Marie Pédrot
2016-10-15
*
|
Merge PR #244.
Pierre-Marie Pédrot
2016-09-08
|
\
\
*
|
|
CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...
Matej Kosik
2016-08-30
*
|
|
CLEANUP: rename "Context.Named.{to,of}_rel" functions to "Context.Named.{to,o...
Matej Kosik
2016-08-26
*
|
|
CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to "Contex...
Matej Kosik
2016-08-25
*
|
|
CLEANUP: removing calls of the "Context.Named.Declaration.get_value" function
Matej Kosik
2016-08-25
*
|
|
CLEANUP: minor readability improvements
Matej Kosik
2016-08-24
|
|
/
|
/
|
|
*
Make the user_err header an optional parameter.
Emilio Jesus Gallego Arias
2016-08-19
|
*
Unify location handling of error functions.
Emilio Jesus Gallego Arias
2016-08-19
|
/
*
Two protections against failures when printing evar_map.
Hugo Herbelin
2016-08-17
*
Remove unused optional "predicative" argument.
Guillaume Melquiond
2016-08-10
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
Univs: add source locations of levels
Matthieu Sozeau
2016-06-29
*
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-05-08
*
Allowing to attach location to universes in UState.
Pierre-Marie Pédrot
2016-02-19
*
merging conflicts with the original "trunk__CLEANUP__Context__2" branch
Matej Kosik
2016-02-15
|
\
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-02-13
|
*
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
|
/
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-29
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
*
Remove useless rec flags.
Guillaume Melquiond
2016-01-02
*
Merge branch 'v8.5' into trunk
Guillaume Melquiond
2015-12-31
*
CLEANUP: in the Reduction module
Matej Kosik
2015-12-17
*
CLEANUP: in the Reduction module
Matej Kosik
2015-12-17
*
Remove unneeded fixpoint in normalize_context_set. Note that it is no
Matthieu Sozeau
2015-12-01
*
More efficient implementation of equality-up-to-universes in Universes.
Pierre-Marie Pédrot
2015-11-26
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
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
*
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-17
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-15
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-09
*
Splitting kernel universe code in two modules.
Pierre-Marie Pédrot
2015-10-06
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-06
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-02
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-02
*
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
[prev]
[next]