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
...
*
Updated compatibility for rewriting equality proofs that are dependent
herbelin
2009-12-12
*
Promote evar_defs to evar_map (in Evd)
glondu
2009-11-11
*
Restructuration of command.ml + generic infrastructure for inductive schemes
herbelin
2009-11-08
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Fix the bug-ridden code used to choose leibniz or generalized
msozeau
2009-09-08
*
Move out JMeq of subst for compatibility (it affects e.g. the
herbelin
2009-08-06
*
Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"
letouzey
2009-07-24
*
Add new variants of [rewrite] and [autorewrite] which differ in the
msozeau
2009-06-30
*
Some dead code removal + cleanups
letouzey
2009-04-08
*
Port [rewrite] tactics to open terms. Currently no check that evars
msozeau
2008-11-05
*
Évolutions diverses et variées.
herbelin
2008-08-04
*
Even better test for choosing rewrite or setoid_rewrite.
msozeau
2008-07-26
*
- Implantation de la suggestion 1873 sur discriminate. Au final,
herbelin
2008-06-21
*
- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)
herbelin
2008-06-10
*
Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.
msozeau
2008-04-12
*
Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part
msozeau
2008-03-07
*
Plug the new setoid implemtation in, leaving the original one commented
msozeau
2008-03-06
*
Rework on rich forms of rewrite
letouzey
2008-03-01
*
Adding a syntax for "n-ary" rewrite:
letouzey
2007-07-06
*
Nouvelle stratégie d'unification des types des with-bindings dans
herbelin
2007-05-22
*
- Propagation des evars non résolues vers les with_bindings; permet par exemple
herbelin
2007-05-20
*
correction de bug dans Function et augmentation de la classe des fonctions su...
jforest
2007-05-17
*
Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.
herbelin
2007-04-28
*
Une passe sur l'injection et la discrimination...
herbelin
2006-10-01
*
+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and no
jforest
2006-08-22
*
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
[prev]
[next]