aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
AgeCommit message (Expand)Author
2019-07-23Do not rely on dummy TACTIC EXTEND for ssreflect tactics.Pierre-Marie Pédrot
2019-07-11Merge PR #10498: [api] Deprecate GlobRef constructors.Gaëtan Gilbert
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-07-08[core] [api] Support OCaml 4.08Emilio Jesus Gallego Arias
2019-07-07[error] Remove special error printing pre-processingEmilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-07Merge PR #10205: Make discriminate tactic compatible with HoTTPierre-Marie Pédrot
2019-06-06Make discriminate tactic compatible with HoTTAndreas Lynge
2019-06-06Merge PR #8988: Towards unifying parsing/printing for universe instances and ...Gaëtan Gilbert
2019-06-06Merge PR #10305: Fix SSR (un)fold of polymorphic terms - issue 9336Enrico Tassi
2019-06-06Merge PR #10302: Fix SSR 'case B:b' with universe polymorphic equalityEnrico Tassi
2019-06-05Merge PR #10307: allow empty tactic_rules in ARGUMENT EXTENDPierre-Marie Pédrot
2019-06-05allow empty tactic_rules in ARGUMENT EXTENDDabrowski
2019-06-04Fix SSR (un)fold of polymorphic terms - issue 9336Andreas Lynge
2019-06-04Fix SSR 'case B:b' with universe polymorphic equalityAndreas Lynge
2019-06-03Apparently unused ssr nonterminalsJim Fehrle
2019-06-01Allowing Set to be part of universe expressions.Hugo Herbelin
2019-06-01Towards unifying parsing/printing for universe instances and Type's argument.Hugo Herbelin
2019-05-27Merge PR #10237: Fix some incorrect uses of proof-local environmentPierre-Marie Pédrot
2019-05-24Stop using pstate in global print queriesGaëtan Gilbert
2019-05-23Fixing typos - Part 3JPR
2019-05-23Fixing typos - Part 2JPR
2019-05-13Passing evar_map to evars_of_term rather than expecting the term to be evar-nf.Hugo Herbelin
2019-05-13Moving Evd.evars_of_term from constr to econstr + consequences.Hugo Herbelin
2019-05-13Merge PR #9887: [api] Remove 8.10 deprecations.Gaëtan Gilbert
2019-05-10Split the hypothesis conversion check in a conversion + ordering check.Pierre-Marie Pédrot
2019-05-10Make the check flag of conversion functions mandatory.Pierre-Marie Pédrot
2019-05-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
2019-04-30fix `simpl_rel` and notations, `{pred T}` alias, `nonPropType` interfaceGeorges Gonthier
2019-04-29Merge PR #9983: Hypothesis conversion allocates a single evarHugo Herbelin
2019-04-29Merge PR #9651: [ssr] Add tactics under and overCyril Cohen
2019-04-25Add a typing colon in the output of the Search ssreflect vernacularErik Martin-Dorel
2019-04-23Deprecate the *_no_check variants of conversion tactics.Pierre-Marie Pédrot
2019-04-23[ssr] set under's tactic argument at LEVEL 3Erik Martin-Dorel
2019-04-23[ssr] under: optimization of the tactic for (under eq_bigl => *)Erik Martin-Dorel
2019-04-23[ssr] Define over as a rewrite rule & Merge 'Under[ _ ] notationsErik Martin-Dorel
2019-04-23[ssr] under: Fix the defective form ("=> [*|*]" implied) and its docErik Martin-Dorel
2019-04-23[ssr] under: Add iff support in side-conditionsErik Martin-Dorel
2019-04-23[ssr] under: use varnames from the 1st ipat with multi-goal under lemmasErik Martin-Dorel
2019-04-23[ssr] new syntax for the under tacticEnrico Tassi
2019-04-23[ssr] under: Simplify the over tacticErik Martin-Dorel
2019-04-23[ssr] under: Add comment to justify the need for check_numgoalsErik Martin-Dorel
2019-04-23[ssr] over: Expose the new type of tactic for Ssrfwd.overtacErik Martin-Dorel
2019-04-23[ssr] Remove the unify_helper tactic that appears unnecessaryErik Martin-Dorel
2019-04-23[ssr] under: Fix rewrite goals order when called from underErik Martin-Dorel
2019-04-23[ssr] over: Add Ssrfwd.overtac in the .mliErik Martin-Dorel
2019-04-23[ssr] under: Check that the number of hints and focused goals matchErik Martin-Dorel
2019-04-23[ssr] under(one-liner version): Do nf_betaiota in the last goalErik Martin-Dorel
2019-04-23[ssr] under: Change the style of a few tests (over tactic vs. lemma)Erik Martin-Dorel
2019-04-23[ssr] under: Move {beta_expand, unify_helper} in the module type (qualify them)Erik Martin-Dorel
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 14:05:51 +0000