coq/contrib/dp, branch master The formal proof system Directory 'contrib' renamed into 'plugins', to end confusion with archive of user contribs 2009-03-20T01:22:58+00:00 letouzey 2009-03-20T01:22:58+00:00 7d220f8b61649646692983872626d6a8042446a9 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7 
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 letouzey 2009-03-14T11:29:46+00:00 eb93dfaceccbba06f62eb92ef5e12a133c7959d4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11977 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11977 85f007b7-540e-0410-9357-904b9bb8a0f7
Nettoyage des variables Coq et amélioration de coqmktop. Les 2008-12-19T15:30:49+00:00 notin 2008-12-19T15:30:49+00:00 a81329a241ba18b8c8535576290a0ffa23739d27 principaux changements sont: - coqtop (et coqc) maintenant insensible aux variables d'environnement COQTOP, COQBIN et COQLIB; le chemin vers les librairies Coq peut être spécifié par l'option -coqlib - coqmktop prend 4 nouvelles options: -boot, -coqlib, -camlbin et -camlp4bin; en mode boot, coqmktop se réfère à Coq_config pour les chemins des exécutables OCaml; en dehors du mode boot, coqmktop cherche les exécutables OCaml dans PATH - installation des *.cmxs *.o et *.a en plus des *.cm[ioxa]; ceux-ci étant installé en copiant l'architecture des sources (ie lib.cmxa est installé dans COQLIB/lib/lib.cmxa) - coq_makefile prend maintenant 3 paramètres sous forme de variables d'environnement: COQBIN pour dire où trouver les exécutables Coq, CAMLBIN et CAMLP4BIN pour les exécutables OCaml et Camlp4/5; les chemins vers les librairies sont déduits en utilisant -where Le tout a testé avec Ssreflect (cf coq-contribs) en essayant de simuler les conditions de la vie réelle (Ocaml pas dans le PATH, installation binaire relocalisée, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11707 85f007b7-540e-0410-9357-904b9bb8a0f7 
principaux changements sont:
  - coqtop (et coqc) maintenant insensible aux variables
    d'environnement COQTOP, COQBIN et COQLIB; le chemin vers les
    librairies Coq peut être spécifié par l'option -coqlib
  - coqmktop prend 4 nouvelles options: -boot, -coqlib, -camlbin et
    -camlp4bin; en mode boot, coqmktop se réfère à Coq_config pour les
    chemins des exécutables OCaml; en dehors du mode boot, coqmktop
    cherche les exécutables OCaml dans PATH
  - installation des *.cmxs *.o et *.a en plus des *.cm[ioxa]; ceux-ci
    étant installé en copiant l'architecture des sources (ie lib.cmxa
    est installé dans COQLIB/lib/lib.cmxa)
  - coq_makefile prend maintenant 3 paramètres sous forme de variables
    d'environnement: COQBIN pour dire où trouver les exécutables Coq,
    CAMLBIN et CAMLP4BIN pour les exécutables OCaml et Camlp4/5; les
    chemins vers les librairies sont déduits en utilisant -where

Le tout a testé avec Ssreflect (cf coq-contribs) en essayant de
simuler les conditions de la vie réelle (Ocaml pas dans le PATH,
installation binaire relocalisée, ...). 




git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11707 85f007b7-540e-0410-9357-904b9bb8a0f7
Bug in 11662 (did not notice that dp_zenon.mll should be modified instead of 2008-12-10T15:16:07+00:00 herbelin 2008-12-10T15:16:07+00:00 a35f6a25dcc00b3ea15adc4715cff0f98e537005 dp_zenon.ml) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11663 85f007b7-540e-0410-9357-904b9bb8a0f7 
dp_zenon.ml)


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11663 85f007b7-540e-0410-9357-904b9bb8a0f7
profondeur maximale 2008-09-10T12:45:54+00:00 filliatr 2008-09-10T12:45:54+00:00 6f764a0a46cdeedc43be1349f5cd06d569bc45a0 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11395 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11395 85f007b7-540e-0410-9357-904b9bb8a0f7
debug et nouvelles commandes Dp_prelude et Dp_predefined 2008-05-13T14:01:11+00:00 filliatr 2008-05-13T14:01:11+00:00 a7e43bf177ae411c0c17e20d522b019741f6000c git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10924 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10924 85f007b7-540e-0410-9357-904b9bb8a0f7
Test que la bibliothèque ZArith est chargée lors d'un appel à simplify, ergo, etc. (cf bug #1831) 2008-04-22T18:02:54+00:00 notin 2008-04-22T18:02:54+00:00 076e53c0b5585a37f741bd5a3b564e43c663b22b git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10832 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10832 85f007b7-540e-0410-9357-904b9bb8a0f7
tactique gappa 2008-04-17T14:35:33+00:00 filliatr 2008-04-17T14:35:33+00:00 cde0f764b75f25526005d078e17a5ef5d52301f1 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10810 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10810 85f007b7-540e-0410-9357-904b9bb8a0f7
flottants 2008-04-16T15:03:59+00:00 filliatr 2008-04-16T15:03:59+00:00 b6b9ea6c22107a33121cb2e7f6f89ec82d1bc7d0 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10804 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10804 85f007b7-540e-0410-9357-904b9bb8a0f7
Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient 2008-04-01T14:45:20+00:00 herbelin 2008-04-01T14:45:20+00:00 124016815a5a38dfebee75451721ae13bca81959 pas correctes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10739 85f007b7-540e-0410-9357-904b9bb8a0f7 
pas correctes



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