index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
Commit message (
Expand
)
Author
Age
*
Merge PR#508: Optimize pending evars
Maxime Dénès
2017-04-06
|
\
*
|
Replacing "cast surgery" in LetIn by a proper field (see PR #404).
Hugo Herbelin
2017-03-24
|
*
Better algorithm for Evarconv.max_undefined_with_candidates.
Pierre-Marie Pédrot
2017-03-24
*
|
Merge branch 'v8.6' into trunk
Maxime Dénès
2017-03-23
|
\
\
|
*
|
Intern names bound in match patterns
Tej Chajed
2017-03-23
|
|
*
Make the computation of frozen evars lazy in Pretyping.
Pierre-Marie Pédrot
2017-03-23
|
|
*
Fast path in computation of frozen evars in Pretyping.
Pierre-Marie Pédrot
2017-03-23
|
|
*
Ensuring static invariants about handling of pending evars in Pretyping.
Pierre-Marie Pédrot
2017-03-23
|
|
/
|
/
|
*
|
Merge PR#437: Improve unification debug trace.
Maxime Dénès
2017-03-17
|
\
\
*
\
\
Merge PR#393: Replace Typeops with Fast_typeops
Maxime Dénès
2017-02-08
|
\
\
\
*
\
\
\
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-02-01
|
\
\
\
\
|
|
|
_
|
/
|
|
/
|
|
*
|
|
|
Adding a new evar source to remember the name of evars which were
Hugo Herbelin
2017-01-22
|
*
|
|
Fixing bugs in typing "match" (regressions #5322 and #5324 + bugs with let-ins).
Hugo Herbelin
2017-01-22
|
|
|
*
Improve unification debug trace.
Théo Zimmermann
2016-12-13
|
|
_
|
/
|
/
|
|
|
|
*
Replace Typeops by Fast_typeops
Gaetan Gilbert
2016-12-12
|
|
/
|
/
|
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-12-07
|
\
|
|
*
Merge remote-tracking branch 'github/pr/366' into v8.6
Maxime Dénès
2016-12-04
|
|
\
|
|
*
Document changes
Matthieu Sozeau
2016-12-02
|
*
|
Univs: fix bug #5180
Matthieu Sozeau
2016-11-30
|
|
*
Fix UGraph.check_eq!
Matthieu Sozeau
2016-11-30
|
|
/
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-11-18
|
\
|
|
*
Merge remote-tracking branch 'github/pr/339' into v8.6
Maxime Dénès
2016-11-07
|
|
\
|
*
\
Merge commit 'e6edb33' into v8.6
Maxime Dénès
2016-11-07
|
|
\
\
|
|
*
|
More explicit name for status of unification constraints.
Maxime Dénès
2016-11-07
|
|
|
*
Lets Hints/Instances take an optional pattern
Matthieu Sozeau
2016-11-03
*
|
|
|
Stronger static invariant in equality upto universes.
Pierre-Marie Pédrot
2016-10-31
*
|
|
|
Moving Universes to the engine/ folder.
Pierre-Marie Pédrot
2016-10-30
*
|
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-29
|
\
|
|
|
|
*
|
|
Fixing error localisation bug introduced in fixing #5142 (21e1d501e17c).
Hugo Herbelin
2016-10-29
|
|
|
/
|
|
/
|
|
*
|
Merge remote-tracking branch 'github/pr/337' into v8.6
Maxime Dénès
2016-10-28
|
|
\
\
|
|
*
|
Complete overhaul of the Arguments vernacular.
Maxime Dénès
2016-10-27
|
*
|
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-26
|
|
\
\
\
|
|
*
\
\
Merge remote-tracking branch 'github/pr/333' into v8.5
Maxime Dénès
2016-10-25
|
|
|
\
\
\
*
|
|
|
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-24
|
\
|
|
|
|
|
|
|
*
|
|
|
Remove incorrect assertion in cbn (bug #4822).
Guillaume Melquiond
2016-10-22
|
|
|
|
|
*
Renamings to avoid confusion deprecating old names
Matthieu Sozeau
2016-10-22
|
|
|
|
|
*
Unification constraint handling (#4763, #5149)
Matthieu Sozeau
2016-10-22
|
|
|
*
|
|
Fix a bug in error printing of unif constraints
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
|
|
*
|
A fix for #5097 (status of evars refined by "clear" in ltac: closed wrt evars).
Hugo Herbelin
2016-10-20
|
*
|
|
Attempt to improve error rendering in pattern-matching compilation (#5142).
Hugo Herbelin
2016-10-19
*
|
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-18
|
\
|
|
|
|
*
|
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-18
|
|
\
|
|
|
*
|
|
Quick fix to unification regression #4955.
Hugo Herbelin
2016-10-17
|
|
|
/
|
|
/
|
|
|
*
Fixing to #3209 (Not_found due to an occur-check cycle).
Hugo Herbelin
2016-10-17
|
|
*
Fixing a missing constraint in consider_remaining_unif_constraints.
Hugo Herbelin
2016-10-17
*
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-17
|
\
|
|
|
*
|
Completing reverting generalization and cleaning of the return clause inference.
Hugo Herbelin
2016-10-13
[next]