index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
unification.ml
Commit message (
Expand
)
Author
Age
...
|
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-11-18
|
/
|
*
|
Stronger static invariant in equality upto universes.
Pierre-Marie Pédrot
2016-10-31
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-24
|
\
\
|
|
*
Renamings to avoid confusion deprecating old names
Matthieu Sozeau
2016-10-22
|
|
*
Unification constraint handling (#4763, #5149)
Matthieu Sozeau
2016-10-22
|
|
*
Port fix for bugs 4763, 5149, previously 0b417c12e
Matthieu Sozeau
2016-10-22
|
|
/
|
*
Merge remote-tracking branch 'gforge/v8.5' into v8.6
Matthieu Sozeau
2016-10-21
|
|
\
|
|
*
Revert "unification.ml: fix for bug #4763, unif regression"
Maxime Dénès
2016-10-21
*
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-08
|
\
|
|
|
*
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-08
|
|
\
|
|
|
*
w_merge: Add a comment about the (List.rev evars)
Matthieu Sozeau
2016-10-06
|
|
*
unification.ml: fix for bug #4763, unif regression
Matthieu Sozeau
2016-10-06
*
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-05
|
\
|
|
|
*
|
Merge remote-tracking branch 'github/pr/263' into v8.6
Maxime Dénès
2016-10-03
|
|
\
\
*
|
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-09-23
|
\
|
|
|
|
*
|
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-09-23
|
|
\
\
\
|
|
|
|
/
|
|
|
/
|
|
|
*
|
Fixing #5095 (non relevant too strict test in let-in abstraction).
Hugo Herbelin
2016-09-22
*
|
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-09-14
|
\
|
|
|
|
*
|
|
no-refold patch
Paul Steckler
2016-09-09
|
|
|
*
Tracking careless uses of slow name lookup.
Pierre-Marie Pédrot
2016-09-09
|
|
|
/
|
|
/
|
*
|
|
Merge PR #244.
Pierre-Marie Pédrot
2016-09-08
|
\
\
\
*
\
\
\
Merge remote-tracking branch 'v8.6' into trunk
Matej Kosik
2016-08-25
|
\
\
\
\
|
|
|
/
/
|
|
/
|
|
*
|
|
|
CLEANUP: minor readability improvements
Matej Kosik
2016-08-24
|
*
|
|
Pushing error backtrace in unification reraise.
Pierre-Marie Pédrot
2016-08-22
|
/
/
/
|
*
|
Make the user_err header an optional parameter.
Emilio Jesus Gallego Arias
2016-08-19
|
*
|
Remove errorlabstrm in favor of user_err
Emilio Jesus Gallego Arias
2016-08-19
|
/
/
*
|
closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)
Pierre Letouzey
2016-07-03
*
|
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
|
Separate flags for fix/cofix/match reduction and clean reduction function names.
Maxime Dénès
2016-07-01
*
|
A mini-optimization for free in unification.ml: test in O(1)
Hugo Herbelin
2016-06-10
*
|
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
*
|
Splitting Evarutil in two distinct files.
Pierre-Marie Pédrot
2016-03-20
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-20
|
\
|
|
*
Fix #4623: set tactic too weak with universes (regression)
Maxime Dénès
2016-03-17
|
*
Try eta-expansion of records only on non-recursive ones
Matthieu Sozeau
2016-03-15
*
|
Try eta-expansion of records only on non-recursive ones
Matthieu Sozeau
2016-03-14
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-09
|
\
|
|
*
Fix strategy of Keyed Unification
Matthieu Sozeau
2016-03-09
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-05
|
\
|
|
*
Fix part of bug #4533: respect declared global transparency of
Matthieu Sozeau
2016-02-23
*
|
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
|
|
/
|
/
|
|
*
Optimizing the computation of frozen evars.
Pierre-Marie Pédrot
2016-02-03
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-13
|
\
|
|
*
Extend last commit: keyed unification uses full conversions on the applied co...
Matthieu Sozeau
2016-01-12
|
*
Fix essential bug in new Keyed Unification mode reported by R. Krebbers.
Matthieu Sozeau
2016-01-12
*
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
[prev]
[next]
Pierre-Marie Pédrot
Matthieu Sozeau
Matthieu Sozeau
Maxime Dénès
Hugo Herbelin
Paul Steckler
Matej Kosik
Matej Kosik
Emilio Jesus Gallego Arias
Pierre Letouzey