aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
AgeCommit message (Expand)Author
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
2019-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
2019-08-17Delay the computation of frozen evars in legacy unification.Pierre-Marie Pédrot
2019-08-08Merge PR #10324: Fix #10088: Ltac2 & operator conflicts with notations involv...Maxime Dénès
2019-07-29Tentatively providing a localization function to ad-hoc camlp5 parsers.Pierre-Marie Pédrot
2019-07-26Remove unused grammar productionsJim Fehrle
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-07-01[decls] Remove goal_object_kind type.Emilio Jesus Gallego Arias
2019-07-01[declare] Separate kinds from entries in constant declarationEmilio Jesus Gallego Arias
2019-07-01[api] Refactor most of `Decl_kinds`Emilio Jesus Gallego Arias
2019-06-26[declare] Fine tuning of Hook type.Emilio Jesus Gallego Arias
2019-06-25Remove the internal_flag argument from Declare API.Pierre-Marie Pédrot
2019-06-24[api] Remove `polymorphic` type alias, use labels instead.Emilio Jesus Gallego Arias
2019-06-24[lemmas] [proof] Split proof kinds into per-layer components.Emilio Jesus Gallego Arias
2019-06-24[proof] Remove duplicated universe polymorphic from decl_kindsEmilio Jesus Gallego Arias
2019-06-24[lemmas] Turn Lemmas.info into a proper type with constructor.Emilio Jesus Gallego Arias
2019-06-24Duplicate the type of constant entries in Proof_global.Pierre-Marie Pédrot
2019-06-20Merge PR #9645: [proof] Remove terminator type, unifying regular and obligati...Pierre-Marie Pédrot
2019-06-19Merge PR #10239: Deprecate grammar entry "intropattern" in tactic notations i...Théo Zimmermann
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-17[proof] Move declaration hooks to DeclareDef.Emilio Jesus Gallego Arias
2019-06-16Deprecate "intro_pattern" in tactic notations in favor of "simple_intropattern".Hugo Herbelin
2019-06-13Merge PR #10319: [STM] Only VtSideeff can be VtNow/VtLaterEnrico Tassi
2019-06-12Merge PR #10180: `deprecated` attribute support for notations and syntactic d...Théo Zimmermann
2019-06-11STM: encode in static types that vernac_when is only used when VtSideffGaëtan Gilbert
2019-06-09[proof] Uniformize Proof_global APIEmilio Jesus Gallego Arias
2019-06-09[proof] Move proofs that have an associated constant to `Lemmas`Emilio Jesus Gallego Arias
2019-06-08Cleaning the status of Local Definition and similar.Hugo Herbelin
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-06`deprecated` attribute support for notations and syntactic definitionsMaxime Dénès
2019-06-04[rewrite] remove program_mode from attributes (unused)Enrico Tassi
2019-06-04[classes] remove program mode from the new_instance_* APIsEnrico Tassi
2019-06-04[vernac] more precise types for Add Morph, Instance, and FunctionEnrico Tassi
2019-06-04[rewrite] Add Morphism syntax made different for module type parametersEnrico Tassi
2019-06-04Rename Proof_global.{pstate -> t}Gaëtan Gilbert
2019-06-04Alternate syntax for ![]: VERNAC EXTEND Foo STATE proofGaëtan Gilbert
2019-06-04coqpp: add new ![] specifiers for structured proof interactionGaëtan Gilbert
2019-06-04Proof_global: pass only 1 pstate when we don't want the proof stackGaëtan Gilbert
2019-06-04rewrite.ml: remove outdated commentGaëtan Gilbert
2019-06-04rewrite.ml: drop the id returned by new_instance earlierGaëtan Gilbert
2019-05-27Merge PR #10237: Fix some incorrect uses of proof-local environmentPierre-Marie Pédrot
2019-05-25Documenting syntax "injection ... as [= pat1 ... patn ]".Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:34:29 +0000