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
...
*
Suppression StronglyClassical, StronglyConstructive devient plus concretement...
herbelin
2003-11-08
*
Branchement de Show Script sur l'afficheur structure
herbelin
2003-11-05
*
Amelioration message d'erreur
herbelin
2003-11-04
*
Pas de defaut a 1 et LeftA pour les infixes v8; fusion de l'univers et du nom...
herbelin
2003-11-01
*
Interdiction de nommer un object de nom commencant par Coq en dehors de la bi...
herbelin
2003-11-01
*
Debranchement de Print si pas verbose (necessaire pour traducteur)
herbelin
2003-11-01
*
Ajout de Print Visibility
herbelin
2003-10-28
*
Affichage Assert_failure en ocaml 3.07
herbelin
2003-10-28
*
Options -strongly-constructive et -strongly-classical
herbelin
2003-10-28
*
Independance de grammar.cmo vis a vis de Search; reorganisation VernacDefinition
herbelin
2003-10-23
*
Conjecture declare maintenant un axiome; reorganisation VernacDefinition
herbelin
2003-10-23
*
Integration de SearchNamed dans SearchAbout
herbelin
2003-10-22
*
reorganisation des niveaux (ex: = est a 70)
barras
2003-10-22
*
bug traduction de auto.(simpl). en auto.simpl.
barras
2003-10-20
*
Bug des terminaux quotés
herbelin
2003-10-17
*
oups! ca compile maintenant
barras
2003-10-16
*
translator avoids printing a . followed by a ( by inserting a space
barras
2003-10-16
*
Debranchement de l'affichage systematique des projections avec la notation po...
herbelin
2003-10-16
*
En v7 sans traducteur, une incoherence virtuelle de syntaxe V8 n'est pas une ...
herbelin
2003-10-14
*
Changement 'as notation' en 'where notation'
herbelin
2003-10-14
*
Changement 'as notation' en 'where notation'; Plus d'uniformite dans la gesti...
herbelin
2003-10-14
*
Admitted rendu independant de Conjecture: plus pratique en mode interactif
herbelin
2003-10-13
*
Bug introduit dans start_proof par le commit precedent
herbelin
2003-10-13
*
Petits bugs
herbelin
2003-10-13
*
Deplacement pr_subgoal and co vers Pfedit
herbelin
2003-10-13
*
Ajout d'une fonction de recherche sur les composantes du nom des objets
herbelin
2003-10-13
*
Protection contre les noms de lemmes existant deja
herbelin
2003-10-13
*
Deplacement pr_subgoal and co vers Pfedit; Ajout SearchNamed
herbelin
2003-10-13
*
translate_file etait abusivement positionne
herbelin
2003-10-11
*
changement nouvelle syntaxe (pt fixes)
barras
2003-10-10
*
Renommage en v8 de PolyList en List et List en MonoList
herbelin
2003-10-10
*
Nouveau format de l'option 'format'
herbelin
2003-10-09
*
Prise en compte des paramètres implicites d'inductifs pour la globalisation ...
herbelin
2003-10-08
*
Des abbreviations pour constrintern.ml
herbelin
2003-10-08
*
Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...
herbelin
2003-10-08
*
Renommage no-strict en -strict-implicit; option -dont-load-proofs
herbelin
2003-10-08
*
Debranchement de l'affichage automatique de Proof par le traducteur (trop com...
herbelin
2003-10-07
*
Correction du bug 335 et Export/Require Export dans un module
coq
2003-10-07
*
Reparation plus juste de l'inefficacite avec loaded_modules (respecte l'ordre)
herbelin
2003-10-04
*
pr_vernac est paresseux; States.unfreeze seulement après que msgnl ait
herbelin
2003-10-03
*
Correction bug explosion de la taille de la liste loaded_modules
herbelin
2003-10-03
*
Implantation de l'option 'format' des Notations
herbelin
2003-10-01
*
Ajout 'Close Scope'.
herbelin
2003-09-30
*
Ajout 'Close Scope'.
herbelin
2003-09-30
*
Ajout 'About'
herbelin
2003-09-26
*
Decouplage printing en v8 pour les interpretations de notations
herbelin
2003-09-26
*
V8Infix declarait a tort une regle d'interpretation V7
herbelin
2003-09-25
*
Traduction aussi si -translate et -load-vernac-source
herbelin
2003-09-24
*
Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...
herbelin
2003-09-23
*
Utilisation de noms dans 'Implicit Arguments [...]'
herbelin
2003-09-23
[prev]
[next]