aboutsummaryrefslogtreecommitdiff
path: root/pretyping/typeclasses.ml
AgeCommit message (Expand)Author
2016-11-03Lets Hints/Instances take an optional patternMatthieu Sozeau
2016-09-09Fast path in Clenvtac.clenv_refine typeclass resolution.Pierre-Marie Pédrot
2016-09-09Monomorphize a costly boolean equality operation.Pierre-Marie Pédrot
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-16Typeclasses:rename solve_instantiation* & use HookMatthieu Sozeau
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-03-20Pushing Proofview further down the dependency alley.Pierre-Marie Pédrot
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
2016-02-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-02-03More compact representation for evar resolvability flag.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11mergeMatej Kosik
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-12-31Do not compose List.length with List.filter.Guillaume Melquiond
2015-12-05Moving extended_rel_vect/extended_rel_list to the kernel.Hugo Herbelin
2015-10-02Univs: fix many evar_map initializations and leaks.Matthieu Sozeau
2015-02-16Fix bug #3960: potential evar instance categorized as an unresolvableMatthieu Sozeau
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-10-01Fixing new failure of #3017 after 012fe1a96ba81ab (Referring to evarsHugo Herbelin
2014-09-18For type classes, tell that VarInstance's behave like GoalEvar (avoid a loop ...Hugo Herbelin
2014-09-15Rework typeclass resolution and control of backtracking.Matthieu Sozeau
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-09-11Add a flag for restricting resolution of typeclasses toMatthieu Sozeau
2014-08-25instanciation is French, instantiation is EnglishJason Gross
2014-08-03Move to a representation of universe polymorphic constants using indices for ...Matthieu Sozeau
2014-06-17Existing Class now works with universe polymorphism. Fixes HoTT bug #063Matthieu Sozeau
2014-05-06- Fix treatment of global universe constraints which should be passed alongMatthieu Sozeau
2014-05-06Adapt universe polymorphic branch to new handling of futures for delayed proofs.Matthieu Sozeau
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-09-05Optimizing some evar_maps manipulation. In particular, using a [map] insteadppedrot
2013-08-25Actually using the domain function for maps.ppedrot
2013-08-01Added printing of instance priority to the Print Instances command.ppedrot
2013-06-12One more fix for rewrite: disallow resolving of the (partial) constraintsmsozeau
2013-05-14Delayed the computation of parameters in sort polymorphism ofherbelin
2013-05-14Replacing compatibility layer for Fmap in Typeclasses. Code wasppedrot
2013-05-14More semantical-friendly function.ppedrot
2013-05-12Use the Hook module here and there.ppedrot
2013-04-29Merging Context and Sign.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-04-22code simplifications concerning Summaryletouzey
2013-04-18Finer fix for bug 3017, mark unresolvability only of goals that aremsozeau
2013-04-03Fix for bug #3017: wrong handling of the unresolvability statusmsozeau
2013-03-22Fix bug# 2994, 2971 about better error messages.msozeau
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 12)letouzey
2013-03-12Allowing different types of, not to be mixed, generic Stores throughppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 13:21:42 +0000