aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
Commit message (Expand)AuthorAge
* Reductionops.nf_* now take an environment.Gravatar Gaëtan Gilbert2018-02-02
* Delete duplicate lineGravatar Paul Steckler2018-01-30
* Remove dead code from funind.Gravatar Maxime Dénès2018-01-24
* [vernac] vernac_expr no longer recursiveGravatar Vincent Laporte2018-01-08
* [API] remove large file containing duplicate interfacesGravatar Enrico Tassi2017-12-27
* [api] Also deprecate constructors of Decl_kinds.Gravatar Emilio Jesus Gallego Arias2017-12-23
* Separate vernac controls and regular commands.Gravatar Maxime Dénès2017-12-20
* Merge PR #6419: [vernac] Split `command.ml` into separate files.Gravatar Maxime Dénès2017-12-18
|\
* \ Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.Gravatar Maxime Dénès2017-12-18
|\ \
| | * [flags] Make program_mode a parameter for commands in vernac.Gravatar Emilio Jesus Gallego Arias2017-12-17
| | * [vernac] Split `command.ml` into separate files.Gravatar Emilio Jesus Gallego Arias2017-12-17
| |/
| * [econstr] Switch constrintern API to non-imperative style.Gravatar Emilio Jesus Gallego Arias2017-12-15
* | Merge PR #978: In printing, experimenting factorizing "match" clauses with sa...Gravatar Maxime Dénès2017-12-14
|\ \ | |/ |/|
| * In printing, factorizing "match" clauses with same right-hand side.Gravatar Hugo Herbelin2017-12-12
* | Getting rid of pf_is_matching in Funind.Gravatar Pierre-Marie Pédrot2017-12-06
|/
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 22:42:11 +0000