aboutsummaryrefslogtreecommitdiff
path: root/toplevel/classes.ml
AgeCommit message (Expand)Author
2016-11-07Fixes to compile with ocaml 4.01Matthieu Sozeau
2016-11-03Lets Hints/Instances take an optional patternMatthieu Sozeau
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-04-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-07Allow to unset the refinement mode of Instance in MLMatthieu Sozeau
2016-03-20Making Evarutil independent from Reductionops.Pierre-Marie Pédrot
2016-03-20Moving Refine to its proper module.Pierre-Marie Pédrot
2016-03-14Typeclasses: respect Declare Instance priorityMatthieu Sozeau
2016-02-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-19Fixing bug #4580: [Set Refine Instance Mode] also used for Program Instance.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-29Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-23Implement support for universe binder lists in Instance and Program Fixpoint/...Matthieu Sozeau
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: removing unused fieldMatej Kosik
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-11-20Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-19Allow program hooks to see the refined universe_context at the end of aMatthieu Sozeau
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-28Univs: local names handling.Matthieu Sozeau
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-10-18Constraining refine to monotonic functions.Pierre-Marie Pédrot
2015-10-02Univs: fix many evar_map initializations and leaks.Matthieu Sozeau
2015-09-23Hopefully better names to constructors of internal_flag, as discussedHugo Herbelin
2015-04-09Fix declarations of instances to perform restriction of universeMatthieu Sozeau
2015-02-18Fix bug #4046.Matthieu Sozeau
2015-02-16Fix bug #3960: potential evar instance categorized as an unresolvableMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-12-29Fixing bug #3632 for good.Pierre-Marie Pédrot
2014-11-30Adding a Refine Instance Mode option that allows to deactivate thePierre-Marie Pédrot
2014-10-23Evd.future_goals: forgot to revert the list in two places.Arnaud Spiwack
2014-10-22Proofview: move more functions to the Unsafe module.Arnaud Spiwack
2014-10-22Remove the deprecated open-constr based refine.Arnaud Spiwack
2014-10-22Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Arnaud Spiwack
2014-10-07Splitting out of auto.ml a file hints.ml dedicated to hints so as toHugo Herbelin
2014-09-30Add syntax for naming new goals in refine: writing ?[id] instead of _Hugo Herbelin
2014-09-15Rework typeclass resolution and control of backtracking.Matthieu Sozeau
2014-09-12Uniformisation of the order of arguments env and sigma.Hugo Herbelin
2014-06-23Proper handling of the polymorphism flag for Context, fixing HoTT bug #98.Matthieu Sozeau
2014-06-18Proofs now take and return an evar_universe_context, simplifying interfacesMatthieu Sozeau
2014-06-11Fix bug #3289Matthieu Sozeau
2014-06-10- Fix substitution of universes which needlessly hashconsed existing universes.Matthieu Sozeau
2014-06-08Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofPierre-Marie Pédrot
2014-06-08Enforce a correct exception handling in declaration_hooksEnrico Tassi
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Fix context forgetting universes (temporary, the fix is not exactly right).Matthieu Sozeau
2014-05-06Various fixes of universe polymorphism and projections when they're set.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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 11:06:49 +0000