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






MSetRBT : implementation of MSets via Red-Black trees
2012-04-13T18:00:56+00:00

letouzey

2012-04-13T18:00:56+00:00

c8ec3774d0c4c17e23609fea45f517f678ba56df

 Initial contribution by Andrew Appel, many ulterior modifications
 by myself.

 Interest: red-black trees maintain logarithmic depths as AVL,
 but they do not rely on integer height annotations as AVL,
 allowing interesting performance when computing in Coq or after
 standard extraction. More on this topic in the article by A. Appel.

 The common parts of MSetAVL and MSetRBT are shared in a new file
 MSetGenTree which include the definition of tree and functions
 such as mem fold elements compare subset.

 Note that the height of AVL trees is now the first arg of the
 Node constructor instead of the last one.

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





 Initial contribution by Andrew Appel, many ulterior modifications
 by myself.

 Interest: red-black trees maintain logarithmic depths as AVL,
 but they do not rely on integer height annotations as AVL,
 allowing interesting performance when computing in Coq or after
 standard extraction. More on this topic in the article by A. Appel.

 The common parts of MSetAVL and MSetRBT are shared in a new file
 MSetGenTree which include the definition of tree and functions
 such as mem fold elements compare subset.

 Note that the height of AVL trees is now the first arg of the
 Node constructor instead of the last one.

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







FSetPositive: sets of positive inspired by FMapPositive.
2010-07-16T15:50:16+00:00

letouzey

2010-07-16T15:50:16+00:00

8bc0c8675a30eb54b6f9af5c19a6279de011c1ed

 Contributed by Alexandre Ren, Damien Pous, and Thomas Braibant.

 I've also included a MSets version, hence FSetPositive might become
 soon a mere wrapper for MSetPositive, as for other FSets
 implementations.

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





 Contributed by Alexandre Ren, Damien Pous, and Thomas Braibant.

 I've also included a MSets version, hence FSetPositive might become
 soon a mere wrapper for MSetPositive, as for other FSets
 implementations.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13287 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