aboutsummaryrefslogtreecommitdiff
path: root/toplevel/classes.ml
AgeCommit message (Expand)Author
2013-08-01Granting bug #3098: adding priority to Existing Instances.ppedrot
2013-05-12Use the Hook module here and there.ppedrot
2013-05-09A uniformization step around understand_* and interp_* functions.herbelin
2013-05-08Declaration of multiple hypotheses or parameters now share typingherbelin
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-03-13Modules and ppvernac, sequel of Enrico's commit 16261letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 13)letouzey
2013-03-12invalid_arg instead of raise (Invalid_argement ...)letouzey
2013-03-11Added a Local Definition vernacular command. This type of definitionppedrot
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-12-18Modulification of nameppedrot
2012-12-18Modulification of Labelppedrot
2012-12-14Modulification of identifierppedrot
2012-12-08Finish patch for Hint Resolve, stopping to generate new constant names formsozeau
2012-11-26Monomorphization (toplevel)ppedrot
2012-10-26Change Hint Resolve, Immediate to take a global reference as argumentmsozeau
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-24Assumption commands are now displayed as unsafe in Coqide.aspiwack
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-21Fix bug #2808: wrong handling of evars in Instance command.msozeau
2012-06-04Forward-port fixes from 8.4 (15358, 15353, 15333).msozeau
2012-05-30Getting rid of Pp.msgppedrot
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-05-29Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evdletouzey
2012-03-20Fix interface of resolve_typeclasses: onlyargs -> with_goals:msozeau
2012-03-19Fix bugs related to Program integration.msozeau
2012-03-14Final part of moving Program code inside the main code. Adapted add_definitio...msozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-27 02:56:38 +0000