index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
equality.ml
Commit message (
Expand
)
Author
Age
*
Adding a syntax for "n-ary" rewrite:
letouzey
2007-07-06
*
Correction d'un bug dans l'affichage du message d'erreur real_clean
herbelin
2007-05-29
*
Nouvelle stratégie d'unification des types des with-bindings dans
herbelin
2007-05-22
*
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
*
Proposition de correction pour le bug #1173 (ou du moins pour un
herbelin
2007-04-13
*
Changement mineur du comportement de 'rewrite .. in * |-': si le
notin
2007-03-30
*
Suppression argument pattern_source du case_info (code jamais utilisé)
herbelin
2007-03-15
*
Correction bug #1439 (comportement de replace by)
notin
2007-03-13
*
Correction typo liée au commit 8779 (levait une anomalie)
herbelin
2007-02-21
*
remplacement d'un test d'egalite par un test de convertibilite dans injection...
jforest
2006-12-22
*
revision de la semantique de rewrite ... in <clause>. details dans la doc
letouzey
2006-10-05
*
Changement de comportement du [rewrite ... in H]: Coq échoue si H
notin
2006-10-03
*
Retour sur la suppression du pf_nf (trop d'exemples utilisent avec
herbelin
2006-10-03
*
Une passe sur l'injection et la discrimination...
herbelin
2006-10-01
*
Suppression de la comparaison (inutile) des paramètres globaux des
herbelin
2006-09-30
*
+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and no
jforest
2006-08-22
*
Correcting for bug #1167
jforest
2006-07-05
*
Updating documentation of replace and correcting a typo in error message of r...
jforest
2006-06-12
*
Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...
herbelin
2006-05-30
*
- Déplacement des types paramétriques prod, sum, option, identity,
herbelin
2006-05-28
*
"subst." works now even when it exists an hypothesis have the form "x=x" in t...
jforest
2006-05-20
*
Extension syntaxique de rewrite in: au lieu de pouvoir faire
letouzey
2006-05-02
*
Changement de comportement de rewrite: face a une egalité setoid, on
letouzey
2006-05-02
*
Correction bug 1119 (inversion marche a moitie dans Type)
herbelin
2006-04-02
*
+ destruct now works as induction on multiple arguments :
jforest
2006-03-21
*
- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses
herbelin
2006-01-16
*
Nettoyage coqlib
herbelin
2005-12-30
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
Changement des named_context
gregoire
2005-12-02
*
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-11-08
*
Types inductifs parametriques
mohring
2005-11-02
*
Réparation bug #1004; nettoyage
herbelin
2005-09-08
*
essai de typage des instantiations d\'evars
barras
2005-06-06
*
Expansion Case dans injection et discriminate (cf bug #829)
herbelin
2004-11-21
*
Ajout 'dependent rewrite in'
herbelin
2004-10-28
*
Restructuration fonctions de réécriture depuis égalité dépendante; facto...
herbelin
2004-10-27
*
New tactic [setoid_]rewrite ... in ... [generate side conditions ...].
sacerdot
2004-09-30
*
Proof term size optimization: setoid_rewrite H where H is an application of
sacerdot
2004-09-30
*
New syntax
sacerdot
2004-09-29
*
Correction bug report #855
herbelin
2004-09-24
*
hiding the meta_map in evar_defs
barras
2004-09-15
*
inclusion de meta_map dans evar_defs
barras
2004-09-12
*
deuxieme vague de modifs: evar_defs fonctionnel
barras
2004-09-07
*
premiere reorganisation de l\'unification
barras
2004-09-03
*
Protection erreur find_eq_data dans decompEqThen et uniformisation messages d...
herbelin
2004-07-30
*
Since setoid_{replace,rewrite} now uses replace there is a circularity
sacerdot
2004-07-23
*
Nouvelle en-tête
herbelin
2004-07-16
*
Message d'erreur
herbelin
2004-03-17
*
bug d'Inversion #529 (pb avec ordre d'evaluation)
barras
2004-03-15
[next]