aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
AgeCommit message (Expand)Author
2020-03-08Merge PR #11578: [exn] Keep information from multiple extra exn handlersPierre-Marie Pédrot
2020-03-05Merge PR #11522: Adding an alias `pose proof (x:=t)` for `pose proof t as x` ...Pierre-Marie Pédrot
2020-03-04Merge PR #11380: [exninfo] Deprecate aliases for exception re-raising.Pierre-Marie Pédrot
2020-03-04Merge PR #11709: Deprecate the "prolog" tactic.Théo Zimmermann
2020-03-03[exn] Keep information from multiple extra exn handlersEmilio Jesus Gallego Arias
2020-03-03[exninfo] Deprecate aliases for exception re-raising.Emilio Jesus Gallego Arias
2020-03-03Adding an alias "pose proof (x:=a)" for "pose proof a as x".Hugo Herbelin
2020-03-01[parser] lk_int -> lk_natMaxime Dénès
2020-03-01Refactor lookaheads using DSLMaxime Dénès
2020-02-28Deprecate the "prolog" tactic.Pierre-Marie Pédrot
2020-02-25Merge PR #11489: [exn] remove `raise` taking optional exception information a...Pierre-Marie Pédrot
2020-02-25Merge PR #11655: [parsing] Track need to reinit by typingPierre-Marie Pédrot
2020-02-24[exn] remove `raise` taking optional exception information argumentEmilio Jesus Gallego Arias
2020-02-24Merge PR #11653: Tactic_matching.pattern_match_term: remove ignored "refresh"...Pierre-Marie Pédrot
2020-02-22Making structure of type "tolerability" and related clearer.Hugo Herbelin
2020-02-21[parsing] Track need to reinit by typingEmilio Jesus Gallego Arias
2020-02-21Tactic_matching.pattern_match_term: remove ignored "refresh" argumentGaëtan Gilbert
2020-02-13[build] Consolidate stdlib's .v files under a single directory.Emilio Jesus Gallego Arias
2020-02-13Merge PR #11521: Remove Goptions.opt_name fieldPierre-Marie Pédrot
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2020-02-12Standardize constr -> globref operations to use destRef/isRef/isRefXGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Extractactics.destauto_inGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Extractactics.mkCaseEqGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Rewrite.symmetry_inGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Rewrite.default_morphismGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Rewrite.build_morphism_signatureGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Rewrite.resolve_morphismGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Rewrite.decompose_app_relGaëtan Gilbert
2019-12-26Remove uses of Global in Evd API.Pierre-Marie Pédrot
2019-12-18Merge PR #11027: Cleanup post #10647 (expose comind universe handling)Pierre-Marie Pédrot
2019-12-18Merge PR #11203: Make the string argument of `time` print correctlyPierre-Marie Pédrot
2019-12-16Pretyping.check_evars: make initial evar map optionalGaëtan Gilbert
2019-12-10Side-effect free wrapper around already declared schemes.Pierre-Marie Pédrot
2019-12-06Make the string argument of `time` print correctlyJason Gross
2019-12-06Moving the diversity of constr printers to a label style.Hugo Herbelin
2019-12-05Merge PR #11241: Unfortunate Coq 8.10 bug with "cofix with" tactic syntaxEmilio Jesus Gallego Arias
2019-12-05Unfortunate bug with "cofix with": case of a CProdN over no bindings.Hugo Herbelin
2019-12-05Merge PR #11210: Tacinterp: push_trace doesn't need to be wrapped in a tacticPierre-Marie Pédrot
2019-11-30Actually deprecate the `cutrewrite` tacticMaxime Dénès
2019-11-28Tacinterp: push_trace doesn't need to be wrapped in a tacticGaëtan Gilbert
2019-11-26Undeprecate Add Setoid / Add Morphism.Théo Zimmermann
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-16Merge PR #10996: Refine Instance returnsPierre-Marie Pédrot
2019-11-14Rename non-unique local nonterminalsJim Fehrle
2019-11-13Return of Refine Instance as an attribute.Gaëtan Gilbert
2019-10-18factorize or_var_mapAlexandre Moine
2019-09-23Fixes #10778 (fresh was not updated after renaming of intropattern entry in #...Hugo Herbelin
2019-08-29Make sure that all query commands return a notice (not an info) feedbackMaxime Dénès
2019-08-26Tauto: use Coqlib to locate “not” and “NNPP”Vincent Laporte
2019-08-23Merge PR #10665: [api] Move handling of variable implicit data to impargsGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 23:44:21 +0000