index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
toplevel
/
himsg.ml
Age
Commit message (
Expand
)
Author
2003-03-31
Restauration de make_all_different (disparu depuis version 1.74) car sinon de...
herbelin
2003-03-29
Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)
herbelin
2003-03-12
*** empty log message ***
barras
2002-12-21
Légère amélioration des messages d'erreur des with-bindings et des Rewrite
herbelin
2002-12-19
suite du commit precedent
barras
2002-09-03
pretyping/pretyping.ml
herbelin
2002-08-13
Renoncement à distinguer les types "constr" et "types"; nettoyage
herbelin
2002-08-02
Modules dans COQ\!\!\!\!
coq
2002-05-29
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-04-10
Amélioration des messages d'erreurs concernant l'inférence des implicites
herbelin
2001-12-21
Un ++ au lieu d'un ;
herbelin
2001-12-18
Nettoyage exceptions liées au vieux Case
herbelin
2001-12-13
compat ocaml 3.03
filliatr
2001-11-29
nouvel algo de conversion plus uniforme
barras
2001-11-21
Amélioration message Cases
herbelin
2001-11-21
Amélioration messages d'erreur arité incorrecte (notamment record)
herbelin
2001-11-12
Suites modifs du noyau. Univ devient purement fonctionnel.
barras
2001-11-05
GROS COMMIT:
barras
2001-10-15
Orthographe
herbelin
2001-10-09
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-05-28
Pretty -> Prettyp
filliatr
2001-05-23
amelioration des messages d'erreurs vis a vis des evars
barras
2001-05-03
Changement de la structure des points fixes
barras
2001-04-25
Amelioration message args constructeur
herbelin
2001-04-24
Messages d'erreur Cases
herbelin
2001-04-13
Mise en place d'un test de clauses non utilisees
herbelin
2001-03-28
amelioration de la structure des univers
barras
2001-03-15
entetes
filliatr
2001-03-11
Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisation
herbelin
2001-03-01
Déplacement de qualid dans Nametab, hors du noyau
herbelin
2001-02-28
Typo message Scheme
herbelin
2000-12-18
Amélioration message d'erreur mauvais prédicat
herbelin
2000-12-14
Raffinement erreur Wrong Predicate
herbelin
2000-12-06
Ajout erreur DoesNotOccurIn
herbelin
2000-12-06
Reparation conditions de positivites inductifs, echange dans add_entry
mohring
2000-11-27
uniformisation messages d'erreur
filliatr
2000-11-23
print_id, print_sp -> pr_id, pr_sp
herbelin
2000-11-22
Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...
herbelin
2000-11-20
Ajout erreur GlobalNotFound
herbelin
2000-11-08
amélioration
herbelin
2000-11-02
suppression des (* open Generic *)
filliatr
2000-10-18
Renommage canonique :
herbelin
2000-10-11
Message d'erreur bad pattern
herbelin
2000-10-10
Messages d'erreurs Cases
herbelin
2000-09-15
Expression anglaise
herbelin
2000-09-14
Abstraction de constr
herbelin
2000-09-10
Correction pour make doc
herbelin
2000-09-10
Suppression de Abst
herbelin
2000-09-10
Ajout d'un LetIn primitif.
herbelin
2000-09-06
kernel/type_errors.ml
herbelin
[next]