aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evd.ml
AgeCommit message (Expand)Author
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-09-05Optimizing some evar_maps manipulation. In particular, using a [map] insteadppedrot
2013-09-05Cleaning up of Evd. Extruding the tower of modules used to define evar_maps.ppedrot
2013-09-03Partly replacing list-based access functions in Evd. This is stillppedrot
2013-08-25Actually using the domain function for maps.ppedrot
2013-08-08State Transaction Machinegareuselesinge
2013-08-04Removing now useless merging primitives from Evd.ppedrot
2013-08-03Small fixes due to the arrival of OCaml 3.12.ppedrot
2013-05-06Small cleaning of Evd interface.ppedrot
2013-05-03Removing a redundant function from Evd.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-03-12A version of Univ.check_eq with no anomaly for Evd.set_eq_sortletouzey
2013-03-12Allowing different types of, not to be mixed, generic Stores throughppedrot
2013-02-17Locating errors from consider_remaining_unif_problems if possibleherbelin
2013-01-29Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_envherbelin
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-18Modulification of nameppedrot
2012-12-14Moved Intset and Intmap to Int namespace.ppedrot
2012-11-26Removed some FIXME related to equality on universes.ppedrot
2012-11-26Small cleaning of interface in Univppedrot
2012-11-22Monomorphization (pretyping)ppedrot
2012-11-20Cleaning and small optimization in CList.ppedrot
2012-11-03Reversed roles of undefined/defined evars in Evd, thus saving preciousppedrot
2012-10-29Removed many calls to OCaml generic equality. This was done byppedrot
2012-10-17univ inconsistency error message gives evidence of a cyclebarras
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-15Some documentation and cleaning of CList and Util interfaces.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-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evdletouzey
2012-03-22Univ: enforce_leq instead of enforce_geq for more uniformityletouzey
2012-03-20Generalized the use of evar candidates in type inference unification:herbelin
2012-03-02Noise for nothingpboutill
2011-12-17Added ability to take the type of applied metas into account whenherbelin
2011-12-16Introducing a notion of evar candidates to be used when an evar isherbelin
2011-10-26When checking for emptiness, use Foo.is_empty instead of (=) Foo.emptyletouzey
2011-10-25Continuing r14585 (ill-typed restriction bug).herbelin
2011-10-22Fixing uncaught exception in pr_evar_map (pr_global failed for unknown global...herbelin
2011-10-11More on r14536 (an unused pattern-matching remained in the commit).herbelin
2011-10-10Little code simplification of instantiate_evar in evd.mlherbelin
2011-10-10Added information about evar origin in pretty-printing evd for debugherbelin
2011-10-10Passed conv_algo to evar_define and move call to solve_refl toherbelin
2011-08-02More robust evar_map debugging printerherbelin
2011-06-21Cleaning debugging printer relative to new proof engine. Inherbelin
2011-06-12Added a new flag for freezing evars in tactic unification. Used thisherbelin
2011-05-13A better procedure for checking presence of undefined evars.aspiwack
2011-05-04First phase removing obsolete support for eta up to conversion inherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 16:02:35 +0000