aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/indfun_common.ml
Commit message (Expand)AuthorAge
* [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
* Remove the function Global.type_of_global_unsafe.Gravatar Pierre-Marie Pédrot2017-07-13
* Merge PR#763: [proof] Deprecate redundant wrappers.Gravatar Maxime Dénès2017-06-14
|\
| * [proof] Deprecate redundant wrappers.Gravatar Emilio Jesus Gallego Arias2017-06-11
* | Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
|/
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* Merge PR#512: [cleanup] Unify all calls to the error function.Gravatar Maxime Dénès2017-05-29
|\
| * [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* | [coqlib] Move `Coqlib` to `library/`.Gravatar Emilio Jesus Gallego Arias2017-05-27
* | [coqlib] Deprecate redundant Coqlib functions.Gravatar Emilio Jesus Gallego Arias2017-05-27
|/
* Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\
* \ Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \
| | * [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| |/
| * Fix 4.04 warningsGravatar Gaetan Gilbert2017-04-27
| * Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* | [location] [ast] Port module AST to CAstGravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Switch glob_constr to Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-24
|/
* Merge branch v8.6 into trunkGravatar Hugo Herbelin2017-04-22
|\
| * Solving first problem in bug #4306. TO DO : solve the let in problemGravatar Julien Forest2017-04-04
* | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
|\ \
| * | Replacing "cast surgery" in LetIn by a proper field (see PR #404).Gravatar Hugo Herbelin2017-03-24
* | | Funind API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Equality API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|/ /
* | Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Gravatar Maxime Dénès2016-09-22
* | Stylistic improvements in intf/decl_kinds.mli.Gravatar Maxime Dénès2016-09-20
* | Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
* | Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
|/
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Rename Ephemeron -> CEphemeron.Gravatar Maxime Dénès2016-03-04
* Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
* Univs: fix evar_map leaks bugs in FunctionGravatar Matthieu Sozeau2015-10-02
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Function now supports puniveresGravatar jforest2015-04-14
* Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofGravatar Pierre-Marie Pédrot2014-06-08
* Enforce a correct exception handling in declaration_hooksGravatar Enrico Tassi2014-06-08
* Fix funind w.r.t. universesGravatar Matthieu Sozeau2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Factoring(continued).Gravatar Arnaud Spiwack2013-12-04
* Refactoring: storing more information in the terminator closure.Gravatar Arnaud Spiwack2013-12-04
* The commands that initiate proofs are now in charge of what happens when proo...Gravatar Arnaud Spiwack2013-12-04
* Remove the Hiddentac module.Gravatar Arnaud Spiwack2013-11-25
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
* declaration_hooks use EphemeronGravatar gareuselesinge2013-10-18
* Less "Coq" strings everywhereGravatar letouzey2013-08-22
* get rid of closures in global/proof stateGravatar gareuselesinge2013-08-08
* Use definition_entry to declare local definitionsGravatar gareuselesinge2013-05-09
* code simplifications concerning SummaryGravatar letouzey2013-04-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 17:46:01 +0000