aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Mises à jour test-suite + amélioration message d'erreur pour non-bug #1757Gravatar herbelin2008-05-07
* Move exception-handling code for catching tactics failure Gravatar msozeau2008-05-01
* Clarification de l'ordre d'interprétation des variables dans ltac. EnGravatar herbelin2008-05-01
* Correct a bug in "new auto" and also unify_eqn which did not do localGravatar msozeau2008-04-30
* Fix eauto still using delta when it shouldn't (should make CoRN compileGravatar msozeau2008-04-29
* Backtrack on using metas eagerly in auto, only done in "new auto" forGravatar msozeau2008-04-28
* Correction du bug des types singletons pas sous-type de SetGravatar herbelin2008-04-27
* - Backtrack sur option with_types suite à confusion sur l'utilisationGravatar herbelin2008-04-27
* - Fix bug in unification not taking into account the right metaGravatar msozeau2008-04-27
* - Backtrack sur extension de syntaxe pour pose qui rentre en conflit avecGravatar herbelin2008-04-26
* Debug implementation of failing tactics in Morphism to allow earlierGravatar msozeau2008-04-26
* Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveGravatar herbelin2008-04-25
* - Add pretty-printers for Idpred, Cpred and transparent_state, used forGravatar msozeau2008-04-24
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* Backtrack on change of flags for elim, otherwise rewrite goes underGravatar msozeau2008-04-23
* Change default eauto depth to 100 in setoid_rewrite, bump necessaryGravatar msozeau2008-04-23
* - Correct unification for the rewrite variant of setoid_rewrite,Gravatar msozeau2008-04-21
* - Parameterize unification by two sets of transparent_state, one for openGravatar msozeau2008-04-21
* Work on the "occurrences" tactic argument. It is now possible to passGravatar msozeau2008-04-20
* Bug squashing day !Gravatar msozeau2008-04-17
* Little fixes in setoid_rewrite.Gravatar msozeau2008-04-17
* More renamings to avoid clashes (e.g. with CoRN).Gravatar msozeau2008-04-15
* Document CHANGES in setoid rewrite, move DefaultRelation toGravatar msozeau2008-04-15
* - Add "Global" modifier for instances inside sections with the usualGravatar msozeau2008-04-15
* - Un peu de doc, préparation du CHANGES pour la release.Gravatar herbelin2008-04-15
* Diverses corrections Gravatar herbelin2008-04-14
* Renamings to avoid clashes with definitions in Relation_Definitions, nowGravatar msozeau2008-04-14
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* Add the ability to specify what to do with free variables in instanceGravatar msozeau2008-04-12
* Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.Gravatar msozeau2008-04-12
* Verify Setoid is loaded only if we're not in Coq.Classes.*. Add explicitGravatar msozeau2008-04-09
* Verify Setoid is loaded before doing anything.Gravatar msozeau2008-04-09
* Fix evar bugs in type classes:Gravatar msozeau2008-04-09
* - A little cleanup in Classes/*. Separate standard morphisms onGravatar msozeau2008-04-08
* - Retour en arrière sur la capacité du nouvel apply à utiliser lesGravatar herbelin2008-04-05
* Minor fixes: Gravatar msozeau2008-04-05
* Mise en place d'une extension de apply pour que celui-ci sacheGravatar herbelin2008-04-04
* - Relâchement de la contrainte de bonne longueur des intropatternsGravatar herbelin2008-04-04
* Quelques améliorations des intro patterns:Gravatar herbelin2008-04-04
* Erreur ou acceptation silencieuce plutôt qu'avertissement systématique quandGravatar herbelin2008-04-04
* Protection de rewrite in contre le dépliage des constantes dans w_unify, ce quiGravatar herbelin2008-04-04
* Minor fixes. Use expanded type in class_tactics for Morphism search, toGravatar msozeau2008-04-02
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
* Ajout "simple apply" et "simple eapply" pour apply sans unfoldGravatar herbelin2008-04-01
* - Fix for rewriting under dependent products.Gravatar msozeau2008-03-31
* Modifications diverses et variées :Gravatar herbelin2008-03-30
* Improve error handling and messages for typeclasses. Gravatar msozeau2008-03-28
* Various fixes on typeclasses:Gravatar msozeau2008-03-27
* Interpret patterns for hypotheses types in match goal in type_scope (if not aGravatar msozeau2008-03-25
* Fix a bug found by B. Grégoire when declaring morphisms in moduleGravatar msozeau2008-03-23