aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/dp/dp_simplify.ml
Commit message (Expand)AuthorAge
* 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
* Gestion du forall et envoie d'axiome à la procédureGravatar coq2005-04-21
* dp: traitement des definitionsGravatar coq2005-04-07
* 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