aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/implicit_quantifiers.mli
Commit message (Expand)AuthorAge
* CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* Fixing bug #3811: "Universe annotations confused inside generalizing binders".Gravatar Pierre-Marie Pédrot2015-07-29
* Update headers.Gravatar Maxime Dénès2015-01-12
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* More comments and less doublons in some mliGravatar pboutill2011-02-10
* More {raw => glob} changes for consistencyGravatar glondu2010-12-24
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Fix bug #2262: bad implicit argument number by avoiding countingGravatar msozeau2010-06-09
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Use generalizable variables info when internalizing arbitrary bindings,Gravatar msozeau2009-11-08
* Add a new vernacular command for controling implicit generalization ofGravatar msozeau2009-10-27
* Fix bug #2162 and a name clashing bug in generalized binders.Gravatar msozeau2009-10-09
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
* Open notation for declaring record instances.Gravatar msozeau2008-10-23
* Generalized implementation of generalization.Gravatar msozeau2008-10-23
* A much better implementation of implicit generalization:Gravatar msozeau2008-10-22
* Fixes in handling of implicit arguments:Gravatar msozeau2008-07-04
* Code cleanup in typeclasses, remove dead and duplicated code.Gravatar msozeau2008-06-21
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
* Do another pass on the typeclasses code. Correct globalization of classGravatar msozeau2008-03-19
* Move generally useful definition of nf_evar on contexts to evarutil.Gravatar msozeau2008-02-08
* Generalize instance declarations to any context, better name handling. Add ho...Gravatar msozeau2008-01-15
* Cleaner quantifiers for type classes, breaks clrewrite for the moment but imp...Gravatar msozeau2008-01-07
* Fix a naming bug reported by Arnaud Spiwack, allow instance search to create ...Gravatar msozeau2008-01-05
* Fix name capture bug and call the right pretyper in subtac.Gravatar msozeau2007-12-31
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31