aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
Commit message (Expand)AuthorAge
* Correct some spelling errorsmasterGravatar Benjamin Barenblat2018-07-22
* [build] Build Coq and plugins with `-strict-sequence`Gravatar Emilio Jesus Gallego Arias2018-07-14
* Remove unused env argument to fresh_sort_in_familyGravatar Gaëtan Gilbert2018-07-03
* Implement uniform parameters in ComInductiveGravatar Jasper Hugunin2018-07-01
* Remove reference name type.Gravatar Maxime Dénès2018-06-18
* [api] Misctypes removal: move Tactypes to proofsGravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
* Merge PR #7558: [api] Make `vernac/` self-contained.Gravatar Maxime Dénès2018-05-30
|\
* | Tactics.introduction: remove dangerous option ~checkGravatar Enrico Tassi2018-05-28
| * [api] Make `vernac/` self-contained.Gravatar Emilio Jesus Gallego Arias2018-05-27
* | Remove some occurrences of Evd.emptyGravatar Maxime Dénès2018-05-25
|/
* [tactics] Remove anonymous fix/cofix form.Gravatar Emilio Jesus Gallego Arias2018-05-24
* Merge PR #7177: Unifying names of "smart" combinators + adding combinators in...Gravatar Pierre-Marie Pédrot2018-05-24
|\
| * Moving Option.smart_map to Option.Smart.map.Gravatar Hugo Herbelin2018-05-23
* | [api] Move `opacity_flag` to `Proof_global`.Gravatar Emilio Jesus Gallego Arias2018-05-23
|/
* Split off Universes functions dealing with generating new universes.Gravatar Gaëtan Gilbert2018-05-17
* Deprecate Typing.e_* functionsGravatar Gaëtan Gilbert2018-05-14
* Deprecate Evarconv.e_conv,e_cumulGravatar Gaëtan Gilbert2018-05-11
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* Deprecate mixing univ minimization and evm normalization functions.Gravatar Gaëtan Gilbert2018-04-17
* Evar maps contain econstrs.Gravatar Gaëtan Gilbert2018-04-13
* Correction of ugly message described in #4667Gravatar Julien Forest2018-04-11
* change error message in #5147Gravatar Julien Forest2018-04-09
* removing uggly error message of #5147Gravatar Julien Forest2018-04-09
* Merge PR #6960: [api] Move some types to their proper module.Gravatar Pierre-Marie Pédrot2018-04-06
|\
| * [api] Move some types to their proper module.Gravatar Emilio Jesus Gallego Arias2018-04-02
* | Make parsing independent of the cumulativity flag.Gravatar Gaëtan Gilbert2018-03-21
|/
* [ssreflect] Fix module scoping problems due to packing and mli files.Gravatar Emilio Jesus Gallego Arias2018-03-10
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
* [located] More work towards using CAst.tGravatar Emilio Jesus Gallego Arias2018-03-09
* 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
|\
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-28 15:37:03 +0000