aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Expand)Author
2013-03-19Removing the module Libtypes and unifying the Search[Pattern|Rewrite]?ppedrot
2013-03-15Extract_env : correct exceptions mentionned in a try ... withletouzey
2013-03-13Modules and ppvernac, sequel of Enrico's commit 16261letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 8)letouzey
2013-03-12Implicit_quantifiers.is_freevar: cleaner, no more try...with _ ->...letouzey
2013-03-12Restrict (try...with...) to avoid catching critical exn (part 3)letouzey
2013-03-12Hipattern : consider jmeq only when Logic.JMeq is loadedletouzey
2013-02-27Coqlib: minor simplificationsletouzey
2013-02-19Dir_path --> DirPathletouzey
2013-02-18use List.rev_map whenever possibleletouzey
2013-02-18Minor code cleanups, especially take advantage of Dir_path.is_emptyletouzey
2013-01-28Actually adding backtrace handling.ppedrot
2013-01-28Uniformization of the "anomaly" command.ppedrot
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2013-01-21Fix bug 2958: Inductive deep in in clause are impossiblepboutill
2013-01-18Unset Asymmetric Patternspboutill
2013-01-07Fixup notation printing in patternspboutill
2012-12-18Modulification of nameppedrot
2012-12-18Fixing parsing of specific primitive tokens used as notations for patternsherbelin
2012-12-17Fixed interpretation of "x" as a binding variable for the returnherbelin
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-12-14Implemented a full-fledged equality on [constr_expr]. By the way,ppedrot
2012-12-13Using library string functions.ppedrot
2012-12-13Renamed Option.Misc.compare to the more uniform Option.equal.ppedrot
2012-12-04Backtrack on activating scopes with type casts (was r15978).herbelin
2012-11-28Fix ocamldebug constr printerpboutill
2012-11-26Fixed a monomorphization error.ppedrot
2012-11-25Monomorphization (interp)ppedrot
2012-11-25More equality functionsppedrot
2012-11-23Added a constr_pattern_eqppedrot
2012-11-17Taking into account the type of a definition (if it exists), and theherbelin
2012-11-13More monomorphizationsppedrot
2012-11-13Added a CString module.ppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-10-31Change [Hints Resolve] to still accept constrs as argumentsmsozeau
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-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-09-09Fixed bug #2895ppedrot
2012-08-08Updating headers.herbelin
2012-07-30Bigint: avoid dependency over Ppletouzey
2012-07-21Fixing bug #2835 (the rationale for printing notations was notherbelin
2012-07-21Improving management of notations with binders (see #2708 where aherbelin
2012-07-20Fixup implicits in patterns & notationspboutill
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 12:03:19 +0000