aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
Commit message (Expand)AuthorAge
* Useless use of maps in constr internalizing.Gravatar ppedrot2013-06-25
* Generalizing the use of maps instead of lists in the interpretationGravatar ppedrot2013-06-22
* Cutting the dependency of Genarg in constr_expr, glob_constrGravatar ppedrot2013-06-21
* Uniformizing generic argument types.Gravatar ppedrot2013-06-06
* Use definition_entry to declare local definitionsGravatar gareuselesinge2013-05-09
* A uniformization step around understand_* and interp_* functions.Gravatar herbelin2013-05-09
* States: frozen states can hold closuresGravatar gareuselesinge2013-05-06
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Indfun : use States.with_state_protection instead of freeze/unfreezeGravatar letouzey2013-04-23
* code simplifications concerning SummaryGravatar letouzey2013-04-22
* Revised infrastructure for lazy loading of opaque proofsGravatar letouzey2013-04-02
* Restrict (try...with...) to avoid catching critical exn (part 15)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 11)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 9)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 7)Gravatar letouzey2013-03-13
* Recdef: an anomaly isn't so anomalous, occurs in 1618.vGravatar letouzey2013-03-12
* invalid_arg instead of raise (Invalid_argement ...)Gravatar letouzey2013-03-12
* Allowing (Co)Fixpoint to be defined local and Let-style.Gravatar ppedrot2013-03-11
* Added a Local Definition vernacular command. This type of definitionGravatar ppedrot2013-03-11
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
* Dir_path --> DirPathGravatar letouzey2013-02-19
* use List.rev_map whenever possibleGravatar letouzey2013-02-18
* Minor code cleanups, especially take advantage of Dir_path.is_emptyGravatar letouzey2013-02-18
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of LabelGravatar ppedrot2012-12-18
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Moved Intset and Intmap to Int namespace.Gravatar ppedrot2012-12-14
* Taking into account the type of a definition (if it exists), and theGravatar herbelin2012-11-17
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
* correcting a little bug in FunctionGravatar jforest2012-10-31
* still some more dead code removalGravatar letouzey2012-10-06
* remove useless hidden_flag in TacMutual(Co)FixGravatar letouzey2012-10-06
* Moved Compat to parsing. This permits to break the dependency of theGravatar ppedrot2012-10-04
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Fixing a bug introduced in Funind plugin when reorganizing the CListGravatar ppedrot2012-09-24
* More cleaning in CArray...Gravatar ppedrot2012-09-18
* More cleaning on Utils and CList. Some parts of the code beingGravatar ppedrot2012-09-17
* Some documentation and cleaning of CList and Util interfaces.Gravatar ppedrot2012-09-15
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* Partial revert of Yann commit in order to use CLib.List when openingGravatar ppedrot2012-09-14
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Fixup for macOS 10.8 & Ocaml 4.0Gravatar pboutill2012-08-08
* Fixes r15610 (A new status Unsafe in Interface).Gravatar aspiwack2012-07-13