aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2012-12-18Modulification of nameppedrot
2012-12-18Modulification of Labelppedrot
2012-12-18Taking into account the possibility of having a type of type which isherbelin
2012-12-18Fixed a little inefficiency of "set/destruct" over a pattern. Nowherbelin
2012-12-18Factorization of the elim unif flag with the default flag. Sinceherbelin
2012-12-17Do not display REVERTcast inserted by reduction tactics (unless printing all).herbelin
2012-12-17Fixed a bug in the algorithm trying to elaborate a "match" return predicate.herbelin
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-12-14Moved Intset and Intmap to Int namespace.ppedrot
2012-12-13Renamed Option.Misc.compare to the more uniform Option.equal.ppedrot
2012-12-08Finish patch for Hint Resolve, stopping to generate new constant names formsozeau
2012-11-28Evarconv: Fix #2936 + commentspboutill
2012-11-28Reductionops uses Closure.redspboutill
2012-11-26Removed some FIXME related to equality on universes.ppedrot
2012-11-26Small cleaning of interface in Univppedrot
2012-11-25More equality functionsppedrot
2012-11-25Fixed bug #2930: folded let-in's were hiding a violation to the occurherbelin
2012-11-23Added a constr_pattern_eqppedrot
2012-11-22Monomorphization (pretyping)ppedrot
2012-11-20Cleaning and small optimization in CList.ppedrot
2012-11-13Added a CString module.ppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-11-08Removing another bunch of generic equalitiesppedrot
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-26Change Hint Resolve, Immediate to take a global reference as argumentmsozeau
2012-10-17univ inconsistency error message gives evidence of a cyclebarras
2012-10-06Adapt pieces of code needing -rectypesletouzey
2012-10-04Improving error message when abtraction over goal (abstract_list_allherbelin
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-18More cleaning in CArray...ppedrot
2012-09-18More cleanup of Util: utf8 aspects moved to a new file unicode.mlletouzey
2012-09-18Cleaning interface of Util.ppedrot
2012-09-17More cleaning on Utils and CList. Some parts of the code beingppedrot
2012-09-15Some documentation and cleaning of CList and Util interfaces.ppedrot
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-09-14Partial revert of Yann commit in order to use CLib.List when openingppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-08-24correct some ends of .mllib files (avoid a broken tolink.ml)letouzey
2012-08-09Unification in Evar_conv uses an abstract machine statepboutill
2012-08-08Updating headers.herbelin
2012-08-07Avoid Pp.std_ppcmds in Misctypes.sort_infoletouzey
2012-07-29Fixing #2836 (materialize_evar might refine as a side effect theherbelin
2012-07-25Fix eta contraction in Reductionopspboutill
2012-07-20Reductionops refactoringpboutill
2012-07-20Fixing test-suitepboutill
2012-07-12flex_maybeflex factoringpboutill
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 22:59:38 +0000