aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/dp
Commit message (Expand)AuthorAge
* Nettoyage des variables Coq et amélioration de coqmktop. LesGravatar notin2008-12-19
* Bug in 11662 (did not notice that dp_zenon.mll should be modified instead of Gravatar herbelin2008-12-10
* profondeur maximaleGravatar filliatr2008-09-10
* debug et nouvelles commandes Dp_prelude et Dp_predefinedGravatar filliatr2008-05-13
* Test que la bibliothèque ZArith est chargée lors d'un appel à simplify, er...Gravatar notin2008-04-22
* tactique gappaGravatar filliatr2008-04-17
* flottantsGravatar filliatr2008-04-16
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
* tactique gappaGravatar filliatr2008-03-19
* tactique gappaGravatar filliatr2008-03-14
* tactique Gappa : mise en placeGravatar filliatr2008-03-11
* Prise en compte des notations "alias" dans la globalisation des coercions.Gravatar herbelin2007-11-08
* bugs dpGravatar filliatr2007-11-06
* traces ErgoGravatar filliatr2007-03-20
* encodage des typesGravatar filliatr2007-02-14
* tactique yicesGravatar filliatr2007-02-14
* Error au lieu de anomaly si les appels à simplify, harvey, zenon, ... échouentGravatar herbelin2007-01-22
* typo malencontreuseGravatar filliatr2006-12-21
* contrib/dp: tactique ergo (voir ergo.lri.fr)Gravatar filliatr2006-12-15
* contrib/dpGravatar filliatr2006-12-08
* Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...Gravatar notin2006-04-28
* appel Zenon sans preludeGravatar filliatr2006-03-27
* tactic haRVey pour appeler haRVey (contrib/dp)Gravatar filliatr2006-03-02
* appel de ZenonGravatar filliatr2006-03-01
* *** empty log message ***Gravatar filliatr2006-02-28
* dp: sortie WhyGravatar filliatr2006-02-27
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...Gravatar herbelin2005-12-26
* Dp: ajout d'abstraction aux applications de fonction non premier ordreGravatar coq2005-06-24
* dp: ajout des prédicats de sortesGravatar coq2005-06-24
* Dp : ajoût des existentielsGravatar coq2005-06-15
* dp: traitement des fixpointsGravatar coq2005-06-09
* traitement des caseGravatar coq2005-06-08
* dp: ajout du prouveur ZenonGravatar coq2005-05-24
* Adoption du nom canonique global_of_constr pour éviter confusion avec type r...Gravatar herbelin2005-05-20
* Gestion du forall et envoie d'axiome à la procédureGravatar coq2005-04-21
* dp: traitement des definitionsGravatar coq2005-04-07
* Problemes de renommage reglesGravatar coq2005-04-05
* symboles de fonctions globaux traitesGravatar coq2005-03-24
* Ajout de l'axiome du but prouve par la tactique simplifiGravatar coq2005-03-22
* appel de Simplify depuis CoqGravatar coq2005-03-18
* tactiques prouveurs premier ordre dans contrib/dp/Gravatar coq2005-03-16
* nouvelles tactiques pour appeler des procedures de decision du premier ordreGravatar coq2005-03-16