aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/class_tactics.ml4
Commit message (Expand)AuthorAge
...
* Quick fix for references to section variables unbound in the currentGravatar msozeau2010-01-26
* Opened the possibility to type Ltac patterns but it is not fully functional yetGravatar herbelin2009-12-24
* Backtrack on making exact hints for lemmas starting with productsGravatar msozeau2009-12-19
* Turn evars created by a tactic application into a subgoal immediately inGravatar msozeau2009-12-06
* Fix anomaly when using typeclass resolution with filtered hyps in evars.Gravatar msozeau2009-12-06
* Fix make_exact_entry to allow applying [forall x, P x] hints directly,Gravatar msozeau2009-12-01
* Fix bug in typeclass resolution. Better handling of universes inGravatar msozeau2009-12-01
* Fix backtracking heuristic in typeclass resolution. Gravatar msozeau2009-11-30
* Substitute terms for evars-as-goals as soon as they are solved inGravatar msozeau2009-11-27
* Minor fixes in typeclasses, avoiding repeated evar normalizations.Gravatar msozeau2009-11-24
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* Fixes around typeclasses:Gravatar msozeau2009-10-27
* Fix bug in typeclass resolution discoverd by Eeelis van der Weegen:Gravatar msozeau2009-10-15
* Correctly do backtracking during type class resolution even if only newGravatar msozeau2009-10-05
* Removal of trailing spaces.Gravatar serpyc2009-10-04
* Better use of transparency information for local hypotheses: Gravatar msozeau2009-09-22
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Fix the bug-ridden code used to choose leibniz or generalizedGravatar msozeau2009-09-08
* Use the proper unification flags in e_exact. This makes exact fail a bitGravatar msozeau2009-07-09
* Reactivation of pattern unification of evars in apply unification, inGravatar herbelin2009-07-08
* Jolification : tentative de supprimer les "( evd)" et associés quiGravatar aspiwack2009-07-07
* Fix "unsatisfiable constraints" error messages to include all theGravatar msozeau2009-06-18
* Use a lazy value for the message in FailError, so that it won't beGravatar msozeau2009-06-11
* When typing a non-dependent arrow, do not put the (anonymous) variableGravatar msozeau2009-06-11
* Do a fixpoint on the result of typeclass search to force theGravatar msozeau2009-06-08
* Minor unification changes:Gravatar msozeau2009-05-18
* Minor fixes in typeclasses:Gravatar msozeau2009-05-16
* - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceGravatar herbelin2009-05-09
* Improvements in typeclasses eauto and generalized rewriting:Gravatar msozeau2009-05-05
* Fixes for bugs in r12110:Gravatar msozeau2009-04-28
* Cleanup old eauto code.Gravatar msozeau2009-04-27
* - Implementation of a new typeclasses eauto procedure based on successGravatar msozeau2009-04-27
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* Move setoid_rewrite to its own module and do some clean up inGravatar msozeau2009-04-07
* Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"Gravatar herbelin2009-03-16
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
* pushed evar reduction in kernelGravatar barras2009-02-06
* Fix bug #2004 due to bad handling of evars in the unification for Gravatar msozeau2009-01-21
* Various little fixes:Gravatar msozeau2009-01-18
* Fix a bunch of bugs related to setoid_rewrite, unification and evars:Gravatar msozeau2009-01-12
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* - Another bug in get_sort_family_of (sort-polymorphism of constants andGravatar herbelin2008-12-28
* - Optimized "auto decomp" which had a (presumably) exponential inGravatar herbelin2008-12-26
* Fix looping class resolution bug discovered by B. Aydemir and use theGravatar msozeau2008-12-14
* Do not catch _all_ exceptions in setoid unification.Gravatar msozeau2008-12-04
* Fix bug reported by Mark Dickinson on Coq-Club about [setoid_rewrite] notGravatar msozeau2008-11-10
* More factorization of inductive/record and typeclasses: move classGravatar msozeau2008-11-09
* Port [rewrite] tactics to open terms. Currently no check that evarsGravatar msozeau2008-11-05
* Backtrack sur commit 11467 (tentative d'optimisation meta_instance quiGravatar herbelin2008-10-26
* Generalized implementation of generalization.Gravatar msozeau2008-10-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 14:05:28 +0000