coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Less ambitious application of a notation for eq_rect. We proposed	herbelin	2011-08-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	"rewrite Heq in H" but "rewrite" is sometimes used by users and I don't want to have to change their file. The solution to put the notations in a module does not work with name "rewrite" because loading the module would change the status of "rewrite" from simple ident to keyword (and we cannot declare "rewrite" as an ident, as shown in previous commit). Then we come back on notation "rew" (this name is also used by some users), in a module. This continues commit r14366 and r14390 and improves on the level of the notation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14400 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New proposition "rewrite Heq in H" for eq_rect (assuming that there is	herbelin	2011-08-08
\| \| \| \| \| \|	a smaller risk that "rewrite" clashes with a name used for constr). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14390 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tentative abbreviation "rew Heq in H" for eq_rect. (feedback welcome)	herbelin	2011-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14281 85f007b7-540e-0410-9357-904b9bb8a0f7
*	As many notation for for vectors as for List.	pboutill	2011-05-03
\| \| \| \| \| \|	Tiny doc of mli-doc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14089 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Fix solve_simpl_eqn which was cheking instances types in the wrong ↵	msozeau	2011-03-23
\| \| \| \| \| \| \| \|	environment sometimes. - Remove compilation warning in classes.ml due to (as yet) unused code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13924 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Inference of match predicate produces ill-typed unification problem,	msozeau	2011-03-11
\| \| \| \| \| \| \|	revert to manual building of the predicate. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13906 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Vectors fully use implicit arguments	pboutill	2011-02-10
\| \| \| \| \| \|	and take disavantages for maximal insertion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13827 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixpoints are traverse during implicits arguments search to toplevel	pboutill	2011-02-10
\| \| \| \| \| \|	registration (& CHANGES update) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13826 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Interp a definition with the implicit arguments of its local context	pboutill	2011-02-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13825 85f007b7-540e-0410-9357-904b9bb8a0f7
*	local variables can have implicits locally	pboutill	2011-02-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13824 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Data structure telling implicits of local variables is a map in the	pboutill	2011-02-10
\| \| \| \| \| \|	intern_env git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13823 85f007b7-540e-0410-9357-904b9bb8a0f7
*	First release of Vector library.	pboutill	2010-12-10
	To avoid names&notations clashs with list, Vector shouldn't be "Import"ed but one can "Import Vector.VectorNotations." to have notations. SetoidVector at least remains to do. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13702 85f007b7-540e-0410-9357-904b9bb8a0f7