aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
AgeCommit message (Expand)Author
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
2021-01-13Avoid using "subgoals" in the UI, it means the same as "goals"Jim Fehrle
2020-12-30Merge PR #13321: Move evaluable_global_reference from Names to Tacred.coqbot-app[bot]
2020-12-27Refactor cpattern into a recordLasse Blaauwbroek
2020-12-27Make ssrtermkind algebraic instead of a charLasse Blaauwbroek
2020-12-21Move evaluable_global_reference from Names to Tacred.Pierre-Marie Pédrot
2020-11-25Separate interning and pretyping of universesGaëtan Gilbert
2020-11-20Use nat_or_var where negative values don't make senseJim Fehrle
2020-11-05Merge PR #12218: Numeral notations for non inductive typescoqbot-app[bot]
2020-11-04Remove warning on SSR Search having moved.Théo Zimmermann
2020-10-30Renaming Numeral into NumberPierre Roux
2020-10-27Merge PR #13238: Fix some tactic print bugscoqbot-app[bot]
2020-10-27Rename tactic_expr -> ltac_exprJim Fehrle
2020-10-27Rename operconstr -> termJim Fehrle
2020-10-27Merge PR #13075: Introducing the foundations for a name-alias-agnostic APIcoqbot-app[bot]
2020-10-26adjust Search deprecation warningRalf Jung
2020-10-22Fix printing of wit_constr and some ssr problems with printing empty listsLasse Blaauwbroek
2020-10-21Add missing deprecations in Projection API.Pierre-Marie Pédrot
2020-10-14Deprecating wit_var to the benefit of its synonymous wit_hyp.Hugo Herbelin
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-09-22Fixes #9716, #13004: don't drop the qualifier of quotations at printing time.Hugo Herbelin
2020-09-11[parsing] Rename token NUMERAL to NUMBERPierre Roux
2020-08-28When reporting an implicit argument error on a rename argument, use the renam...Hugo Herbelin
2020-08-27Remove a call to the old refiner in ssr.Pierre-Marie Pédrot
2020-08-20[ssr] when porting v8.2 code no backtracking point has to be addedEnrico Tassi
2020-08-19Merge PR #12725: Store evar identity instances in evarinfo / named_context_valEnrico Tassi
2020-08-10[ssr] turn "nothing to inject" into a real warning (fix #12746)Enrico Tassi
2020-08-06Actually use the default instance stored inside named_context_val.Pierre-Marie Pédrot
2020-07-18Merge PR #12696: [gramlib] Remove legacy located exception wrapper in favor o...Pierre-Marie Pédrot
2020-07-17Do not store the full environment inside ssr ast_closure_term.Pierre-Marie Pédrot
2020-07-16[gramlib] Remove legacy located exception wrapper in favor of standard infras...Emilio Jesus Gallego Arias
2020-07-08Remove Evarutil.new_evar_instance from the API.Pierre-Marie Pédrot
2020-06-29Moving the remaining Refiner functions to Tacmach.Pierre-Marie Pédrot
2020-06-29Remove Refiner.refiner.Pierre-Marie Pédrot
2020-06-15[ssr] fix env handling in error message (fix #12507)Enrico Tassi
2020-06-15[ssr] remove catch allEnrico Tassi
2020-05-18[search] [ssr] Emit deprecated message when calling search from ssreflectEmilio Jesus Gallego Arias
2020-05-15Move SSR's Search to a new plugin and deprecate it.Théo Zimmermann
2020-05-15Search: new clauses for searching head, conclusion, kind...Hugo Herbelin
2020-05-14[exn] [tactics] improve backtraces on monadic errorsEmilio Jesus Gallego Arias
2020-05-14Merge PR #11922: No more local reduction functions in Reductionops.Maxime Dénès
2020-05-11Merge PR #12273: Deprecate Refiner APIEmilio Jesus Gallego Arias
2020-05-10No more local reduction functions in Reductionops.Pierre-Marie Pédrot
2020-05-09Merge PR #12163: Fix #12159 (Numeral Notations do not play well with multiple...Hugo Herbelin
2020-05-07Deprecate the legacy tacticals from module Refiner.Pierre-Marie Pédrot
2020-05-05[ssr] wrap a couple of exception with tclLIFTEnrico Tassi
2020-05-04[ssr] get rid of (pf_)mkSsrConstEnrico Tassi
2020-05-03Further port of ssr tacticsPierre-Marie Pédrot
2020-05-03Further port of SSR tactics.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:22:37 +0000