aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* 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
* Proper implicit arguments handling for assumptionsGravatar msozeau2008-02-26
* Merge with lmamane's private branch:Gravatar lmamane2008-02-22
* Some bad emacs messup that was commited...Gravatar msozeau2008-02-14
* Backtrack changes on eauto, move specialized version of eauto inGravatar msozeau2008-02-14
* Move class_setoid to class_tactics.Gravatar msozeau2008-02-13
* Debugging of the class_setoid tactic and eauto. Prepare for move fromGravatar msozeau2008-02-13
* Essai de prise en compte de delta dans unify_0 (même sur termes non clos). Gravatar herbelin2008-02-13
* Granting wish 1794 (the name provided in the "using" clause of theGravatar herbelin2008-02-10
* Backport Program Instance into Instance. Proper early error message ifGravatar msozeau2008-02-10
* Fix the clrewrite tactic, change Relations.v to work on relations in PropGravatar msozeau2008-02-09
* Change implementation of resolution for typeclasses to use a customizedGravatar msozeau2008-02-08
* Add more information to IllFormedRecBody exceptions, to show the exactGravatar msozeau2008-02-08
* Mise en place d'une toute petite amélioration de l'unification deGravatar herbelin2008-02-07
* Suite 10518Gravatar herbelin2008-02-06
* Correction d'un bug à l'interprétation de "change" (on exigeait queGravatar herbelin2008-02-06
* New algorithm to resolve morphisms, after discussion with NicolasGravatar msozeau2008-02-06