aboutsummaryrefslogtreecommitdiff
path: root/interp/implicit_quantifiers.ml
AgeCommit message (Expand)Author
2015-07-29Fixing bug #3811: "Universe annotations confused inside generalizing binders".Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-09-17Revert specific syntax for primitive projections, avoiding uglyMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-24Turn many List.assoc into List.assoc_fletouzey
2013-04-22code simplifications concerning Summaryletouzey
2013-03-12Implicit_quantifiers.is_freevar: cleaner, no more try...with _ ->...letouzey
2012-12-14Modulification of identifierppedrot
2012-11-25Monomorphization (interp)ppedrot
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-04Replacing some str with strbrkppedrot
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29Basic stuff about constr_expr migrated from topconstr to constrexpr_opsletouzey
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-03-02Noise for nothingpboutill
2011-11-02Add type annotations around all calls to Libobject.declare_objectletouzey
2011-10-28Remove dynamic stuff from constr_expr and glob_constrglondu
2011-02-10Fixpoints are traverse during implicits arguments search to toplevelpboutill
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-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-22Extension of the recursive notations mechanismherbelin
2010-06-09Fix bug #2262: bad implicit argument number by avoiding countingmsozeau
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-01-28Fix implicit_application for let-bound variables in the class context.msozeau
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
2009-11-08Use generalizable variables info when internalizing arbitrary bindings,msozeau
2009-11-06Misc fixes.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-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-03-28Rewrite of Program Fixpoint to overcome the previous limitations: msozeau
2009-02-19On remplace evar_map par evar_defs (seul evar_defs est désormais exporté aspiwack
2008-11-05Move Record desugaring to constrintern and add ability to use notationsmsozeau
2008-10-23Open notation for declaring record instances.msozeau
2008-10-23Generalized implementation of generalization.msozeau
2008-10-22Fix bugs #1975 and #1976.msozeau
2008-10-22A much better implementation of implicit generalization:msozeau
2008-10-22Affichage des notations récursives:herbelin
2008-09-15Fix bug #1943 and restrict the inference optimisation of Program tomsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:58:57 +0000