aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
Commit message (Expand)AuthorAge
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Emilio Jesus Gallego Arias2018-02-28
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
* Merge PR #6767: [ci] add elpiGravatar Maxime Dénès2018-02-21
|\
* | Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.Gravatar Hugo Herbelin2018-02-20
| * pretyping: restore API understand_judgment_tcc (now understand_tcc_ty)Gravatar Enrico Tassi2018-02-19
|/
* Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ...Gravatar Maxime Dénès2018-02-19
|\
| * Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
* | Merge PR #6651: Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-02-12
|\ \ | |/ |/|
* | Reductionops.nf_* now take an environment.Gravatar Gaëtan Gilbert2018-02-02
* | Delete duplicate lineGravatar Paul Steckler2018-01-30
| * Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 11:58:54 +0000