aboutsummaryrefslogtreecommitdiff
path: root/interp/implicit_quantifiers.mli
AgeCommit message (Expand)Author
2015-10-13Fix some typos.Guillaume Melquiond
2015-07-29Fixing bug #3811: "Universe annotations confused inside generalizing binders".Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-04-29Merging Context and Sign.ppedrot
2012-12-18Modulification of nameppedrot
2012-12-14Modulification of identifierppedrot
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
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-02-10More comments and less doublons in some mlipboutill
2010-12-24More {raw => glob} changes for consistencyglondu
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
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-06-09Fix bug #2262: bad implicit argument number by avoiding countingmsozeau
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2009-11-08Use generalizable variables info when internalizing arbitrary bindings,msozeau
2009-10-27Add a new vernacular command for controling implicit generalization ofmsozeau
2009-10-09Fix bug #2162 and a name clashing bug in generalized binders.msozeau
2009-03-28Rewrite of Program Fixpoint to overcome the previous limitations: msozeau
2008-10-23Open notation for declaring record instances.msozeau
2008-10-23Generalized implementation of generalization.msozeau
2008-10-22A much better implementation of implicit generalization:msozeau
2008-07-04Fixes in handling of implicit arguments:msozeau
2008-06-21Code cleanup in typeclasses, remove dead and duplicated code.msozeau
2008-04-01Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientherbelin
2008-03-19Do another pass on the typeclasses code. Correct globalization of classmsozeau
2008-02-08Move generally useful definition of nf_evar on contexts to evarutil.msozeau
2008-01-15Generalize instance declarations to any context, better name handling. Add ho...msozeau
2008-01-07Cleaner quantifiers for type classes, breaks clrewrite for the moment but imp...msozeau
2008-01-05Fix a naming bug reported by Arnaud Spiwack, allow instance search to create ...msozeau
2007-12-31Fix name capture bug and call the right pretyper in subtac.msozeau
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau