coq/theories/Lists/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 






FinFun.v: results about injective/surjective/bijective fonctions over finite domains
2014-02-07T10:50:26+00:00

Pierre Letouzey

2014-02-03T10:11:38+00:00

009fb68f0578e462b817f50772e2fba8d58c4f0d

 + Some extra results about NoDup, Fin.t, ...





 + Some extra results about NoDup, Fin.t, ...







isolate instances about Permutation and PermutationA which may slow rewrite
2012-07-10T15:38:59+00:00

letouzey

2012-07-10T15:38:59+00:00

a884f7dcebed71608f395fe140722790367089e2

 After discovering a rewrite in Ergo that takes a loooong time due
 to a bad interaction with the instances of Permutation and PermutationA :

 - PermutationA is now in a separate file SetoidPermutation
 - File Permutation.v isn't Require'd by SetoidList anymore
   nor MergeSort.v, just the definitions in Sorted.v
 - Attempt to put a priority on these instances.

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





 After discovering a rewrite in Ergo that takes a loooong time due
 to a bad interaction with the instances of Permutation and PermutationA :

 - PermutationA is now in a separate file SetoidPermutation
 - File Permutation.v isn't Require'd by SetoidList anymore
   nor MergeSort.v, just the definitions in Sorted.v
 - Attempt to put a priority on these instances.

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







Remove obsolete TheoryList
2011-02-10T18:05:09+00:00

glondu

2011-02-10T18:05:09+00:00

2d8c70b3380d899c2717d00f2f27b4c6aefa2322

This library is no longer used anywhere, and its contents is
very... let's say historical... More seriously, many (and presumably
the most useful) stuff that used to be there are in List, now.

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





This library is no longer used anywhere, and its contents is
very... let's say historical... More seriously, many (and presumably
the most useful) stuff that used to be there are in List, now.

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







Factorisation between Makefile and ocamlbuild systems : .vo to compile are in */*/vo.itarget
2009-12-09T16:45:42+00:00

letouzey

2009-12-09T16:45:42+00:00

cfc9e109a653047b7ca73224525bba67a8c3a571

 On the way: no more -fsets (yes|no) and -reals (yes|no) option of configure
  if you want a partial build, make a specific rule such as theories-light

 Beware: these vo.itarget should not contain comments. Even if this is legal
  for ocamlbuild, the $(shell cat ...) we do in Makefile can't accept that.

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





 On the way: no more -fsets (yes|no) and -reals (yes|no) option of configure
  if you want a partial build, make a specific rule such as theories-light

 Beware: these vo.itarget should not contain comments. Even if this is legal
  for ocamlbuild, the $(shell cat ...) we do in Makefile can't accept that.

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