coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Finer-grained types for toplevel values.	Pierre-Marie Pédrot	2015-12-21
*	Removing ad-hoc interpretation rules for tactic notations and their genarg.	Pierre-Marie Pédrot	2015-12-21
*	Changing the toplevel type of the int_or_var generic type to int.	Pierre-Marie Pédrot	2015-12-21
*	Removing the now useless genarg generic argument.	Pierre-Marie Pédrot	2015-12-21
*	Using dynamic values in tactic evaluation.	Pierre-Marie Pédrot	2015-12-21
*	Tying the loop in tactic printing API.	Pierre-Marie Pédrot	2015-12-18
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-17
\|\
* \|	Getting rid of some hardwired generic arguments.	Pierre-Marie Pédrot	2015-12-17
\| *	FIx parsing of tactic "simple refine".	Maxime Dénès	2015-12-16
\| *	Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".	Guillaume Melquiond	2015-12-16
\| *	Refine tactic now shelves unifiable holes.	Pierre-Marie Pédrot	2015-12-15
\| *	Changing the order of the goals generated by unshelve.	Pierre-Marie Pédrot	2015-12-15
* \|	Granting clear_flag in injection, even legacy mode. This is possible	Hugo Herbelin	2015-12-15
* \|	More code sharing between tactic notation and genarg interpretation.	Pierre-Marie Pédrot	2015-12-13
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-11
\|\\|
\| *	Add tactic native_cast_no_check, analog to vm_cast_no_check.	Maxime Dénès	2015-12-11
\| *	Fixing a pat%constr bug. Thanks to Enrico for reporting.	Hugo Herbelin	2015-12-10
\| *	Silently ignore requests to _not_ clear something when that something cannot ...	Guillaume Melquiond	2015-12-10
\| *	Fixing parsing of the unshelve tactical.	Pierre-Marie Pédrot	2015-12-09
\| *	Adding an unshelve tactical.	Pierre-Marie Pédrot	2015-12-09
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-08
\|\\|
\| *	Fix some typos.	Guillaume Melquiond	2015-12-07
* \|	Fixing compilation with old CAMLPX versions.	Pierre-Marie Pédrot	2015-12-05
* \|	Removing redundant versions of generalize.	Hugo Herbelin	2015-12-05
* \|	Moving extended_rel_vect/extended_rel_list to the kernel.	Hugo Herbelin	2015-12-05
* \|	Experimenting removing strong normalization of the mid-statement in tactic cut.	Hugo Herbelin	2015-12-05
* \|	Moving three related small half-general half-ad-hoc utility functions	Hugo Herbelin	2015-12-05
* \|	Getting rid of some quoted tactics in Tauto.	Pierre-Marie Pédrot	2015-12-05
* \|	Getting rid of the dynamic node of the tactic AST.	Pierre-Marie Pédrot	2015-12-04
\| *	Fix in setoid_rewrite in Type: avoid the generation of a rigid universe	Matthieu Sozeau	2015-12-04
* \|	Removing the last use of valueIn in Tauto.	Pierre-Marie Pédrot	2015-12-04
* \|	Removing dynamic inclusion of constrs in tactic AST.	Pierre-Marie Pédrot	2015-12-04
* \|	Removing the globTacticIn primitive.	Pierre-Marie Pédrot	2015-12-03
* \|	Fixing Tauto compilation for older versions of OCaml.	Pierre-Marie Pédrot	2015-12-03
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-03
\|\\|
* \|	Removing the last use of tacticIn in setoid_ring.	Pierre-Marie Pédrot	2015-12-03
* \|	Removing the use of tacticIn in Tauto.	Pierre-Marie Pédrot	2015-12-03
\| *	Slight simplification of code for pat/constr.	Hugo Herbelin	2015-12-02
\| *	Dead code from August 2014 in apply in.	Hugo Herbelin	2015-12-02
* \|	Removing dead code in Obligations.	Pierre-Marie Pédrot	2015-12-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-29
\|\\|
\| *	Fix [Polymorphic Hint Rewrite].	Matthieu Sozeau	2015-11-27
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-26
\|\\|
\| *	Fix generation of equality schemes on polymorphic equality types.	Matthieu Sozeau	2015-11-23
* \|	Removing a use of old refine in Tactics.	Pierre-Marie Pédrot	2015-11-23
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-20
\|\\|
\| *	Fix bug #4429: eauto with arith: 70x performance regression in Coq 8.5.	Pierre-Marie Pédrot	2015-11-19
\| *	Fix bug #4433, removing hack on evars appearing in a pattern from a	Matthieu Sozeau	2015-11-19
\| *	Improve error message.	Maxime Dénès	2015-11-18
* \|	Inlining the only use of Clenv.connect_clenv.	Pierre-Marie Pédrot	2015-11-18