aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2006-08-24Amelioration des messages d'erreur de Fucntion jforest
2006-08-24MAJ biblioherbelin
2006-08-24MAJ JMeq sur Type + typos (sur propositions de Pierre Castéran)herbelin
2006-08-24MAJ biblioherbelin
2006-08-24JMeq maintenant applicable sur Typeherbelin
2006-08-23Bug in replace tactics introduced in r9073 (overlap between replace .. with a...jforest
2006-08-22making otags working jforest
2006-08-22Forgot a file in previous commit jforest
2006-08-22+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and nojforest
2006-08-22remove an orphan comment (attached to a piece of code that was removed).bertot
2006-08-17Checks that abstract setoid rings can be defined in a module and the tacticbertot
2006-08-17corrects an error in the substitution of module paths inside tactics:bertot
2006-08-16+ timide essai pour le traitement des as dans les patterns lors de la generat...jforest
2006-08-16MAJ Rectutorial (P. Castéran)notin
2006-08-15working on functional induction automation (tactic finduction andcourtieu
2006-08-14comparison functions should be Defined not Qedletouzey
2006-08-11Bug corrections in Function.jforest
2006-08-08In the old version, recursive functions cannot be declared inside a sectionbertot
2006-07-28Modifications dans les scripts de configuration (coqtop et coqide affichent m...notin
2006-07-28MAJ de la biblio du manuel de référencenotin
2006-07-28Reparation bug Show intros: les hypothèses introduites précédemmentcourtieu
2006-07-27Correction du bug #1170: les options synchronisées déclarées dans une sect...notin
2006-07-26Modification script sed pour compatibilité Windowsnotin
2006-07-22- Ajout d'un cast vm dans la syntaxe : x <: t bgregoir
2006-07-20Correction du bug #1116 jforest
2006-07-18amelioration du comportement de induction (retour a la version V8.0)jforest
2006-07-18Correction bug #1192notin
2006-07-18Code cleaning in Functionjforest
2006-07-18Code cleaning in Functionjforest
2006-07-17Renommage sqtr_lem_1 (bug 1189)notin
2006-07-17MAJjforest
2006-07-13bug correction when defining graph of fixpoints/definitions not generated by ...jforest
2006-07-13Retrait du -noassert qui etait present en natif. letouzey
2006-07-13Nombre magique pour la 8.1betaherbelin
2006-07-12Documentation machine virtuelleherbelin
2006-07-12Correction incohérence parsing de %delim dans les motifsherbelin
2006-07-11Ajout de quelques Arguments Scope pour simuler la récursivité du scope Rfun...herbelin
2006-07-11Ajout de quelques Arguments Scope pour simuler la récursivité du scope rome...herbelin
2006-07-11MAJ doc/refmannotin
2006-07-11MAJherbelin
2006-07-11Documentation de lazymatch et des extensions de idtac et failherbelin
2006-07-11Utilisation du mot-clé lazymatch pour le match paresseux (à défaut d'avoir...herbelin
2006-07-10+functional inversion now takes the function to invert as an optional argument. jforest
2006-07-09Argument Scope de list déplacé dans List.vherbelin
2006-07-07Correction bug 1172 + correction en passant de la taille des paramètres de f...herbelin
2006-07-07Correction bug 1172 + correction en passant de la taille des paramètres de f...herbelin
2006-07-07MAJherbelin
2006-07-07Documentation Declare Implicit Tactic, Print Canonical Projections, ... + lé...herbelin
2006-07-07MAJ du manuel de référence (modules+fixpoints+pose proof)notin
2006-07-06Documentation Whelpherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-26 09:02:30 +0000