aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/indfun.ml
Commit message (Expand)AuthorAge
* rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...Gravatar Pierre Letouzey2016-07-03
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
* Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
* Factorizing the uses of Declareops.safe_flags.Gravatar Pierre-Marie Pédrot2016-06-16
* Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\
| * Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
* | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* | merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\ \
* | | More conversion functions in the new tactic API.Gravatar Pierre-Marie Pédrot2016-02-15
| * | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
|/ /
* | CLEANUP: removing unused fieldGravatar Matej Kosik2016-01-11
* | CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedGravatar Matej Kosik2015-12-18
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-29
|\ \
| * | Univs: fix bug #4375, accept universe binders on (co)-fixpointsGravatar Matthieu Sozeau2015-10-28
| * | Do not pause globing in funind. (Fix bug #4382)Gravatar Guillaume Melquiond2015-10-28
* | | Type delayed_open_constr is now monotonic.Gravatar Pierre-Marie Pédrot2015-10-19
|/ /
* | Univs: fix after rebase (from_ctx/from_env)Gravatar Matthieu Sozeau2015-10-02
* | Univs: fix evar_map leaks bugs in FunctionGravatar Matthieu Sozeau2015-10-02
| * Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control assuming gua...Gravatar Arnaud Spiwack2015-09-25
* | Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
|/
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Function now supports puniveresGravatar jforest2015-04-14
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* handling Functional Scheme for required but not imported modulesGravatar Julien Forest2014-12-11
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* Fixing bug 3951Gravatar Julien Forest2014-09-22
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Experimentally adding an option for automatically erasing anGravatar Hugo Herbelin2014-08-05
* Better struture for Ltac internalization environments in Constrintern.Gravatar Pierre-Marie Pédrot2014-08-02
* Add a type of untyped term to Ltac's value.Gravatar Arnaud Spiwack2014-07-29
* 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
* Renaming new_induct -> induction; new_destruct -> destruct.Gravatar Hugo Herbelin2014-05-08
* Adapt universe polymorphic branch to new handling of futures for delayed proofs.Gravatar Matthieu Sozeau2014-05-06
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar 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
* Removing the need of evarmaps in constr internalization.Gravatar Pierre-Marie Pédrot2013-12-17
* Remove the Hiddentac module.Gravatar Arnaud Spiwack2013-11-25
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
* cList.index is now cList.index_f, same for index0Gravatar letouzey2013-10-23
* declaration_hooks use EphemeronGravatar gareuselesinge2013-10-18
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
* Removing more association lists in Constrintern.Gravatar ppedrot2013-09-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 20:56:56 +0000