aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/extratactics.ml4
Commit message (Expand)AuthorAge
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Remove useless Liboject.export_function fieldGravatar glondu2009-09-17
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Move out JMeq of subst for compatibility (it affects e.g. theGravatar herbelin2009-08-06
* Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"Gravatar letouzey2009-07-24
* Add new variants of [rewrite] and [autorewrite] which differ in theGravatar msozeau2009-06-30
* - Fixing declarative mode in presence of high use of Change_evars nodesGravatar herbelin2009-05-20
* - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceGravatar herbelin2009-05-09
* Rewrite autorewrite to use a dnet indexed by the left-hand sides (orGravatar msozeau2009-04-14
* Getting rid of the previous implementation of setoid_rewrite which wasGravatar msozeau2009-01-18
* Finish fix for the treatment of [inverse] in [setoid_rewrite], making aGravatar msozeau2008-12-16
* About "apply in":Gravatar herbelin2008-12-09
* Port [rewrite] tactics to open terms. Currently no check that evarsGravatar msozeau2008-11-05
* Fixes and refinements regarding occurrence selection:Gravatar herbelin2008-10-26
* Various little improvements:Gravatar msozeau2008-09-25
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Fixes in generalize_eqs/dependent induction to allow the user to specifyGravatar msozeau2008-07-28
* New tactics [conv] to test convertibility (actually, unification) of twoGravatar msozeau2008-07-22
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
* Correction du bug des types singletons pas sous-type de SetGravatar herbelin2008-04-27
* Plug the new setoid implemtation in, leaving the original one commentedGravatar msozeau2008-03-06
* Nettoyage de code en vue de la release. Plus de Warning: Unused Gravatar aspiwack2007-12-18
* Adding the tactic "instantiate" (without argument), to force theGravatar glondu2007-12-07
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Add a new tactic to generalize an instantiated inductive predicate adding equ...Gravatar msozeau2007-08-07
* Nouvelle stratégie d'unification des types des with-bindings dansGravatar herbelin2007-05-22
* - Propagation des evars non résolues vers les with_bindings; permet par exempleGravatar herbelin2007-05-20
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
* Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.Gravatar herbelin2007-04-28
* Correction bug #1041 (double cause : non évitement des noms existants enGravatar herbelin2006-12-12
* Ajout de la tactique "apply in".Gravatar herbelin2006-10-24
* Une passe sur l'injection et la discrimination...Gravatar herbelin2006-10-01
* Bug in replace tactics introduced in r9073 (overlap between replace .. with a...Gravatar jforest2006-08-23
* + Changing "in <hyp>" to "in <clause>" (no at, no InValue and noGravatar jforest2006-08-22
* Suite utilisation hyp au lieu ident: donne la localisationnGravatar herbelin2006-06-23
* Correction ident -> hyp pour dinterpréter des identificateurs devant êt...Gravatar herbelin2006-06-23
* Changement du type d'argument 'TacticArgType X' en un typeGravatar herbelin2006-06-08
* Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...Gravatar herbelin2006-05-30
* Extension syntaxique de rewrite in: au lieu de pouvoir faire Gravatar letouzey2006-05-02
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* + destruct now works as induction on multiple arguments : Gravatar jforest2006-03-21
* Messages de idtac et fail peuvent maintenant être des listes de string, int ...Gravatar herbelin2006-01-21
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Petit bug Declare Implicit TacticGravatar herbelin2005-09-10
* Nouvelle déclaration 'Declare Implicit Tactic' pour automatiser la résoluti...Gravatar herbelin2005-09-09
* Implemented autorewrite with ... in hyp [using ...].Gravatar sacerdot2005-05-18
* HUGE COMMITGravatar sacerdot2005-01-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 15:02:40 +0000