aboutsummaryrefslogtreecommitdiff
path: root/contrib/dp
AgeCommit message (Expand)Author
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey
2009-03-14Makefile: ml dependencies of contribs are moved to .mllib filesletouzey
2008-12-19Nettoyage des variables Coq et amélioration de coqmktop. Lesnotin
2008-12-10Bug in 11662 (did not notice that dp_zenon.mll should be modified instead of herbelin
2008-09-10profondeur maximalefilliatr
2008-05-13debug et nouvelles commandes Dp_prelude et Dp_predefinedfilliatr
2008-04-22Test que la bibliothèque ZArith est chargée lors d'un appel à simplify, er...notin
2008-04-17tactique gappafilliatr
2008-04-16flottantsfilliatr
2008-04-01Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientherbelin
2008-03-19tactique gappafilliatr
2008-03-14tactique gappafilliatr
2008-03-11tactique Gappa : mise en placefilliatr
2007-11-08Prise en compte des notations "alias" dans la globalisation des coercions.herbelin
2007-11-06bugs dpfilliatr
2007-03-20traces Ergofilliatr
2007-02-14encodage des typesfilliatr
2007-02-14tactique yicesfilliatr
2007-01-22Error au lieu de anomaly si les appels à simplify, harvey, zenon, ... échouentherbelin
2006-12-21typo malencontreusefilliatr
2006-12-15contrib/dp: tactique ergo (voir ergo.lri.fr)filliatr
2006-12-08contrib/dpfilliatr
2006-04-28Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...notin
2006-03-27appel Zenon sans preludefilliatr
2006-03-02tactic haRVey pour appeler haRVey (contrib/dp)filliatr
2006-03-01appel de Zenonfilliatr
2006-02-28*** empty log message ***filliatr
2006-02-27dp: sortie Whyfilliatr
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...herbelin
2005-06-24Dp: ajout d'abstraction aux applications de fonction non premier ordrecoq
2005-06-24dp: ajout des prédicats de sortescoq
2005-06-15Dp : ajoût des existentielscoq
2005-06-09dp: traitement des fixpointscoq
2005-06-08traitement des casecoq
2005-05-24dp: ajout du prouveur Zenoncoq
2005-05-20Adoption du nom canonique global_of_constr pour éviter confusion avec type r...herbelin
2005-04-21Gestion du forall et envoie d'axiome à la procédurecoq
2005-04-07dp: traitement des definitionscoq
2005-04-05Problemes de renommage reglescoq
2005-03-24symboles de fonctions globaux traitescoq
2005-03-22Ajout de l'axiome du but prouve par la tactique simplificoq
2005-03-18appel de Simplify depuis Coqcoq
2005-03-16tactiques prouveurs premier ordre dans contrib/dp/coq
2005-03-16nouvelles tactiques pour appeler des procedures de decision du premier ordrecoq
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-20 10:16:06 +0000