aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et f...Gravatar herbelin2006-01-21
* Déplacement de pr_arg et pr_opt de Ppconstr vers UtilGravatar herbelin2006-01-21
* Backtrack commit précédent (incompatible avec le choix de prendre Idtac com...Gravatar herbelin2006-01-21
* Préservation énoncé exact Acc_ind par choix nom 'a' comme paramètre de AccGravatar herbelin2006-01-21
* majGravatar coq2006-01-20
* Ajout de la contrainte de résoudre l'assertion dans 'assert by'Gravatar herbelin2006-01-20
* Test bug 983Gravatar herbelin2006-01-20
* *** empty log message ***Gravatar barras2006-01-20
* majGravatar coq2006-01-19
* Conséquences supplémentaires de la fin du support v7Gravatar herbelin2006-01-19
* Export eassumptionGravatar herbelin2006-01-19
* Extended Unicode supportGravatar herbelin2006-01-19
* Correction associativité de IF et exists (visible à l'affichage uniquement ...Gravatar herbelin2006-01-19
* majGravatar coq2006-01-18
* Retrait de 'by' comme mot-clé en espérant qu'il n'y aura pas d'interférenc...Gravatar herbelin2006-01-18
* Recursive Definition now supports functions with more than one argument.Gravatar coq2006-01-18
* majGravatar coq2006-01-17
* majGravatar coq2006-01-16
* dans la liste des cmo pour dev/printers.cma, manquait proofs/tacexpr.cmoGravatar letouzey2006-01-16
* Version préliminaire d'inversion de la compilation du filtrageGravatar herbelin2006-01-16
* Ajout motif d'introduction "?" (IntroAnonymous) pour laisser CoqGravatar herbelin2006-01-16
* Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq choisir un nomGravatar herbelin2006-01-16
* *** empty log message ***Gravatar coq2006-01-16
* Code redondantGravatar herbelin2006-01-16
* Correction dans vernac_exact_proof -- jmnGravatar coq2006-01-16
* - Tactic "assert" now accepts "as" intro patterns and "by" tactic clausesGravatar herbelin2006-01-16
* cvs ci -m "Passage à la limite dans les intro-pattern de n-uplets"Gravatar herbelin2006-01-16
* majGravatar coq2006-01-15
* Ajout de nouvelles plages de symboles unicode; prise en compte des indices un...Gravatar herbelin2006-01-15
* Bug (code prévu pour iso-latin et non utf-8)Gravatar herbelin2006-01-15
* Test utf-8Gravatar herbelin2006-01-15
* majGravatar coq2006-01-14
* Code mort du traducteurGravatar herbelin2006-01-14
* majGravatar coq2006-01-13
* Correction du bug #1055Gravatar coq2006-01-13
* majGravatar coq2006-01-12
* Changing well founded induction to fix on accessibility proof in orderGravatar bertot2006-01-12
* Compatibilité prtermGravatar herbelin2006-01-12
* majGravatar coq2006-01-11
* Test conflictuel - ajouté pour mémoireGravatar herbelin2006-01-11
* Test or-patternsGravatar herbelin2006-01-11
* Ajout test notation récursiveGravatar herbelin2006-01-11
* Suppression traducteurGravatar herbelin2006-01-11
* remove warnings that were left in the directory contrib/interfaceGravatar bertot2006-01-11
* removes several warnings in contrib/interfaceGravatar bertot2006-01-11
* Résidus du traducteur v7 -> v8Gravatar herbelin2006-01-11
* Standardisation du nom de subst_raw en subst_rawconstrGravatar herbelin2006-01-11
* Suite réorganisation des fonctions d'affichageGravatar herbelin2006-01-11
* Standardisation du nom de subst_raw en subst_rawconstrGravatar herbelin2006-01-11
* Résidus du traducteur v7 -> v8Gravatar herbelin2006-01-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-14 11:24:29 +0000