aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* Coqdoc patch for Program, fix xlate.ml warning and little subtac fixes.Gravatar msozeau2007-01-29
* "suffices" implemented + syntax cleanupGravatar corbinea2007-01-28
* Pas de solution à court terme pour ce problème de complexitéGravatar herbelin2007-01-28
* Explication du intros until nGravatar notin2007-01-26
* Contounement d'un probleme avec la VM dans Function Gravatar jforest2007-01-26
* correction d'un bug d'efficacite dans le printerGravatar jforest2007-01-26
* decl mode: anonymous factsGravatar corbinea2007-01-25
* Redondance erronée dans les testsGravatar herbelin2007-01-25
* doc de ringGravatar bgregoir2007-01-24
* modifications des messages d'erreurs renvoyés lors de la comparaison Gravatar soubiran2007-01-24
* Update some tests and fix section bug.Gravatar msozeau2007-01-24
* changement de la fonction norm_substGravatar bgregoir2007-01-24
* Tentative amélioration messages d'erreur prédicat d'élimination (cf notammentGravatar herbelin2007-01-24
* Correction bug #1333 (test non récursivité des dépendances en d'autresGravatar herbelin2007-01-24
* Updated Makefile to include ConstructiveEpsilon.vGravatar emakarov2007-01-23
* Derivation of (exists x : A, P x) -> {x : A | P x} for decidable PGravatar emakarov2007-01-23
* ring : Correction du bug PR#1306Gravatar bgregoir2007-01-23
* Correction du bug #1315:Gravatar notin2007-01-22
* Correction d'un bug d'unification-pattern dans l'algo d'unificationGravatar herbelin2007-01-22
* Allègement de l'affichage des références par le printer si possibleGravatar herbelin2007-01-22
* Clarification redondance Axiome du choix unique/descriptionGravatar herbelin2007-01-22
* changes in declarative language : by term using tacticGravatar corbinea2007-01-22
* Correction pour le rapport de bug #1325 par rétablissement duGravatar herbelin2007-01-22
* Error au lieu de anomaly si les appels à simplify, harvey, zenon, ... échouentGravatar herbelin2007-01-22
* Prise en compte des univers algébriques dans les types inférés dansGravatar herbelin2007-01-19
* Export de l'afficheur de substitutions de noms de modules pour le débogueurGravatar herbelin2007-01-19
* Protection contre les warnings 'unused variable' de ocaml 3.09Gravatar herbelin2007-01-19
* Protection contre les warnings 'unused variable' de ocaml 3.09Gravatar herbelin2007-01-19
* Tests de référence circulaire au sous-typage de module (pour mémoire)Gravatar herbelin2007-01-19
* Update installation instructions to the modern world a bit.Gravatar lmamane2007-01-18
* Update for v8.1Gravatar lmamane2007-01-18
* Move definition of VO_TOOLS_DEP before first use of it.Gravatar lmamane2007-01-17
* Reintroduce compatibility with old versions of GNU makeGravatar lmamane2007-01-17
* Correction bug #1282Gravatar herbelin2007-01-17
* Correction bug #1302Gravatar herbelin2007-01-17
* Correction adresse CoRN dans FAQ (suite)Gravatar herbelin2007-01-17
* Correction adresse CoRN dans FAQ (cf #1317)Gravatar herbelin2007-01-17
* README update:Gravatar lmamane2007-01-17
* Various subtac fixes.Gravatar msozeau2007-01-15
* Suite au mail de Lionel a propos du Makefile: Gravatar letouzey2007-01-12
* un saut de ligne ...Gravatar letouzey2007-01-12
* addition du neq unicodeGravatar letouzey2007-01-12
* Petit oubli dans commit 9474Gravatar herbelin2007-01-11
* Ajout d'une option de débogage pour expliciter l'instance des evarsGravatar herbelin2007-01-11
* - Make .vo files depend on coqdoc if COQ_XML is set (bug #848)Gravatar lmamane2007-01-10
* Merge with Lionel Elie Mamane's private branch:Gravatar lmamane2007-01-10
* Merge from Lionel Elie Mamane's private branch:Gravatar lmamane2007-01-10
* Suite commit restructuration discharge (application du type deGravatar herbelin2007-01-10
* Nouvelle approche pour le discharge modulaireGravatar herbelin2007-01-10
* Subtac fixes, support for reasoning on wf defs.Gravatar msozeau2007-01-08
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-22 07:17:40 +0000