aboutsummaryrefslogtreecommitdiff
path: root/contrib/dp
AgeCommit message (Collapse)Author
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵letouzey
user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-14Makefile: ml dependencies of contribs are moved to .mllib filesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11977 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-19Nettoyage des variables Coq et amélioration de coqmktop. Lesnotin
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
2008-12-10Bug in 11662 (did not notice that dp_zenon.mll should be modified instead of herbelin
dp_zenon.ml) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11663 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-09-10profondeur maximalefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11395 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-13debug et nouvelles commandes Dp_prelude et Dp_predefinedfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10924 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-22Test que la bibliothèque ZArith est chargée lors d'un appel à simplify, ↵notin
ergo, etc. (cf bug #1831) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10832 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-17tactique gappafilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10810 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-16flottantsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10804 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-01Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientherbelin
pas correctes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10739 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-19tactique gappafilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10696 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-14tactique gappafilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10663 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-11tactique Gappa : mise en placefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10655 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-08Prise en compte des notations "alias" dans la globalisation des coercions.herbelin
Au passage, un peu plus de standardisation des noms de fonctions de globalisation Principe de base : locate_foo : qualid -> foo (échoue avec Not_found) global : reference -> global_reference (échoue avec UserError) global_of_foo : foo -> global_reference (échoue avec UserError) f_with_alias : se comporte comme f mais prenant aussi en compte les notations de la forme "Notation id:=ref" Principale exception : locate, au lieu de locate_global locate_global_with_alias, qui prend en entrée un "qualid located" Restent beaucoup de fonctions qui pourraient utiliser global_with_alias au lieu de global, notamment dans contribs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10305 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-06bugs dpfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10293 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-20traces Ergofilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9720 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-14encodage des typesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9646 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-14tactique yicesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9645 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-22Error au lieu de anomaly si les appels à simplify, harvey, zenon, ... échouentherbelin
(particulièrement intéressant pour simplify du fait de sa proximité avec simpl) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9508 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-21typo malencontreusefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9458 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-15contrib/dp: tactique ergo (voir ergo.lri.fr)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9453 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-08contrib/dpfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9418 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵notin
'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-27appel Zenon sans preludefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8664 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-02tactic haRVey pour appeler haRVey (contrib/dp)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8110 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-01appel de Zenonfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8106 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-28*** empty log message ***filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8103 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-27dp: sortie Whyfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8099 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
et d'"externalisation"; standardisation du nom des fonctions d'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des ↵herbelin
G_*new en G_*.ml + autres petites modifications liées à suppression du traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7740 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-24Dp: ajout d'abstraction aux applications de fonction non premier ordrecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7166 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-24dp: ajout des prédicats de sortescoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7165 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-15Dp : ajoût des existentielscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7144 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-09dp: traitement des fixpointscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7130 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-08traitement des casecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7126 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-24dp: ajout du prouveur Zenoncoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7066 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-20Adoption du nom canonique global_of_constr pour éviter confusion avec type ↵herbelin
reference git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7052 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-21Gestion du forall et envoie d'axiome à la procédurecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6950 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-07dp: traitement des definitionscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6919 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-05Problemes de renommage reglescoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6914 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-24symboles de fonctions globaux traitescoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6882 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-22Ajout de l'axiome du but prouve par la tactique simplificoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6875 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-18appel de Simplify depuis Coqcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6854 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-16tactiques prouveurs premier ordre dans contrib/dp/coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6842 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-16nouvelles tactiques pour appeler des procedures de decision du premier ordrecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6841 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-20 20:23:49 +0000