aboutsummaryrefslogtreecommitdiff
path: root/toplevel/classes.mli
AgeCommit message (Expand)Author
2017-02-15[stm] Break stm/toplevel dependency loop.Emilio Jesus Gallego Arias
2016-11-03Lets Hints/Instances take an optional patternMatthieu Sozeau
2016-04-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-07Allow to unset the refinement mode of Instance in MLMatthieu Sozeau
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: kernel/context.ml{,i}Matej Kosik
2015-04-09Fix declarations of instances to perform restriction of universeMatthieu Sozeau
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-10-22Remove the deprecated open-constr based refine.Arnaud Spiwack
2014-09-15Rework typeclass resolution and control of backtracking.Matthieu Sozeau
2014-06-23Proper handling of the polymorphism flag for Context, fixing HoTT bug #98.Matthieu Sozeau
2014-06-11Fix bug #3289Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-08-08State Transaction Machinegareuselesinge
2013-08-01Granting bug #3098: adding priority to Existing Instances.ppedrot
2013-04-29Merging Context and Sign.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2012-12-14Modulification of identifierppedrot
2012-08-24Assumption commands are now displayed as unsafe in Coqide.aspiwack
2012-08-08Updating headers.herbelin
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-03-02Noise for nothingpboutill
2011-11-17Merge subinstances branch by me and Tom Prince.msozeau
2011-05-05Merge branch 'subclasses' into coq-trunkmsozeau
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
2011-04-13Add [Polymorphic] flag for defsmsozeau
2011-03-13- Add modulo_delta_types flag for unification to allow fullmsozeau
2011-03-11Keep information on which fields are subclasses in class declarations,msozeau
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2010-01-04Specific syntax for Instances in Module Type: Declare Instanceletouzey
2009-12-27Fix "Existing Instance" to handle globality information and "Existingmsozeau
2009-10-28Integrate a few improvements on typeclasses and Program from the equations br...msozeau
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-11-09More factorization of inductive/record and typeclasses: move classmsozeau
2008-10-23Generalized implementation of generalization.msozeau
2008-07-07- Improve [Context] vernacular to allow arbitrary binders, not justmsozeau
2008-07-04Fixes in handling of implicit arguments:msozeau
2008-06-21Code cleanup in typeclasses, remove dead and duplicated code.msozeau
2008-05-30Improvements on coqdoc by adding more information into .globmsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 04:33:13 +0000