aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
AgeCommit message (Expand)Author
2013-05-09Use definition_entry to declare local definitionsgareuselesinge
2013-05-09A uniformization step around understand_* and interp_* functions.herbelin
2013-05-06States: frozen states can hold closuresgareuselesinge
2013-04-29Merging Context and Sign.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-04-23Indfun : use States.with_state_protection instead of freeze/unfreezeletouzey
2013-04-22code simplifications concerning Summaryletouzey
2013-04-02Revised infrastructure for lazy loading of opaque proofsletouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 15)letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 11)letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 9)letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 7)letouzey
2013-03-12Recdef: an anomaly isn't so anomalous, occurs in 1618.vletouzey
2013-03-12invalid_arg instead of raise (Invalid_argement ...)letouzey
2013-03-11Allowing (Co)Fixpoint to be defined local and Let-style.ppedrot
2013-03-11Added a Local Definition vernacular command. This type of definitionppedrot
2013-02-26kernel/declarations becomes a pure mliletouzey
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-28Uniformization of the "anomaly" command.ppedrot
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-12-18Modulification of nameppedrot
2012-12-18Modulification of Labelppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-12-14Moved Intset and Intmap to Int namespace.ppedrot
2012-11-17Taking into account the type of a definition (if it exists), and theherbelin
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-10-31correcting a little bug in Functionjforest
2012-10-06still some more dead code removalletouzey
2012-10-06remove useless hidden_flag in TacMutual(Co)Fixletouzey
2012-10-04Moved Compat to parsing. This permits to break the dependency of theppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-24Fixing a bug introduced in Funind plugin when reorganizing the CListppedrot
2012-09-18More cleaning in CArray...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-08Updating headers.herbelin
2012-08-08Fixup for macOS 10.8 & Ocaml 4.0pboutill
2012-07-13Fixes r15610 (A new status Unsafe in Interface).aspiwack
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-01More cleaningppedrot
2012-06-01Getting rid of Pp.msgnl and Pp.message.ppedrot
2012-05-30Getting rid of Pp.msgppedrot