coq/contrib/extraction/test/extract, branch master The formal proof system Deletion of contrib/extraction/test 2007-07-12T21:48:26+00:00 letouzey 2007-07-12T21:48:26+00:00 c605392e81dccf2f99c43db538d6ceb4b9759e90 Not maintained, probably broken, of no interest except (maybe) for myself, bad interaction with tools that work recursively (coqdep). ===> I move it to a personal repository git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9986 85f007b7-540e-0410-9357-904b9bb8a0f7 
Not maintained, probably broken, of no interest except (maybe) for
myself, bad interaction with tools that work recursively (coqdep).
===> I move it to a personal repository



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9986 85f007b7-540e-0410-9357-904b9bb8a0f7
BIG MAJ Extraction: 2003-04-16T23:27:41+00:00 letouzey 2003-04-16T23:27:41+00:00 4478577ca03d71742f954783d57b015f8d87f031 ------------------ - (Recursive) Extraction Module devient (Recursive) Extraction Library (pour cause d'ambiguite avec les nouveaux modules Coq). - un nouveau Extraction Module qui extrait dans le toplevel tout module Coq - tout fixpoint est de nouveau inlinable (Yves). - fix bug du calcul d'env minimal des modules en extraction monolithique. - un nouveau fichier Modutil regroupant manques de Modops & functions specifiques aux modules MiniML - plus d'aliases a trainer (mais des substitutions des le depart) - ET SURTOUT: un nommage correct (ou du moins moins pire) dans les modtypes et les functors. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3934 85f007b7-540e-0410-9357-904b9bb8a0f7 
------------------
- (Recursive) Extraction Module devient (Recursive) Extraction Library
  (pour cause d'ambiguite avec les nouveaux modules Coq).
- un nouveau Extraction Module qui extrait dans le toplevel tout module Coq
- tout fixpoint est de nouveau inlinable (Yves).
- fix bug du calcul d'env minimal des modules en extraction monolithique.
- un nouveau fichier Modutil regroupant manques de Modops & functions
  specifiques aux modules MiniML
- plus d'aliases a trainer (mais des substitutions des le depart)
- ET SURTOUT: un nommage correct (ou du moins moins pire) dans les modtypes
  et les functors.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3934 85f007b7-540e-0410-9357-904b9bb8a0f7
changement du test extraction suite aux modif inining 2002-03-21T11:57:23+00:00 letouzey 2002-03-21T11:57:23+00:00 3e61324e81b69f7466a24610fcf4a2ccbe82a6d5 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2556 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2556 85f007b7-540e-0410-9357-904b9bb8a0f7
refonte du test 2001-11-05T17:20:41+00:00 letouzey 2001-11-05T17:20:41+00:00 8cd83fb8dd41521bbc109d37dd49dd3aae0de373 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2162 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2162 85f007b7-540e-0410-9357-904b9bb8a0f7
Remaniement Makefile de test. make reals possible 2001-04-23T11:15:59+00:00 letouzey 2001-04-23T11:15:59+00:00 6a05d25e60d645f6af4ed7f89f6bd22bcf129c9f git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1661 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1661 85f007b7-540e-0410-9357-904b9bb8a0f7
blindage False_rec 2001-04-19T15:07:41+00:00 filliatr 2001-04-19T15:07:41+00:00 8a009c8729dd6905dd7d47877b444fa38dd2e221 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1634 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1634 85f007b7-540e-0410-9357-904b9bb8a0f7
modifs des scripts de test auto 2001-04-19T12:45:22+00:00 filliatr 2001-04-19T12:45:22+00:00 9dffee324277ac229634e9f21e3f46694ec61ca8 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1621 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1621 85f007b7-540e-0410-9357-904b9bb8a0f7
script de bench automatique pour extraction 2001-04-19T12:15:09+00:00 letouzey 2001-04-19T12:15:09+00:00 1f009ebf50eb1e697698b5ca95bdbdda56cee8f9 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1615 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1615 85f007b7-540e-0410-9357-904b9bb8a0f7