index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
pretyping.mli
Commit message (
Expand
)
Author
Age
*
inclusion de meta_map dans evar_defs
barras
2004-09-12
*
deuxieme vague de modifs: evar_defs fonctionnel
barras
2004-09-07
*
Nouvelle en-tête
herbelin
2004-07-16
*
Amelioration message d'erreur pour ltac
herbelin
2003-11-04
*
Suppression définitive de lmatch et or_metanum dans tacinterp
herbelin
2003-05-21
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
- modifs de la condition de garde pour mieux tenir compte des raisonnements
barras
2002-04-02
*
Suppression des local_constraints, des ctxtty et du focus.
clrenard
2001-11-06
*
Ajout de dynamiques pour les quotations constr et tactic
delahaye
2001-10-02
*
amelioration de la structure des univers
barras
2001-03-28
*
entetes
filliatr
2001-03-15
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
Nettoyage Coercion
herbelin
2000-10-19
*
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
*
portage Refine
filliatr
2000-07-20
*
Séparation des contraintes de type et de valeur dans pretyping
herbelin
2000-06-29
*
diverses modifs pour ocamlweb
filliatr
2000-05-03
*
Ajout du langage de tactiques
delahaye
2000-05-03
*
Nettoyage de l'interface d'Astterm; renommage des constr_of_com and co en int...
herbelin
2000-03-28
*
changement type add_anonymous_leaf
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
*
- environment -> safe_environment
filliatr
1999-12-01
*
- Typing -> Safe_typing
filliatr
1999-12-01
*
ocamlweb
filliatr
1999-11-30
*
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