index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
...
*
Improving tclWITHHOLES which did not see undefined evars up to
Hugo Herbelin
2014-06-13
*
Fixing "clear" in internal_cut_replace: forbid dependencies in the
Hugo Herbelin
2014-06-13
*
Improved error message when a meta posed as an evar remains unsolved
Hugo Herbelin
2014-06-13
*
Check resolution of Metas turned into Evars by pose_all_metas_as_evars
Hugo Herbelin
2014-06-13
*
Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284).
Hugo Herbelin
2014-06-13
*
Adapt simpl/cbn unfolding and refolding machinery to projections, so that
Matthieu Sozeau
2014-06-13
*
Code cleaning in Univ.
Pierre-Marie Pédrot
2014-06-12
*
Passing some tactics to the new monad type.
Pierre-Marie Pédrot
2014-06-12
*
Fix bug #3291, stack overflow in rewrite.
Matthieu Sozeau
2014-06-11
*
Fix bug #3289
Matthieu Sozeau
2014-06-11
*
Move bug # 3368 to closed bugs
Matthieu Sozeau
2014-06-11
*
Merge branch 'more-test-suite' of https://github.com/JasonGross/coq into trunk
Matthieu Sozeau
2014-06-11
|
\
*
|
- Fix bug #3368, due to wrong use of the Cst_stack for projections.
Matthieu Sozeau
2014-06-11
*
|
In generalized rewrite, avoid retyping completely and constantly the conclusi...
Matthieu Sozeau
2014-06-11
*
|
fix handling of side effects in abstract (fixes QArithSternBrocot)
Enrico Tassi
2014-06-11
|
*
Add many more cases to the test-suite
Jason Gross
2014-06-10
|
*
Move closed bug 3314
Jason Gross
2014-06-10
|
*
Add a test-case for bug #3314 proving False
Jason Gross
2014-06-10
|
/
*
Fixing Sorting Universes in a world where le and lt constraints may be
Pierre-Marie Pédrot
2014-06-10
*
Compute the trace of a universe inconsistency only when explicitly required
Pierre-Marie Pédrot
2014-06-10
*
Made explanations for universe inconsistencies optional. They are only used
Pierre-Marie Pédrot
2014-06-10
*
Specialize the type of [Univ.compare_neq] so that it is clear it is only used
Pierre-Marie Pédrot
2014-06-10
*
Removing dead code in checker/univ.ml.
Pierre-Marie Pédrot
2014-06-10
*
Removing explanations of universe inconsistencies from the checker. They
Pierre-Marie Pédrot
2014-06-10
*
Imperatively check touched universes in compare_neq functions. This ensures
Pierre-Marie Pédrot
2014-06-10
*
Providing the checker with its own version of the Univ file.
Pierre-Marie Pédrot
2014-06-10
*
- Fix substitution of universes which needlessly hashconsed existing universes.
Matthieu Sozeau
2014-06-10
*
Oops, one refactoring was not compiled.
Matthieu Sozeau
2014-06-10
*
More cleanup/reorganizing of univ.ml to separate constraint/universe handling...
Matthieu Sozeau
2014-06-10
*
Fix module order in printers.mllib
Matthieu Sozeau
2014-06-10
*
Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...
Matthieu Sozeau
2014-06-10
*
Remove unused function in univ
Matthieu Sozeau
2014-06-10
*
Merge branch 'hott-test-suite-progress' of https://github.com/JasonGross/coq ...
Matthieu Sozeau
2014-06-10
|
\
*
|
Flattening Level module structure in Univ.
Pierre-Marie Pédrot
2014-06-09
|
*
Mark some progress in the HoTT/coq test-suite
Jason Gross
2014-06-08
*
|
Adding a toplevel option allowing to deactivate the term sharing in kernel
Pierre-Marie Pédrot
2014-06-08
|
/
*
Moving hook code from Future to Lemmas. This seemed to disrupt compilation of
Pierre-Marie Pédrot
2014-06-08
*
Fix canonical structure resolution in unification (bug found in Ssreflect).
Matthieu Sozeau
2014-06-08
*
Timeout implementation for Windows based on threads.
Pierre-Marie Pédrot
2014-06-08
*
Enforce a correct exception handling in declaration_hooks
Enrico Tassi
2014-06-08
*
ind_tables: always declare side effects (Closes: HOTT#110)
Enrico Tassi
2014-06-08
*
STM: handle "Time Abort" correctly (Closes: 3332)
Enrico Tassi
2014-06-08
*
Function in Univ uselessly exported.
Pierre-Marie Pédrot
2014-06-08
*
Removing 'open Univ' from checker.
Pierre-Marie Pédrot
2014-06-07
*
Moving a Thread.yield in check_interrupt.
Pierre-Marie Pédrot
2014-06-07
*
Adding a new Control file centralizing the control options of Coq.
Pierre-Marie Pédrot
2014-06-07
*
Preserve compatibility on examples such as "intros []." on goals such
Hugo Herbelin
2014-06-06
*
Dead code.
Hugo Herbelin
2014-06-06
*
Fixes the lost evars when interpreting a change with pattern tactic.
Arnaud Spiwack
2014-06-06
*
Remove the syntax [Vernac1. Vernac2. … Vernacn. ].
Arnaud Spiwack
2014-06-06
[prev]
[next]