aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/class_tactics.ml4
Commit message (Expand)AuthorAge
* Fix bug in term dnet preventing some unifications. Allow "higher-order"Gravatar msozeau2008-07-28
* Even better test for choosing rewrite or setoid_rewrite.Gravatar msozeau2008-07-26
* A (safe) implementation of prolog's cut in the typeclasses eauto to avoidGravatar msozeau2008-07-24
* New tactics [conv] to test convertibility (actually, unification) of twoGravatar msozeau2008-07-22
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Stop using the discrimination net in typeclasses/setoid rewrite, which wasGravatar msozeau2008-07-02
* Enhanced discrimination nets implementation, which can now work withGravatar msozeau2008-06-27
* Fix bug in implementation of splitting of class constraints.Gravatar msozeau2008-06-18
* Compatibility fixes (Add Setoid bug and accidental introduction of aGravatar msozeau2008-06-18
* Fixes w.r.t. let binders in class contexts and Add ParametricGravatar msozeau2008-06-17
* Better typeclass error messages, always giving the full set ofGravatar msozeau2008-06-17
* Optionally (and by default) split typeclasses evars into connected Gravatar msozeau2008-06-11
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* - Correct handling of DependentMorphism error, using tclFAIL instead ofGravatar msozeau2008-06-10
* Correct handling of the environment in build_signature, and throwGravatar msozeau2008-06-07
* Change setoid_rewrite's matching semantics to continue matching insideGravatar msozeau2008-06-07
* Correctly catch UnresolvableConstraint exception which is now located. Gravatar msozeau2008-06-05
* Fixes incorrect handling of existing existentials variables inGravatar msozeau2008-06-03
* Improvements on coqdoc by adding more information into .globGravatar msozeau2008-05-30
* Cleanup build_new, remove unneeded try-with and debug interaction ofGravatar msozeau2008-05-20
* Fix globalization bug in class_tactics and refactorize instanceGravatar msozeau2008-05-19
* Fix caml debug flags configuration, -g works with the native compiler onlyGravatar msozeau2008-05-19
* Fix a de Bruijn bug in setoid_rewrite when rewriting underGravatar msozeau2008-05-17
* - Fix bug related to indices of fixpoints.Gravatar msozeau2008-05-13
* Correct a bug in "new auto" and also unify_eqn which did not do localGravatar msozeau2008-04-30
* - Backtrack sur option with_types suite à confusion sur l'utilisationGravatar herbelin2008-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
* - Add pretty-printers for Idpred, Cpred and transparent_state, used forGravatar msozeau2008-04-24
* 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
* 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
* 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
* Minor fixes: Gravatar msozeau2008-04-05
* Erreur ou acceptation silencieuce plutôt qu'avertissement systématique quandGravatar 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
* - Fix for rewriting under dependent products.Gravatar msozeau2008-03-31