aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/tacinterp.mli
AgeCommit message (Expand)Author
2017-10-25[general] Remove Econstr dependency from `intf`Emilio Jesus Gallego Arias
2017-09-28Efficient fresh name generation relying on sets.Pierre-Marie Pédrot
2017-08-01Move type_uconstr to Tacinterp.Maxime Dénès
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-07Put all plugins behind an "API".Matej Kosik
2017-06-06Merge PR#600: Some factorizations of ltac interpretation functions between ss...Maxime Dénès
2017-05-31Factorizing interp_gen through a function interpreting glob_constr.Hugo Herbelin
2017-05-31Splitting interp_open_constr into two variants, with or without type classes.Hugo Herbelin
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-03-14Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFunMaxime Dénès
2017-02-17Ltac as a plugin.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 09:27:33 +0000