aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
AgeCommit message (Collapse)Author
2020-11-05Merge PR #12218: Numeral notations for non inductive typescoqbot-app[bot]
Reviewed-by: herbelin Reviewed-by: JasonGross Reviewed-by: jfehrle Ack-by: Zimmi48
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]
Reviewed-by: gares Reviewed-by: herbelin Ack-by: ppedrot
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]
Reviewed-by: SkySkimmer Ack-by: gares Ack-by: ejgallego
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
Note: "hyp" was documented in Ltac Notation chapter but "var" was not.
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 ↵Hugo Herbelin
renaming. Example: > Arguments id [B] {b} : rename. > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: Argument B is a trailing implicit, so it can't be declared non maximal. Please use { } instead of [ ].
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
Amends c1b1afe76e1655cc3275bdf4215f0ab690efc3cc
2020-08-19Merge PR #12725: Store evar identity instances in evarinfo / named_context_valEnrico Tassi
Ack-by: SkySkimmer Reviewed-by: gares
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 ↵Pierre-Marie Pédrot
of standard infrastructure. Reviewed-by: ppedrot
2020-07-17Do not store the full environment inside ssr ast_closure_term.Pierre-Marie Pédrot
Apart from being verboten to marshal Environ.env, this should use much less memory on-disk. Fixes #12707.
2020-07-16[gramlib] Remove legacy located exception wrapper in favor of standard ↵Emilio Jesus Gallego Arias
infrastructure. The old wrapper was basically unused, this PR also fixes backtraces in some class of bugs such as https://github.com/coq/coq/issues/12695
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
but ssrsearch is not loaded. Fixes #12338
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
- new clauses "hyp:", "concl:", "headhyp:" and "headconcl:" to restrict match to an hypothesis or the conclusion, possibly only at the head (like SearchHead in this latter case) - new clause "is:" to search by kind of object (for some list of kinds) - support for any combination of negations, disjunctions and conjunctions, using a syntax close to that of intropatterns.
2020-05-14[exn] [tactics] improve backtraces on monadic errorsEmilio Jesus Gallego Arias
Current backtraces for tactics leave a bit to desire, for example given the program: ```coq Lemma u n : n + 0 = n. rewrite plus_O_n. ``` the backtrace stops at: ``` Found no subterm matching "0 + ?M160" in the current goal. Called from file "proofs/proof.ml", line 381, characters 4-42 Called from file "tactics/pfedit.ml", line 102, characters 31-58 Called from file "plugins/ltac/g_ltac.mlg", line 378, characters 8-84 ``` Backtrace information `?info` is as of today optional in some tactics, such as `tclZERO`, it doesn't cost a lot however to reify backtrace information indeed in `tclZERO` and provide backtraces for all tactic errors. The cost should be small if we are not in debug mode. The backtrace for the failed rewrite is now: ``` Found no subterm matching "0 + ?M160" in the current goal. Raised at file "pretyping/unification.ml", line 1827, characters 14-73 Called from file "pretyping/unification.ml", line 1929, characters 17-53 Called from file "pretyping/unification.ml", line 1948, characters 22-72 Called from file "pretyping/unification.ml", line 2020, characters 14-56 Re-raised at file "pretyping/unification.ml", line 2021, characters 66-73 Called from file "proofs/clenv.ml", line 254, characters 12-58 Called from file "proofs/clenvtac.ml", line 95, characters 16-53 Called from file "engine/proofview.ml", line 1110, characters 40-46 Called from file "engine/proofview.ml", line 1115, characters 10-34 Re-raised at file "clib/exninfo.ml", line 82, characters 4-38 Called from file "proofs/proof.ml", line 381, characters 4-42 Called from file "tactics/pfedit.ml", line 102, characters 31-58 Called from file "plugins/ltac/g_ltac.mlg", line 378, characters 8-84 ``` which IMO is much better.
2020-05-14Merge PR #11922: No more local reduction functions in Reductionops.Maxime Dénès
Reviewed-by: Matafou Ack-by: SkySkimmer Reviewed-by: gares
2020-05-11Merge PR #12273: Deprecate Refiner APIEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-05-10No more local reduction functions in Reductionops.Pierre-Marie Pédrot
This is extracted from #9710, where we need the environment anyway to compute iota rules on inductive types with let-bindings. The commit is self-contained, so I think it could go directly in to save me a few rebases. Furthermore, this is also related to #11707. Assuming we split cbn from the other reduction machine, this allows to merge the "local" machine with the general one, since after this PR they will have the same type. One less reduction machine should make people happy.
2020-05-09Merge PR #12163: Fix #12159 (Numeral Notations do not play well with ↵Hugo Herbelin
multiple scopes for the same inductive)
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
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Remove legacy API in SSR.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tacticsPierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 18:40:01 +0000