aboutsummaryrefslogtreecommitdiff
path: root/contrib/dp/dp_simplify.ml
AgeCommit message (Expand)Author
2006-12-08contrib/dpfilliatr
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-04-21Gestion du forall et envoie d'axiome à la procédurecoq
2005-04-07dp: traitement des definitionscoq
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