coq/contrib/extraction, branch master

Directory 'contrib' renamed into 'plugins', to end confusion with archive of user contribs

2009-03-20T01:22:58+00:00

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

Makefile: ml dependencies of contribs are moved to .mllib files

2009-03-14T11:29:46+00:00

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

extraction: update of README+CHANGES, rm of BUGS+TODO

2009-02-27T17:04:45+00:00

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

pushed evar reduction in kernel

2009-02-06T21:25:52+00:00

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

Petit nettoyage faisant suite au commit #11847 .

2009-01-23T14:47:07+00:00

Quelques modifications autour (géographiquement) de Util.list_split_at

Util.list_split_at devient Util.list_split_when (dénomination inventée
arbitrairement par moi-même, mais qui ne devrait pas déranger grand
monde vu qu'il semble n'y avoir que deux occurences de cette fonction).
Pour laisser la place à la fonction suivante :

Introduction de Util.list_split_at: qui sépare la liste à une position
donnée (alors que la nouvellement nommé list_split_when sépare à la 
première occurence "vrai" d'un prédicat).                            

Ajout de quelques commentaires dans util.ml (pas le mli) sur ces deux 
fonctions.

Suppression de Impargs.list_split_at (appel à Util).   

Suppression de Subtac_pretyping.list_split_at (qui était du code mort de 
toute façon).

Suppression Util.list_split_by qui n'est utilisé nulle part et est une 
réimplémentation de List.partition (qui est probablement meilleure, en 
particulier tail-recursive)



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

Fix #2011 : an incorrect environment when extracting Module ... with ...

2009-01-22T18:56:41+00:00

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

Extraction Library works now when some files share the same short name (fix #2025)

2009-01-22T16:40:26+00:00

 For instance, when we need to extract Init.Wf and Program.Wf,
 the first one gives wf.ml and the second wf0.ml.

 This name resolution mechanism is merged with the handling of the
 extraction filename blacklist. Hence, after Extraction Blacklist Foo,
 the coq file Foo.v will now be extracted as foo0.ml (instead of
 coq_Foo.ml as previously).

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

Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->

2008-12-31T10:57:09+00:00

splay_prod_n, lam_it -> it_mkLambda, splay_lambda -> splay_lam). Added
shortcuts for "fst (decompose_prod t)" and co.




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

Avoid printing that extraction has created file Foo when it's not the case

2008-12-17T16:53:39+00:00

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

Extraction Blacklist : a new command for avoiding conflicts with existing files

2008-12-16T19:07:09+00:00

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