index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
tacred.mli
Commit message (
Expand
)
Author
Age
*
Ajout Simpl et Change sur des sous-termes
herbelin
2002-12-09
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Mise au point de declare_red_expr
herbelin
2002-05-30
*
Finalement un seul constr pour l'instant dans ExtraRedExpr
herbelin
2002-05-30
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
nouvel algo de conversion plus uniforme
barras
2001-11-29
*
Suppression des local_constraints, des ctxtty et du focus.
clrenard
2001-11-06
*
GROS COMMIT:
barras
2001-11-05
*
Nettoyage reduce_to_ind et one_step_reduce
herbelin
2001-09-09
*
amelioration des messages d'erreurs vis a vis des evars
barras
2001-05-23
*
entetes
filliatr
2001-03-15
*
Mise en place de la possibilite d'unfolder des variables locales et des const...
filliatr
2001-01-31
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
Minor correction for Ocamlweb + doc update
coq
2000-09-14
*
Déplacement de fonctions de Reduction vers Tacred
herbelin
2000-09-14
*
Nouveaux types 'constructor' et 'inductive' dans Term;
herbelin
1999-12-15
*
- états fabriqués avec -silent
filliatr
1999-12-13
*
modifs pour premiere edition de liens
filliatr
1999-12-02