aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
Commit message (Expand)AuthorAge
* Remove "obsolete_locality" and fix STM vernac classification.Gravatar Maxime Dénès2017-11-29
* Use Entries.constant_universes_entry more.Gravatar Gaëtan Gilbert2017-11-24
* Stop exposing UState.universe_context and its Evd wrapper.Gravatar Gaëtan Gilbert2017-11-24
* Separate checking univ_decls and obtaining universe binder names.Gravatar Gaëtan Gilbert2017-11-24
* [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
* [printing] Deprecate all printing functions accessing the global proof.Gravatar Emilio Jesus Gallego Arias2017-11-21
* Merge PR #6181: [proof] Attempt to deprecate some V82 parts of the proof API.Gravatar Maxime Dénès2017-11-21
|\
* | [plugins] Prepare plugin API for functional handling of state.Gravatar Emilio Jesus Gallego Arias2017-11-19
| * [proof] Attempt to deprecate some V82 parts of the proof API.Gravatar Emilio Jesus Gallego Arias2017-11-19
|/
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Using a specific function to register vernac printers.Gravatar Hugo Herbelin2017-11-02
* Passing around the flag for injection so that tactics calling inj atGravatar Hugo Herbelin2017-10-26
* [stm] Remove state-handling from Futures.Gravatar Emilio Jesus Gallego Arias2017-10-17
* Merge PR #1040: Efficient fresh name generationGravatar Maxime Dénès2017-10-03
|\
* | [vernac] Remove `Qed exporting` syntax.Gravatar Emilio Jesus Gallego Arias2017-09-29
| * Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
|/
* Don't lose names in UState.universe_context.Gravatar Gaëtan Gilbert2017-09-19
* Parse directly to Sorts.family when appropriate.Gravatar Gaëtan Gilbert2017-09-08
* Making detyping potentially lazy.Gravatar Pierre-Marie Pédrot2017-09-04
* Merge PR #912: Detyping functions are now operating on EConstr.t.Gravatar Maxime Dénès2017-08-16
|\
* \ Merge PR #864: Some cleanups after cumulativity for inductive typesGravatar Maxime Dénès2017-08-16
|\ \
| | * Detyping functions are now operating on EConstr.t.Gravatar Pierre-Marie Pédrot2017-08-01
| |/ |/|
* | Merge PR #806: closing bug 5315Gravatar Maxime Dénès2017-08-01
|\ \
| | * Improve errors for cumulativity when monomorphicGravatar Amin Timany2017-07-31
* | | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadGravatar Maxime Dénès2017-07-31
|\ \ \ | |_|/ |/| |
| | * closing bug 5315Gravatar Julien Forest2017-07-29
| |/ |/|
| * deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* | Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
|/
* [api] Remove type equalities from API.Gravatar Emilio Jesus Gallego Arias2017-07-25
* [funind] Remove spurious character in comment.Gravatar Emilio Jesus Gallego Arias2017-07-17
* [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
* Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.Gravatar Pierre-Marie Pédrot2017-07-13
* Safer API for Global.body_of_constant and variants.Gravatar Pierre-Marie Pédrot2017-07-13
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* closing bug #5618 introduce by PR 828Gravatar Julien Forest2017-06-29
* closing bug #4250Gravatar Julien Forest2017-06-23
* Merge PR#803: Clean ssrGravatar Maxime Dénès2017-06-20
|\
| * Removing Proof_type from the API.Gravatar Pierre-Marie Pédrot2017-06-16
* | Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
|/
* Merge PR#763: [proof] Deprecate redundant wrappers.Gravatar Maxime Dénès2017-06-14
|\
* \ Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Maxime Dénès2017-06-14
|\ \
* | | Recdef do now a Require Export FunInd (better compat)Gravatar Pierre Letouzey2017-06-14
* | | Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
* | | Merge PR#718: API cleanup: aliasesGravatar Maxime Dénès2017-06-12
|\ \ \
| | | * [proof] Deprecate redundant wrappers.Gravatar Emilio Jesus Gallego Arias2017-06-11
| |_|/ |/| |
* | | Remove remaining vo.itarget files (obsolete since PR #499)Gravatar Pierre Letouzey2017-06-10
| * | Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
|/ /
| * A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Hugo Herbelin2017-06-09
|/
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 00:36:15 +0000