index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
Commit message (
Expand
)
Author
Age
*
Divers; restructuration des points d'entrée de Constrintern
herbelin
2005-12-21
*
Restructuration des points d'entrée de Pretyping et Constrintern
herbelin
2005-12-21
*
Abandon gestion des extensions de syntaxe de la v7 et du traducteur dans meta...
herbelin
2005-12-20
*
Suppression de la mise en boite automatique si format utilisateur
herbelin
2005-12-19
*
Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...
herbelin
2005-12-17
*
Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...
herbelin
2005-12-17
*
Orthographe de 'instantiate'
herbelin
2005-12-17
*
Changement des named_context
gregoire
2005-12-02
*
bug de coqide sous windows (bad file descriptor)
barras
2005-11-23
*
bug #909: Top n'est cree que si le contexte est vide
barras
2005-11-23
*
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-11-08
*
- debugging og "Show Intros": no line breaking + fresh ids
coq
2005-11-08
*
Point-virgule manquant ligne 914 détecté par nouveau warning X de ocaml 3.09
herbelin
2005-11-04
*
Types inductifs parametriques
mohring
2005-11-02
*
No parentheses around f in 'f \subst{...}'
herbelin
2005-05-26
*
Utilisation du module Buffer; encodage plus rigoureux des symboles en uri
herbelin
2005-05-26
*
Patch to avoid Whelp bug removed.
sacerdot
2005-05-26
*
New command: "Print Ltac qualid" to print user defined tactics.
sacerdot
2005-05-20
*
Interface vers outil de recherche Whelp
herbelin
2005-05-20
*
Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...
herbelin
2005-05-17
*
Globalisation des Tactic Notation
herbelin
2005-05-15
*
Implementation of a new backtracking system, that allow to go back
coq
2005-04-20
*
Ajout récursif du répertoire COQLIB/user-contrib au chemin de chargement
herbelin
2005-03-11
*
Code mort
herbelin
2005-03-01
*
Keep ClosedSection marker for reset
herbelin
2005-02-20
*
Renaming Print Canonical Structure into Print Canonical Projections
herbelin
2005-02-18
*
Moving centralised discharge into dispatched discharge_function; required to ...
herbelin
2005-02-18
*
Moving centralised discharge into dispatched discharge_function; required to ...
herbelin
2005-02-18
*
Moving centralised discharge into dispatched discharge_function; required to ...
herbelin
2005-02-18
*
Moving centralised discharge into dispatched discharge_function; required to ...
herbelin
2005-02-18
*
Ajout Print Canonical Structures
herbelin
2005-02-12
*
Nettoyage et documentation de Library
herbelin
2005-02-06
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
Ajout de la syntaxe du reset label: "BackTo n".
coq
2005-01-14
*
Affichage numéro de l'état de la commande courante pour mode emacs
herbelin
2005-01-14
*
- Module/Declare Module syntax made more uniform:
sacerdot
2005-01-06
*
HUGE COMMIT
sacerdot
2005-01-03
*
Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...
herbelin
2005-01-02
*
Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...
herbelin
2005-01-02
*
Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...
herbelin
2005-01-02
*
Rétablissement d'un vrai Eval sous le contexte des définitions, pas un qui ...
herbelin
2004-12-30
*
Amélioration message localisation constructions et modules
herbelin
2004-12-09
*
Bug (cf #892)
herbelin
2004-12-06
*
Amélioration message d'erreur v8
herbelin
2004-12-03
*
Complétion commit précédent
herbelin
2004-11-29
*
Réduire pour trouver l'arité d'une classe
herbelin
2004-11-26
*
Correction bug Notation: il faut re-déclarer les règles de parsing des nota...
herbelin
2004-11-22
*
compatibility with POWERPC
gregoire
2004-11-22
*
Fusion OBJDEF et OBJDEF1 et renommage en CANONICAL-STRUCTUIRE
herbelin
2004-11-19
[next]