coq/contrib/extraction/test/extract.haskell, branch master

Deletion of contrib/extraction/test

2007-07-12T21:48:26+00:00

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

------------------
- (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

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

Big commit extraction:

2002-03-04T15:48:51+00:00

- Changement de syntaxe (Extraction Language Toplevel/Ocaml/Haskell)
- Retour des inductifs singletons et vides dans extraction.ml
  (extraction.ml -> actions sur le type, mlutil.ml -> conserve le type)
- maintenant par defaut Recursive Extraction === Extraction "file"
- kill_prop global est fait dans extraction.ml selon typage (a suivre...)


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

suite et fin (?) de haskell: gestion des modules, mise en place du'un test

2002-02-15T13:02:06+00:00

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