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
*
Prise en compte des délimiteurs dans les motifs de Cases
herbelin
2002-10-21
*
Réparation du mécanisme des infixes quand ils commencent par une lettre
herbelin
2002-10-16
*
Meilleure analyse de si une règle de grammaire/syntaxe existent déjà ou pas
herbelin
2002-10-14
*
Ajout "Arguments Scope" pour associer des "scopes" aux arguments d'une
herbelin
2002-10-14
*
Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...
herbelin
2002-10-13
*
retour en arriere concernant la recherche d'occurence modulo expansion des le...
barras
2002-10-09
*
Que des niveaux d'univers frais dans le type des constantes globales
herbelin
2002-09-29
*
Que des niveaux d'univers frais dans le type des constantes globales
herbelin
2002-09-29
*
Encore quelques rangements dans Nametab + petits trucs
coq
2002-09-27
*
Nametab data structure reorganisation
coq
2002-09-24
*
La notation with dependante + affichage dependante de moduels corrige
coq
2002-09-20
*
pretyping/pretyping.ml
herbelin
2002-09-03
*
Pretty-printing preliminaire des modules, commandes
coq
2002-08-19
*
Suppression automatique du corps des définitions locales opaques dans
herbelin
2002-08-17
*
Strengthenning rules for modules + No modules in sections
coq
2002-08-16
*
Renoncement à distinguer les types "constr" et "types"; nettoyage
herbelin
2002-08-13
*
Renoncement à distinguer les types "constr" et "types"; nettoyage
herbelin
2002-08-13
*
Petites corrections ici et la
coq
2002-08-13
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Error_in_file redondant et inapproprié
herbelin
2002-07-11
*
Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pour
herbelin
2002-07-11
*
Ajout de FNL ou utilisation de msgnl
herbelin
2002-06-07
*
Intgration uniforme de coercions dans les dclarations (Variable and co) et re...
herbelin
2002-06-03
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
Fichier des expressions de commandes vernaculaires
herbelin
2002-05-29
*
Utilisation des de Bruijn pour la constructions des records et de leur projec...
herbelin
2002-05-13
*
Déplacement/renommage de Class.stre_max en Declare.strength_min
herbelin
2002-04-16
*
Amélioration des messages d'erreurs concernant l'inférence des implicites
herbelin
2002-04-10
*
backtrack dans l'algo d'unification
barras
2002-04-10
*
resolution du pb d'efficacite du a Sign.add_named_decl
barras
2002-04-04
*
Bug d'affichage des erreurs localisées dans un fichier suite à
herbelin
2002-03-27
*
Meilleure gestion de la reduction dans Field
delahaye
2002-03-17
*
raccourci -l en plus de -load-vernac-source
letouzey
2002-03-07
*
-dump-glob dans le usage
filliatr
2002-02-27
*
Changé le nom du module Errors (errors.mli, errors.ml) en Cerrors parce
ddr
2002-02-20
*
petits changements cosmetiques sur les tactiques
barras
2002-02-15
*
- Reforme de la gestion des args recursifs (via arbres reguliers)
barras
2002-02-14
*
option -dump-glob pour coqdoc
filliatr
2002-02-14
*
affichage des messages d'erreur pour Stack_overflow, Out_of_memory, Break
barras
2002-02-06
*
Plusieurs arguments autorisés pour Require et Read Module
herbelin
2002-01-18
*
Un ++ au lieu d'un ;
herbelin
2001-12-21
*
Corrections post contournement des streams avec ++
herbelin
2001-12-19
*
Nettoyage exceptions liées au vieux Case
herbelin
2001-12-18
*
Ajout syntaxe 'Canonical Structure' en remplacement de @Definition + suppress...
herbelin
2001-12-16
*
compat ocaml 3.03
filliatr
2001-12-13
*
- condition de garde (suite)
barras
2001-12-10
*
reparation de Locate
barras
2001-11-29
*
nouvel algo de conversion plus uniforme
barras
2001-11-29
*
Amélioration message Cases
herbelin
2001-11-21
*
Amélioration messages d'erreur arité incorrecte (notamment record)
herbelin
2001-11-21
[next]