index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
/
termast.ml
Commit message (
Expand
)
Author
Age
*
Changement des named_context
gregoire
2005-12-02
*
Code v7 obsolete
herbelin
2005-05-05
*
HUGE COMMIT
sacerdot
2005-01-03
*
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
sacerdot
2004-11-16
*
Précisions message d'erreur
herbelin
2004-08-23
*
Nouvelle en-tête
herbelin
2004-07-16
*
modif des fixpoints pour que si on donne une notation au produit, les pts fix...
barras
2004-03-05
*
Substitution dans REvar et PEvar plutot que encodage via noeud application po...
herbelin
2003-12-19
*
Changement de l'afficheur pour que les variables liées aient un nom indépen...
herbelin
2003-09-23
*
Ajout construction If primitive dans constr_expr et rawconstr
herbelin
2003-09-09
*
Paramétrisation vis à vis de existential_key
herbelin
2003-09-06
*
Nouvelle mouture du traducteur v7->v8
herbelin
2003-08-11
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
Affichage des Fix contenant des Let dans leur context (ce que la tactique Fix...
herbelin
2003-04-27
*
simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...
letouzey
2003-04-16
*
Affichage forcé des implicites contextuels si pas de contexte connu
herbelin
2003-04-10
*
Options d'affichage maintenant dans Constrextern
herbelin
2003-04-07
*
Bugs affichage
herbelin
2003-01-16
*
Introduction d'un constructeur ARROW; rétablissement priorités des
herbelin
2002-11-20
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Des critères plus fins d'analyse des implicites automatiques; meilleur affic...
herbelin
2002-10-28
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Utilisation d'une construction spéciale SECVAR pour gérer la
herbelin
2002-05-14
*
Correction bug infix sur des varaiables
mohring
2002-03-29
*
petit nettoyage de kernel/inductive
barras
2002-02-07
*
MAJ de la traduction en ast des variables de section en qualid
herbelin
2001-12-13
*
compat ocaml 3.03
filliatr
2001-12-13
*
GROS COMMIT:
barras
2001-11-05
*
Abstraction de l'immplementation de dirpath et implementation dans l'autre se...
herbelin
2001-10-17
*
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-09
*
Ajout de dynamiques pour les quotations constr et tactic
delahaye
2001-10-02
*
Parsing
herbelin
2001-08-10
*
Facilites pour le debogguage des univers.
coq
2001-05-29
*
un warning pas beau supprimmé
filliatr
2001-04-23
*
Bug affichage d'implicites pour les vars liees
herbelin
2001-04-15
*
Bug MUTCASE au lieu CASE
herbelin
2001-03-22
*
entetes
filliatr
2001-03-15
*
Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisation
herbelin
2001-03-11
*
Déplacement de qualid dans Nametab, hors du noyau
herbelin
2001-03-01
*
Bug affichage coercions
herbelin
2001-02-16
*
ident au lieu de string pour le nom de base de qualid
herbelin
2001-02-16
*
Mise en place d'un système optionnel de discharge immédiat; prise en compte...
herbelin
2001-02-14
*
Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref
herbelin
2001-02-07
*
Ajout d'une commande pour afficher chaque coercion à la demandeparsing/g_bas...
herbelin
2001-02-06
*
Suppression de l'affichage des instances des ?n
herbelin
2000-12-18
*
Ajout des Fix et CoFix dans les patterns
delahaye
2000-11-28
*
Prise en compte des implicites de locaux à l'affichage
herbelin
2000-11-27
*
Affichage des paths avec des '.'; print_id, print_sp -> pr_id, pr_sp;
herbelin
2000-11-23
*
Utilisation de global_reference dans rawconstr
herbelin
2000-11-20
*
suppression des (* open Generic *)
filliatr
2000-11-02
[next]