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
*
- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)
herbelin
2008-06-10
*
Nettoyage des tactiques basées sur "simpl" (delta-réduction cachant
herbelin
2007-04-13
*
Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...
herbelin
2006-05-30
*
Amélioration des messages d'erreurs de tacred; unfold considère maintenant le
herbelin
2006-02-07
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...
herbelin
2005-01-02
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
Nouvelle en-tête
herbelin
2004-07-16
*
Bug (destruct/induction ne savent pas traiter le cas non atomique avec paramÃ...
herbelin
2004-01-27
*
Bug introduit avec le 'Simpl f'
herbelin
2003-11-22
*
Ajout reduce_to_quantified_ref
herbelin
2003-11-09
*
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