aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* - 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
* 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
* Implementation of rewriting under lambdas. Tested on exists only.Gravatar msozeau2008-03-18
* Added a function to rebuild an elim scheme from elim_scheme_info. WillGravatar courtieu2008-03-18
* Correct implementation of normalization of signatures using setoidGravatar msozeau2008-03-18
* Add the possibility of specifying constants to unfold for typeclassGravatar msozeau2008-03-17
* Using the "relation" constant made some unifications fail in the newGravatar msozeau2008-03-16
* Reorganize Program and Classes theories. Requiring Setoid no longer setsGravatar msozeau2008-03-16
* Minor fixes on setoid rewriting. Now uses definitions of [relation] andGravatar msozeau2008-03-16
* Application de refresh_universes dans typing.ml et retyping.ml : lesGravatar herbelin2008-03-15
* Pas très propre de reposer sur la capture des anomalies (et celaGravatar herbelin2008-03-10
* Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)Gravatar herbelin2008-03-10
* Fix compilation problem and finish little cleanup.Gravatar msozeau2008-03-10
* Add a missing morphism declaration that turns morphisms on R ==> R' toGravatar msozeau2008-03-09
* New implementation of Add Relation as a DefaultRelation instanceGravatar msozeau2008-03-08
* correction d'un bug d'efficacite dans Function (+ ajout de eauto_with_bases)Gravatar jforest2008-03-08
* Fix bugs that were reopened due to the change of setoidGravatar msozeau2008-03-08
* f_equal, revert, specialize in ML, contradict in better Ltac (+doc)Gravatar letouzey2008-03-07
* Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As partGravatar msozeau2008-03-07
* typo in last commit (?)Gravatar letouzey2008-03-06
* Plug the new setoid implemtation in, leaving the original one commentedGravatar msozeau2008-03-06
* Syntax changes in typeclasses, remove "?" for usual implicit argumentsGravatar msozeau2008-03-06
* Rework on rich forms of rewriteGravatar letouzey2008-03-01