aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Expand)Author
2006-10-04inefficacite de field_simplify_eqbarras
2006-10-04Correction bug #1211notin
2006-10-03Détection ocaml 3.09 des variables non utilisées (trop peu pour solliciter ...herbelin
2006-10-02bug dans field_simplifybarras
2006-10-01Une passe sur l'injection et la discrimination...herbelin
2006-09-29args implicites dans Fieldbarras
2006-09-29git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9188 85f007b7-540e-04...barras
2006-09-28separation de RealFieldbarras
2006-09-28git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9185 85f007b7-540e-04...barras
2006-09-28Add dependent list combinators test.msozeau
2006-09-27Detection des paramettres pour les Functions bien fondeesjforest
2006-09-26petits pbs de dependancesbarras
2006-09-26Compilation newringnotin
2006-09-26commit de field + renommagesbarras
2006-09-26mise a jour du nouveau ring et ajout du nouveau field, avant renommagesbarras
2006-09-20Declarative Proof Language: main commitcorbinea
2006-09-19Gestion des arguments implicites dans les Functions bien fondeesjforest
2006-09-19added congruence improvementcorbinea
2006-09-18correction of bug #1220jforest
2006-09-16Message modification in Functionjforest
2006-09-15Minor bug correction in well-founded Function.jforest
2006-09-15Report de l'heuristique d'unification premier ordre flexible/rigideherbelin
2006-09-14mise en conformite des messages d'erreur de Function avec la doc.jforest
2006-09-04Fix wrong order for building library, add informative messages.msozeau
2006-09-01New handling of obligations.msozeau
2006-09-01Forgot to add this one.msozeau
2006-09-01Subtac fixes, new way of handling obligations in progress.msozeau
2006-09-01Suite commit 9110 (uniformisation position notation dans les blocs inductifs)herbelin
2006-09-01Ajout possibilité clause "where" dans co-points fixes herbelin
2006-08-25two minor bug corrections in General Recursive Functions jforest
2006-08-24Amelioration des messages d'erreur de Fucntion jforest
2006-08-22making otags working jforest
2006-08-22+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and nojforest
2006-08-16+ timide essai pour le traitement des as dans les patterns lors de la generat...jforest
2006-08-15working on functional induction automation (tactic finduction andcourtieu
2006-08-11Bug corrections in Function.jforest
2006-08-08In the old version, recursive functions cannot be declared inside a sectionbertot
2006-07-18Correction bug #1192notin
2006-07-18Code cleaning in Functionjforest
2006-07-18Code cleaning in Functionjforest
2006-07-13bug correction when defining graph of fixpoints/definitions not generated by ...jforest
2006-07-11Ajout de quelques Arguments Scope pour simuler la récursivité du scope rome...herbelin
2006-07-10+functional inversion now takes the function to invert as an optional argument. jforest
2006-07-07Correction bug 1172 + correction en passant de la taille des paramètres de f...herbelin
2006-07-06Suite remplacement VernacDebug par VernacSetOptionherbelin
2006-07-05Use typing informations while defining graphs for Function. jforest
2006-07-04functional inversion now takes a quatified hypothesis as first argumentjforest
2006-07-04adding comments and cleaning code jforest
2006-07-04- completely new version of "functional inversion" using inversion onjforest
2006-07-03Extension des motifs disjonctifs au cas de disjonction de motifs multiplesherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 15:43:43 +0000