aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/g_indfun.ml4
AgeCommit message (Expand)Author
2018-10-15Port remaining EXTEND ml4 files to coqpp.Pierre-Marie Pédrot
2018-10-15Plug ARGUMENT EXTEND into the argument extension API.Pierre-Marie Pédrot
2018-10-15Deprecating the RAW_TYPED and GLOB_TYPED stanzas of the ARGUMENT EXTEND macro.Pierre-Marie Pédrot
2018-06-18Remove reference name type.Maxime Dénès
2018-06-12[api] Misctypes removal: move Tactypes to proofsEmilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-05-30Merge PR #7558: [api] Make `vernac/` self-contained.Maxime Dénès
2018-05-27[api] Make `vernac/` self-contained.Emilio Jesus Gallego Arias
2018-05-25Remove some occurrences of Evd.emptyMaxime Dénès
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-17Change references to CAMLP4 to CAMLP5 to be more accurate since we noJim Fehrle
2018-01-08[vernac] vernac_expr no longer recursiveVincent Laporte
2017-12-20Separate vernac controls and regular commands.Maxime Dénès
2017-11-29Remove "obsolete_locality" and fix STM vernac classification.Maxime Dénès
2017-11-02Using a specific function to register vernac printers.Hugo Herbelin
2017-09-08Parse directly to Sorts.family when appropriate.Gaëtan Gilbert
2017-07-25[api] Remove type equalities from API.Emilio Jesus Gallego Arias
2017-07-17[API] Remove `open API` in ml files in favor of `-open API` flag.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-10Remove (useless) aliases from the API.Matej Košík
2017-06-07Put all plugins behind an "API".Matej Kosik
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-06-01[printing] Remove duplicated printing function.Emilio Jesus Gallego Arias
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
2017-04-24[location] Use located in misctypes.Emilio Jesus Gallego Arias
2017-04-11Merge PR#379: Introducing evar-insensitive constrsMaxime Dénès
2017-04-07[camlpX] Remove camlp4 compat layer.Emilio Jesus Gallego Arias
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-02-17Moving the Ltac plugin to a pack-based one.Pierre-Marie Pédrot
2017-02-14Funind API using EConstr.Pierre-Marie Pédrot
2017-02-14Ltac now uses evar-based constrs.Pierre-Marie Pédrot
2017-02-14Tactics API using EConstr.Pierre-Marie Pédrot
2016-09-21Merging Stdarg and Constrarg.Pierre-Marie Pédrot
2016-09-14Moving Ltac-specific parsing API to ltac/ folder.Pierre-Marie Pédrot
2016-07-03rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...Pierre Letouzey
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-06-16Fixing a mispelling coma -> comma.Hugo Herbelin
2016-06-16Fixing printing of Function.Hugo Herbelin
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-05-04More toplevel value representation sharing.Pierre-Marie Pédrot
2016-04-27Revert "Fixing printing of Function."Hugo Herbelin
2016-04-27Revert "Fixing a mispelling coma -> comma."Hugo Herbelin
2016-04-27Fixing a mispelling coma -> comma.Hugo Herbelin
2016-04-27Fixing printing of Function.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:03:12 +0000