coq - The formal proof system

Age	Commit message (Expand)	Author
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	Fixing missing substitution / printing cases of TacSelect.	Pierre-Marie Pédrot
2016-06-16	Fixing parsing of constr argument of ltac functions at level 8 in the	Hugo Herbelin
2016-06-16	Fixing printing of keeping hyp on the fly.	Hugo Herbelin
2016-06-16	Fixing printing of inversion as.	Hugo Herbelin
2016-06-16	Fixing extra space in printing destruct/induction as.	Hugo Herbelin
2016-06-16	Fixing printing of induction/destruct as.	Hugo Herbelin
2016-06-16	Fixing printing of pat%constr.	Hugo Herbelin
2016-06-16	In NMake_gen, giving to tactic do_size a grammar rule which respects the levels.	Hugo Herbelin
2016-06-16	Adding option "Set Reversible Pattern Implicit" to Specif.v so that an	Hugo Herbelin
2016-06-16	Being defensive in printing implicit arguments also with manual	Hugo Herbelin
2016-06-16	A stronger invariant on the syntax of TacAssert, what allows for a	Hugo Herbelin
2016-06-16	Changing rule for "*" in Operator_Properties so that, iterated, it	Hugo Herbelin
2016-06-16	Protect the beautifier from change in the lexer state (typically by	Hugo Herbelin
2016-06-16	Not taking arguments given by name or position into account when	Hugo Herbelin
2016-06-16	Merge '/pr/206' into trunk	Enrico Tassi
2016-06-16	Merge PR #195: Complete is_* family of term-examining tactics.	Pierre-Marie Pédrot