aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/equality.ml
Commit message (Expand)AuthorAge
* Added the automatic generation of the boolean equality if possible and theGravatar vsiles2007-10-05
* Ajout de eelim, ecase, edestruct et einduction (expérimental).Gravatar herbelin2007-10-03
* Uniformisation politique de nommage evd/isevars (evd si evar_defs,Gravatar herbelin2007-09-06
* Adding a syntax for "n-ary" rewrite: Gravatar letouzey2007-07-06
* Correction d'un bug dans l'affichage du message d'erreur real_cleanGravatar herbelin2007-05-29
* Nouvelle stratégie d'unification des types des with-bindings dansGravatar herbelin2007-05-22
* correction de bug dans Function et augmentation de la classe des fonctions su...Gravatar jforest2007-05-17
* Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.Gravatar herbelin2007-04-28
* Proposition de correction pour le bug #1173 (ou du moins pour unGravatar herbelin2007-04-13
* Changement mineur du comportement de 'rewrite .. in * |-': si leGravatar notin2007-03-30
* Suppression argument pattern_source du case_info (code jamais utilisé)Gravatar herbelin2007-03-15
* Correction bug #1439 (comportement de replace by)Gravatar notin2007-03-13
* Correction typo liée au commit 8779 (levait une anomalie)Gravatar herbelin2007-02-21
* remplacement d'un test d'egalite par un test de convertibilite dans injection...Gravatar jforest2006-12-22
* revision de la semantique de rewrite ... in <clause>. details dans la docGravatar letouzey2006-10-05
* Changement de comportement du [rewrite ... in H]: Coq échoue si HGravatar notin2006-10-03
* Retour sur la suppression du pf_nf (trop d'exemples utilisent avecGravatar herbelin2006-10-03
* Une passe sur l'injection et la discrimination...Gravatar herbelin2006-10-01
* Suppression de la comparaison (inutile) des paramètres globaux desGravatar herbelin2006-09-30
* + Changing "in <hyp>" to "in <clause>" (no at, no InValue and noGravatar jforest2006-08-22
* Correcting for bug #1167 Gravatar jforest2006-07-05
* Updating documentation of replace and correcting a typo in error message of r...Gravatar jforest2006-06-12
* Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...Gravatar herbelin2006-05-30
* - Déplacement des types paramétriques prod, sum, option, identity,Gravatar herbelin2006-05-28
* "subst." works now even when it exists an hypothesis have the form "x=x" in t...Gravatar jforest2006-05-20
* Extension syntaxique de rewrite in: au lieu de pouvoir faire Gravatar letouzey2006-05-02
* Changement de comportement de rewrite: face a une egalité setoid, onGravatar letouzey2006-05-02
* Correction bug 1119 (inversion marche a moitie dans Type)Gravatar herbelin2006-04-02
* + destruct now works as induction on multiple arguments : Gravatar jforest2006-03-21
* - Tactic "assert" now accepts "as" intro patterns and "by" tactic clausesGravatar herbelin2006-01-16
* Nettoyage coqlibGravatar herbelin2005-12-30
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Changement des named_contextGravatar gregoire2005-12-02
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Types inductifs parametriquesGravatar mohring2005-11-02
* Réparation bug #1004; nettoyageGravatar herbelin2005-09-08
* essai de typage des instantiations d\'evarsGravatar barras2005-06-06
* Expansion Case dans injection et discriminate (cf bug #829)Gravatar herbelin2004-11-21
* Ajout 'dependent rewrite in'Gravatar herbelin2004-10-28
* Restructuration fonctions de réécriture depuis égalité dépendante; facto...Gravatar herbelin2004-10-27
* New tactic [setoid_]rewrite ... in ... [generate side conditions ...].Gravatar sacerdot2004-09-30
* Proof term size optimization: setoid_rewrite H where H is an application ofGravatar sacerdot2004-09-30
* New syntaxGravatar sacerdot2004-09-29
* Correction bug report #855Gravatar herbelin2004-09-24
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* inclusion de meta_map dans evar_defsGravatar barras2004-09-12
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Protection erreur find_eq_data dans decompEqThen et uniformisation messages d...Gravatar herbelin2004-07-30
* Since setoid_{replace,rewrite} now uses replace there is a circularityGravatar sacerdot2004-07-23