aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/implicit_quantifiers.ml
Commit message (Expand)AuthorAge
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
* code simplifications concerning SummaryGravatar letouzey2013-04-22
* Implicit_quantifiers.is_freevar: cleaner, no more try...with _ ->...Gravatar letouzey2013-03-12
* Modulification of identifierGravatar ppedrot2012-12-14
* Monomorphization (interp)Gravatar ppedrot2012-11-25
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Replacing some str with strbrkGravatar ppedrot2012-06-04
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Basic stuff about constr_expr migrated from topconstr to constrexpr_opsGravatar letouzey2012-05-29
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* Add type annotations around all calls to Libobject.declare_objectGravatar letouzey2011-11-02
* Remove dynamic stuff from constr_expr and glob_constrGravatar glondu2011-10-28
* Fixpoints are traverse during implicits arguments search to toplevelGravatar 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
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
* Fix bug #2262: bad implicit argument number by avoiding countingGravatar msozeau2010-06-09
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Fix implicit_application for let-bound variables in the class context.Gravatar msozeau2010-01-28
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Use generalizable variables info when internalizing arbitrary bindings,Gravatar msozeau2009-11-08
* Misc fixes.Gravatar msozeau2009-11-06
* 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
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
* Move Record desugaring to constrintern and add ability to use notationsGravatar msozeau2008-11-05
* Open notation for declaring record instances.Gravatar msozeau2008-10-23
* Generalized implementation of generalization.Gravatar msozeau2008-10-23
* Fix bugs #1975 and #1976.Gravatar msozeau2008-10-22
* A much better implementation of implicit generalization:Gravatar msozeau2008-10-22
* Affichage des notations récursives:Gravatar herbelin2008-10-22
* Fix bug #1943 and restrict the inference optimisation of Program toGravatar msozeau2008-09-15
* Fixes in handling of implicit arguments:Gravatar msozeau2008-07-04
* Code cleanup in typeclasses, remove dead and duplicated code.Gravatar msozeau2008-06-21
* Fix "not an applied typeclass" error for legitimate classesGravatar msozeau2008-05-12