aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
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
2012-07-12miller_pfenning unification code factoringpboutill
2012-07-12flex_kind_of_term does not have a copy of termpboutill
2012-07-12evar reduction is already made by whd_*pboutill
2012-07-12tacred uses stack_reduction_function instead of state_reduction_functionpboutill
2012-07-11Fix regression introduced in r15418 that broke MathClasses. In program mode, ...msozeau
2012-07-10Another correction to the dependent existential variable printingaspiwack
2012-07-06Continuing r15459: it helps testing occur-check early in someherbelin
2012-07-06Practical fix for bug #1206 (anomaly raised in pretyping instead ofherbelin
2012-07-06Fixes bug #2678aspiwack
2012-06-28Cleaning opening of the standard List module.ppedrot
2012-06-25Added a .mli to pretyping/program.mlppedrot
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-21Fix bug #2791 by doing a fixpoint computation in consider_remaining_problems:msozeau
2012-06-20Fixing use of an error instead of a boolean result in the unificationherbelin
2012-06-20Fixing bug #2817 (occur check was not done up to instantiation ofherbelin
2012-06-15Reductionops abstract machine uses Zcase & Zfix stack node.pboutill
2012-06-15Reductionops : Better abstract machine stack utilitiespboutill
2012-06-04Replacing some str with strbrkppedrot
2012-06-04Forward-port fixes from 8.4 (15358, 15353, 15333).msozeau
2012-06-01More cleaningppedrot
2012-06-01Cleaning Pp.ppnl useppedrot
2012-05-30More uniformisation in Pp.warn functions.ppedrot
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
2012-05-29No more Univ in grammar.cmaletouzey
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29Pattern as a mli-only file, operations in Patternopsletouzey
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-05-29Glob_term now mli-only, operations now in Glob_opsletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-05-29Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evdletouzey
2012-05-11Impossible branches inference fixup (bug 2761)pboutill