index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
/
astterm.mli
Commit message (
Expand
)
Author
Age
*
Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...
herbelin
2001-09-10
*
amelioration de la structure des univers
barras
2001-03-28
*
entetes
filliatr
2001-03-15
*
Déplacement de qualid dans Nametab, hors du noyau
herbelin
2001-03-01
*
Mise en place d'un système optionnel de discharge immédiat; prise en compte...
herbelin
2001-02-14
*
Ré-introduction des implicites à la volée dans la définition des inductifs
herbelin
2001-01-27
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
Réorganisation autour de globalize_constr
herbelin
2000-11-24
*
Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...
herbelin
2000-11-22
*
Acceptation des noms qualifiés; utilisation de global_reference dans pattern...
herbelin
2000-11-20
*
Simplifications autour de typed_type (renommé types par analogie avec sorts)...
herbelin
2000-10-18
*
Nettoyage
herbelin
2000-10-18
*
Changement "command" en "constr" et globalize_command en globalize_constr
herbelin
2000-10-16
*
Reorganisation des interp_constr
herbelin
2000-10-03
*
Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion d...
herbelin
2000-09-26
*
Canonisation de certains noms dans Pretyping, Asterm et Safe_typing
herbelin
2000-09-06
*
Modifs d'interpretation de patterns + exceptions dans le lexer
delahaye
2000-07-21
*
ajout interp_sort
herbelin
2000-05-05
*
Ajout du langage de tactiques
delahaye
2000-05-03
*
Déplacement du type reference dans Term
herbelin
2000-04-28
*
Introduction d'un type constr_pattern pour les différents filtrages
herbelin
2000-04-26
*
Réajout globalize_command
herbelin
2000-03-30
*
Nettoyage de l'interface d'Astterm; renommage des constr_of_com and co en int...
herbelin
2000-03-28
*
mise au point lexer / debugage PP
filliatr
1999-12-05
*
- global_reference traite des variables
filliatr
1999-12-03
*
modifs pour premiere edition de liens
filliatr
1999-12-02
*
Intégration du Termast et du Retyping de HH, et modifications connexes
herbelin
1999-12-01
*
module Egrammar
filliatr
1999-12-01
*
- environment -> safe_environment
filliatr
1999-12-01
*
portage Astterm (partiellement)
filliatr
1999-11-29
*
Modification pour faire compiler pretyping.ml qui maintenant compile
herbelin
1999-11-26
*
MAJ pour fusion avec pretyping
herbelin
1999-11-24
*
organisation de trad (entre parsing/ et pretyping/)
filliatr
1999-10-13