aboutsummaryrefslogtreecommitdiff
path: root/pretyping/cases.ml
AgeCommit message (Expand)Author
2013-05-11Fixing a source of evars leak, revealed by contrib QuicksortComplexityherbelin
2013-05-09Uniformization: isevars -> evdref/sigma/evdherbelin
2013-04-30Fix wrong computation of dependency signature in cases raising an uncaught ex...msozeau
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 12)letouzey
2013-03-12invalid_arg instead of raise (Invalid_argement ...)letouzey
2013-02-18Removing Exc_located and using the new exception enrichementppedrot
2013-02-18use List.rev_map whenever possibleletouzey
2013-02-10Splitted Evarutil in two filesppedrot
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-19Array.create is deprecatedpboutill
2012-12-18Modulification of nameppedrot
2012-12-17Fixed a bug in the algorithm trying to elaborate a "match" return predicate.herbelin
2012-12-14Modulification of identifierppedrot
2012-12-14Moved Intset and Intmap to Int namespace.ppedrot
2012-11-22Monomorphization (pretyping)ppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
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-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-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29Glob_term now mli-only, operations now in Glob_opsletouzey
2012-05-29Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evdletouzey
2012-05-11Impossible branches inference fixup (bug 2761)pboutill
2012-03-19Fix bugs related to Program integration.msozeau
2012-03-14Revise API of understand_ltac to be parameterized by a flag for resolution of...msozeau
2012-03-14Merge fixesmsozeau
2012-03-14Everything compiles again.msozeau
2012-03-14Second step of integration of Program:msozeau
2012-03-14Remove support for "abstract typing constraints" that requires unicity of sol...msozeau
2012-03-13A bit of cleaning: unifying push_rels and push_rel_context.herbelin
2012-03-02Glob_term.predicate_pattern: No number of parameters with letins.pboutill
2012-03-02Noise for nothingpboutill
2012-01-16Inductiveops.nb_*{,_env} cleaningpboutill
2011-12-16Introducing a notion of evar candidates to be used when an evar isherbelin
2011-12-04Fixed a small regression in pattern-matching compilation introduced inherbelin
2011-11-28Finally used typing to decide whether an alias needs to be expanded orherbelin
2011-11-28Fixing dependencies postprocessing bug in pattern-matching compilation.herbelin
2011-11-26Fixed a bug in postprocessing dependencies in pattern-matching compilationherbelin
2011-11-21Extend the computation of dependencies in pattern-matching compilationherbelin
2011-11-21Add matching on non-inductive types in building an inversion problemherbelin
2011-11-21Old naming bug in pattern-matching compilation: names in theherbelin
2011-11-21Inlining let-in (i.e. trace of aliases) in extract_predicate for whatherbelin
2011-11-21In pattern-matching compilation, now taking into account the dependenciesherbelin
2011-11-21Optimizing the compilation of unused aliases in pattern-matching.herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 22:40:02 +0000