index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
equality.mli
Commit message (
Expand
)
Author
Age
*
Extension syntaxique de rewrite in: au lieu de pouvoir faire
letouzey
2006-05-02
*
+ destruct now works as induction on multiple arguments :
jforest
2006-03-21
*
Réparation bug #1004; nettoyage
herbelin
2005-09-08
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
Restructuration fonctions de réécriture depuis égalité dépendante; facto...
herbelin
2004-10-27
*
Simplifications concommitantes à la correction du bug #855
herbelin
2004-09-24
*
Nouvelle en-tête
herbelin
2004-07-16
*
Suppression de la distinction entre elimination de Type vers Type ou pas (Fal...
herbelin
2004-03-11
*
Ajout 'replace in'
herbelin
2004-03-01
*
factorisation et generalisation des clauses
barras
2003-11-13
*
Death of 'a somewhat cryptic module'
herbelin
2003-10-11
*
Restructuration des procédures de filtrage
herbelin
2003-05-19
*
notations <>, Assumption avec existentiel, replace term
mohring
2003-03-28
*
nouveau Subst:
barras
2002-12-17
*
Subst (tout court)
filliatr
2002-09-16
*
tactique Subst x1 ... xn
filliatr
2002-09-11
*
Code mort de AutoRewrite
herbelin
2002-09-09
*
AutoRewrite substitutive...
coq
2002-08-13
*
tactique Subst
filliatr
2002-07-17
*
Repercussion de la possibilit de mettre des hyps quantifiees dans Simplify_eq...
herbelin
2002-06-05
*
Rpercussion de la possibilit de mettre des hyps quantifies dans Simplify_eq e...
herbelin
2002-06-05
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
Suppression des local_constraints, des ctxtty et du focus.
clrenard
2001-11-06
*
Suppression option immediate_discharge; nettoyage de Declare et conséquences
herbelin
2001-10-11
*
entetes
filliatr
2001-03-15
*
Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...
herbelin
2001-02-14
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
Nettoyage
herbelin
2000-05-18
*
Ajout du langage de tactiques
delahaye
2000-05-03
*
Adaptés pour le type constr_pattern et les nouvelles fonctions de filtrage
herbelin
2000-04-30
*
Déplacement du type reference dans Term
herbelin
2000-04-28
*
Modification de type_of_case, type_case_branches, etc;nettoyage
herbelin
2000-03-21
*
gros commit de tout ce que j'ai fait pendant les vacances :
filliatr
2000-01-21