aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/indfun_common.ml
AgeCommit message (Expand)Author
2017-04-22Merge branch v8.6 into trunkHugo Herbelin
2017-04-04Solving first problem in bug #4306. TO DO : solve the let in problemJulien Forest
2017-04-04Merge branch 'trunk' into pr379Maxime Dénès
2017-03-24Replacing "cast surgery" in LetIn by a proper field (see PR #404).Hugo Herbelin
2017-02-14Funind API using EConstr.Pierre-Marie Pédrot
2017-02-14Equality API using EConstr.Pierre-Marie Pédrot
2016-09-22Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Maxime Dénès
2016-09-20Stylistic improvements in intf/decl_kinds.mli.Maxime Dénès
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Remove errorlabstrm in favor of user_errEmilio Jesus Gallego Arias
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-03-04Rename Ephemeron -> CEphemeron.Maxime Dénès
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-10-02Univs: fix evar_map leaks bugs in FunctionMatthieu Sozeau
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-04-14Function now supports puniveresjforest
2014-06-08Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofPierre-Marie Pédrot
2014-06-08Enforce a correct exception handling in declaration_hooksEnrico Tassi
2014-05-06Fix funind w.r.t. universesMatthieu Sozeau
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
2013-12-04Factoring(continued).Arnaud Spiwack
2013-12-04Refactoring: storing more information in the terminator closure.Arnaud Spiwack
2013-12-04The commands that initiate proofs are now in charge of what happens when proo...Arnaud Spiwack
2013-11-25Remove the Hiddentac module.Arnaud Spiwack
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-10-18declaration_hooks use Ephemerongareuselesinge
2013-08-22Less "Coq" strings everywhereletouzey
2013-08-08get rid of closures in global/proof stategareuselesinge
2013-05-09Use definition_entry to declare local definitionsgareuselesinge
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 9)letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 7)letouzey
2013-03-12invalid_arg instead of raise (Invalid_argement ...)letouzey
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-18Minor code cleanups, especially take advantage of Dir_path.is_emptyletouzey
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-18Modulification of Labelppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-01Getting rid of Pp.msgnl and Pp.message.ppedrot
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29Decl_kinds becomes a pure mli file, remaining ops in new file kindops.mlletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 09:06:43 +0000