aboutsummaryrefslogtreecommitdiff
path: root/toplevel/classes.ml
AgeCommit message (Expand)Author
2012-03-14Everything compiles again.msozeau
2012-03-02Noise for nothingpboutill
2011-12-12Proof using ...gareuselesinge
2011-11-17Merge subinstances branch by me and Tom Prince.msozeau
2011-10-07Fix bug #2557 and an issue with Propers for complementmsozeau
2011-06-30Keep obligation source information in Programmsozeau
2011-05-05Merge branch 'subclasses' into coq-trunkmsozeau
2011-04-18Add a flag to control betaiota reduction during unification to maintain backw...msozeau
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
2011-04-13- Make typeclass transparency information directly availablemsozeau
2011-04-13Add [Polymorphic] flag for defsmsozeau
2011-03-23- Fix solve_simpl_eqn which was cheking instances types in the wrong environm...msozeau
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
2011-02-14- Fix treatment of globality flag for typeclass instance hints (theymsozeau
2011-02-10Interp a definition with the implicit arguments of its local contextpboutill
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-10-07Fix bug# 2392msozeau
2010-09-28Fix bug #2321, allowing "_" named projections in classes. Not realizingmsozeau
2010-09-28Remove some occurrences of "open Termops"glondu
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-09-02* removed declare_constant and declare_internal_constant vsiles
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-29Correct wrong handling of evars in instance definitions that preventedmsozeau
2010-06-29Made tclABSTRACT normalize evars before saying it does not supportherbelin
2010-05-19Remove compile-command pragmas for emacsletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-27Fix bug #2245, incorrect handling of Context in sections inside modulemsozeau
2010-01-04Specific syntax for Instances in Module Type: Declare Instanceletouzey
2010-01-02Fix bug in last commit, missing a substitution call.msozeau
2010-01-01Fix handling of instance declarations in presence of let-ins (bugmsozeau
2009-12-27Fix "Existing Instance" to handle globality information and "Existingmsozeau
2009-11-15Fix [Instance: forall ..., C args := t] declarations to behave asmsozeau
2009-11-11Promote evar_defs to evar_map (in Evd)glondu
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-11-04Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.gmelquio
2009-10-28Integrate a few improvements on typeclasses and Program from the equations br...msozeau
2009-10-09Fix bug #2162 and a name clashing bug in generalized binders.msozeau
2009-10-05Correctly do backtracking during type class resolution even if only newmsozeau
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-14Backtrack on the forced discharge of type class variables introducedmsozeau
2009-07-07Jolification : tentative de supprimer les "( evd)" et associés quiaspiwack
2009-05-27Fix implicit args code so that declarations are added for allmsozeau
2009-05-27Stop using a "Manual Implicit Arguments" flag and support them as soonmsozeau
2009-05-16Minor fixes in typeclasses:msozeau
2009-05-09- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceherbelin
2009-04-08Some dead code removal + cleanupsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 21:00:30 +0000