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
...
*
|
proof mode: print unification constraints
Matthieu Sozeau
2016-06-16
*
|
Tentative fix of test-suite file to avoid loop
Matthieu Sozeau
2016-06-16
*
|
Typeclasses:rename solve_instantiation* & use Hook
Matthieu Sozeau
2016-06-16
*
|
Fix resolve_one_typeclass to use the new engine
Matthieu Sozeau
2016-06-16
*
|
Bind resolve_one_typeclass to 8.5 or 8.6 resolution
Matthieu Sozeau
2016-06-16
*
|
Fix wrong tabulation in CHANGES
Matthieu Sozeau
2016-06-16
*
|
Put autoapply back, lost during rebase
Matthieu Sozeau
2016-06-16
*
|
Cleanup and refactoring
Matthieu Sozeau
2016-06-16
*
|
Document new Hint Mode option.
Matthieu Sozeau
2016-06-16
*
|
Extend Hint Mode to handle the no-head-evar case
Matthieu Sozeau
2016-06-16
*
|
Revise syntax of Hint Cut
Matthieu Sozeau
2016-06-16
*
|
Example given at DeepSpec workshop
Matthieu Sozeau
2016-06-16
*
|
Purely refactoring and code/API cleanup.
Matthieu Sozeau
2016-06-16
*
|
eauto: fix test-suite file
Matthieu Sozeau
2016-06-16
*
|
bteauto: a Proofview.tactic for multiple goals
Matthieu Sozeau
2016-06-16
*
|
Typeclasses: allow shelved subgoals
Matthieu Sozeau
2016-06-16
*
|
Minor cleanup
Matthieu Sozeau
2016-06-16
*
|
Typeclasses: refine the eauto tactic
Matthieu Sozeau
2016-06-16
*
|
Typeclasses: verbosity and Limit Intros options
Matthieu Sozeau
2016-06-16
*
|
Proofview: extensions for backtracking eauto
Matthieu Sozeau
2016-06-16
*
|
typeclass resolution: add two compatibility options
Matthieu Sozeau
2016-06-16
*
|
setoid_rewrite: fix the Params resolution tactic
Matthieu Sozeau
2016-06-16
*
|
Fix incorrect caching of local hints w.r.t sections
Matthieu Sozeau
2016-06-16
*
|
Compat with ocaml 4.01
Matthieu Sozeau
2016-06-16
*
|
Fix iterative deepening strategy failing too early
Matthieu Sozeau
2016-06-16
*
|
Implement limited proof search and iterative deepening.
Matthieu Sozeau
2016-06-16
*
|
Typeclasses eauto based on new proof engine,
Matthieu Sozeau
2016-06-16
*
|
Typeclasses: stdlib fixes for new search algorithm
Matthieu Sozeau
2016-06-16
*
|
Refine 9cc95f5, unification of Let-In's, bug #3929
Matthieu Sozeau
2016-06-16
*
|
Small factorization in the typing flags of the kernel.
Pierre-Marie Pédrot
2016-06-16
|
\
\
|
*
|
Factorizing the uses of Declareops.safe_flags.
Pierre-Marie Pédrot
2016-06-16
|
*
|
Adding a default safe set of kernel typing flags to Declareops.
Pierre-Marie Pédrot
2016-06-16
|
/
/
*
|
Fixing a mispelling coma -> comma.
Hugo Herbelin
2016-06-16
*
|
Typo in comment.
Hugo Herbelin
2016-06-16
*
|
Fixing space in an error message.
Hugo Herbelin
2016-06-16
*
|
Fixing printing of Register retroknowledge.
Hugo Herbelin
2016-06-16
*
|
Fixing Add Parametric Relation by adding printer for binders.
Hugo Herbelin
2016-06-16
*
|
Adding printers for ring and field commands.
Hugo Herbelin
2016-06-16
*
|
Fixing printing of Function.
Hugo Herbelin
2016-06-16
*
|
Isolating and exporting a function for printing body of a recursive definition.
Hugo Herbelin
2016-06-16
*
|
Simplification in ppvernac.ml.
Hugo Herbelin
2016-06-16
*
|
Removing unused generalization of pr_vernac over pr_constr and pr_lconstr.
Hugo Herbelin
2016-06-16
*
|
Fixing extra space in printing bullets.
Hugo Herbelin
2016-06-16
*
|
Fixing space in printing <+ and <: + fixing missing Inline keyword.
Hugo Herbelin
2016-06-16
*
|
Fixing printing of Instance.
Hugo Herbelin
2016-06-16
*
|
Fixing extra space in printing abbreviations (SyntaxDefinition).
Hugo Herbelin
2016-06-16
*
|
Fixing printing of Polymorphic/Monomorphic.
Hugo Herbelin
2016-06-16
*
|
Fixing printing of Arguments.
Hugo Herbelin
2016-06-16
*
|
Printing notations as parsed.
Hugo Herbelin
2016-06-16
*
|
So as to beautify to work, do not use notations in Inductive types
Hugo Herbelin
2016-06-16
[prev]
[next]