aboutsummaryrefslogtreecommitdiff
path: root/pretyping/cases.ml
AgeCommit message (Expand)Author
2014-05-06Refresh some universes in cases.ml as they might appear in the term.Matthieu Sozeau
2014-05-06Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Yves Bertot
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-23Better representation of evar filters: we represent the vacuous filters ofPierre-Marie Pédrot
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2014-02-12TC: honor the use_typeclasses flag in pretypingEnrico Tassi
2013-12-06Fix test-suite/success/evars.v.Arnaud Spiwack
2013-11-27Adding generic solvers to term holes. For now, no resolution mechanism norPierre-Marie Pédrot
2013-11-02Fix compilation of pattern matching wrt variables: alias.aspiwack
2013-11-02Fix the compilation of pattern matching wrt to variables.aspiwack
2013-10-27Abstracting evar filter away. The API is not perfect, but better than nothing.ppedrot
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-24Turn many List.assoc into List.assoc_fletouzey
2013-10-23cList: set-as-list functions are now with an explicit comparisonletouzey
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 06:34:29 +0000