aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/class_tactics.ml4
Commit message (Expand)AuthorAge
* 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
* 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
* Compatibility fixes, backtrack on definitions of reflexive,Gravatar msozeau2008-03-22
* Add a flag to control rewriting under lambdas. Otherwise makes someGravatar msozeau2008-03-20
* Do another pass on the typeclasses code. Correct globalization of classGravatar msozeau2008-03-19