coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Getting rid of dynamic hacks in Setoid_newring.	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
\| *	Adding a target report to test-suite's Makefile to get a short summary.	Hugo Herbelin	2015-12-02
\| *	Slight simplification of code for pat/constr.	Hugo Herbelin	2015-12-02
\| *	Improving syntax of pat/constr introduction pattern so that	Hugo Herbelin	2015-12-02
\| *	Dead code from August 2014 in apply in.	Hugo Herbelin	2015-12-02
\| *	Update history of revisions.	Hugo Herbelin	2015-12-02
\| *	Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.	Hugo Herbelin	2015-12-02
\| *	Univs/Program: update the universe context with global universe	Matthieu Sozeau	2015-12-02
\| *	Fix bug #4444: Next Obligation performed after a Section opening was	Matthieu Sozeau	2015-12-02
\| *	Add an option to deactivate compatibility printing of primitive	Matthieu Sozeau	2015-12-02
\| *	Fix a bug in externalisation which prevented printing of projections	Matthieu Sozeau	2015-12-02
* \|	Removing dead code in Obligations.	Pierre-Marie Pédrot	2015-12-02
* \|	New algorithm for universe cycle detections.	Jacques-Henri Jourdan	2015-12-01
* \|	Remove unneeded fixpoint in normalize_context_set. Note that it is no	Matthieu Sozeau	2015-12-01
\| *	vio: fix argument parsing (progress on #4442)	Enrico Tassi	2015-12-01
* \|	Simplify coqdep lexer by removing global references.	Guillaume Melquiond	2015-11-30
\| *	Test for bug #4149.	Pierre-Marie Pédrot	2015-11-30
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-29
\|\\|
\| *	Test-suite files for closed bugs	Matthieu Sozeau	2015-11-28
\| *	Closed bugs.	Matthieu Sozeau	2015-11-28
\| *	Univs: correctly register universe binders for lemmas.	Matthieu Sozeau	2015-11-28
\| *	Univs: entirely disallow instantiation of polymorphic constants with	Matthieu Sozeau	2015-11-27
\| *	Avoid recording spurious Set <= Top.i constraints which are always	Matthieu Sozeau	2015-11-27
\| *	Fix [Polymorphic Hint Rewrite].	Matthieu Sozeau	2015-11-27
\| *	Fixing the "parsing rules with idents later declared as keywords" problem.	Hugo Herbelin	2015-11-26
\| *	Make the pretty printer resilient to incomplete nametab (progress on #4363).	Enrico Tassi	2015-11-26
\| *	Adding the Printing Projections options to the index.	Pierre-Marie Pédrot	2015-11-26
* \|	More efficient implementation of equality-up-to-universes in Universes.	Pierre-Marie Pédrot	2015-11-26
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-26
\|\\|
* \|	More invariants in UState.	Pierre-Marie Pédrot	2015-11-26
\| *	Fix for case-insensitive path looking continued (#2554): Adding a	Hugo Herbelin	2015-11-25
\| *	Generalizing the patch to bug #2554 on fixing path looking with	Hugo Herbelin	2015-11-25
\| *	Heuristic to check the version of lablgtk2 in configure.ml.	Pierre-Marie Pédrot	2015-11-25
\| *	Reverting 1467c225 (Fixing an old typo in Retyping, found by Matej).	Hugo Herbelin	2015-11-25
\| *	Advertising that CoqIDE requires lablgtk >= 2.16	Pierre-Marie Pédrot	2015-11-25
\| *	Checking lablgtk version in configure. Fix bug #4423.	Pierre-Marie Pédrot	2015-11-25
\| *	Univs: carry on universe substitution when defining obligations of	Matthieu Sozeau	2015-11-24
\| *	Fixing an old typo in Retyping, found by Matej.	Hugo Herbelin	2015-11-24
\| *	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
\| *	Fix output of universe arcs. (Fix bug #4422)	Guillaume Melquiond	2015-11-23
\| *	Fixing a vm_compute bug in the presence of let-ins among the	Hugo Herbelin	2015-11-22
\| *	Fixing a bug of adjust_subst_to_rel_context.	Hugo Herbelin	2015-11-22