coq/theories/Vectors/vo.itarget, branch master The formal proof system drop vo.itarget files and compute the corresponding the corresponding values automatically instead 2017-06-01T15:33:19+00:00 Matej Kosik 2017-03-23T11:56:24+00:00 718d61a54157733bca61ed84c0ba3761cd52720f 






Vector equalities first stuff
2012-07-20T14:22:44+00:00

pboutill

2012-07-20T14:22:44+00:00

88af5db4957e7e866ea507825ff0f08bd09c38ad

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15632 85f007b7-540e-0410-9357-904b9bb8a0f7





git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15632 85f007b7-540e-0410-9357-904b9bb8a0f7







First release of Vector library.
2010-12-10T13:22:29+00:00

pboutill

2010-12-10T13:22:29+00:00

05085e80668a4d1dedc522c6af343168870cc648

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





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