aboutsummaryrefslogtreecommitdiff
path: root/tactics/class_tactics.ml4
AgeCommit message (Expand)Author
2008-08-22- New auto hints for transparency/opacity control, not bound to msozeau
2008-08-04Évolutions diverses et variées.herbelin
2008-07-28Fix bug in term dnet preventing some unifications. Allow "higher-order"msozeau
2008-07-26Even better test for choosing rewrite or setoid_rewrite.msozeau
2008-07-24A (safe) implementation of prolog's cut in the typeclasses eauto to avoidmsozeau
2008-07-22New tactics [conv] to test convertibility (actually, unification) of twomsozeau
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-07-02Stop using the discrimination net in typeclasses/setoid rewrite, which wasmsozeau
2008-06-27Enhanced discrimination nets implementation, which can now work withmsozeau
2008-06-18Fix bug in implementation of splitting of class constraints.msozeau
2008-06-18Compatibility fixes (Add Setoid bug and accidental introduction of amsozeau
2008-06-17Fixes w.r.t. let binders in class contexts and Add Parametricmsozeau
2008-06-17Better typeclass error messages, always giving the full set ofmsozeau
2008-06-11Optionally (and by default) split typeclasses evars into connected msozeau
2008-06-10- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)herbelin
2008-06-10- Correct handling of DependentMorphism error, using tclFAIL instead ofmsozeau
2008-06-07Correct handling of the environment in build_signature, and throwmsozeau
2008-06-07Change setoid_rewrite's matching semantics to continue matching insidemsozeau
2008-06-05Correctly catch UnresolvableConstraint exception which is now located. msozeau
2008-06-03Fixes incorrect handling of existing existentials variables inmsozeau
2008-05-30Improvements on coqdoc by adding more information into .globmsozeau
2008-05-20Cleanup build_new, remove unneeded try-with and debug interaction ofmsozeau
2008-05-19Fix globalization bug in class_tactics and refactorize instancemsozeau
2008-05-19Fix caml debug flags configuration, -g works with the native compiler onlymsozeau
2008-05-17Fix a de Bruijn bug in setoid_rewrite when rewriting undermsozeau
2008-05-13- Fix bug related to indices of fixpoints.msozeau
2008-04-30Correct a bug in "new auto" and also unify_eqn which did not do localmsozeau
2008-04-27- Backtrack sur option with_types suite à confusion sur l'utilisationherbelin
2008-04-26- Backtrack sur extension de syntaxe pour pose qui rentre en conflit avecherbelin
2008-04-26Debug implementation of failing tactics in Morphism to allow earliermsozeau
2008-04-24- Add pretty-printers for Idpred, Cpred and transparent_state, used formsozeau
2008-04-23Change default eauto depth to 100 in setoid_rewrite, bump necessarymsozeau
2008-04-21- Correct unification for the rewrite variant of setoid_rewrite,msozeau
2008-04-21- Parameterize unification by two sets of transparent_state, one for openmsozeau
2008-04-20Work on the "occurrences" tactic argument. It is now possible to passmsozeau
2008-04-17Bug squashing day !msozeau
2008-04-17Little fixes in setoid_rewrite.msozeau
2008-04-15More renamings to avoid clashes (e.g. with CoRN).msozeau
2008-04-15Document CHANGES in setoid rewrite, move DefaultRelation tomsozeau
2008-04-15- Add "Global" modifier for instances inside sections with the usualmsozeau
2008-04-14Renamings to avoid clashes with definitions in Relation_Definitions, nowmsozeau
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
2008-04-12Add the ability to specify what to do with free variables in instancemsozeau
2008-04-09Verify Setoid is loaded only if we're not in Coq.Classes.*. Add explicitmsozeau
2008-04-09Verify Setoid is loaded before doing anything.msozeau
2008-04-09Fix evar bugs in type classes:msozeau
2008-04-08- A little cleanup in Classes/*. Separate standard morphisms onmsozeau
2008-04-05Minor fixes: msozeau
2008-04-04Erreur ou acceptation silencieuce plutôt qu'avertissement systématique quandherbelin
2008-04-02Minor fixes. Use expanded type in class_tactics for Morphism search, tomsozeau