From d2c7022f0e16e6037c0d8c30c837abaad2c8194f Mon Sep 17 00:00:00 2001 From: Frederic Besson Date: Mon, 12 Apr 2021 21:02:51 +0200 Subject: [zify] bugfix - to zify the conclusion, we are using Tactics.apply (not rewrite) Closes #11089 - constrain the arguments of Add Zify X to be GlobRef.t Unset Primitive Projections so that projections are GlobRef.t. Closes #14043 Update doc/sphinx/addendum/micromega.rst Co-authored-by: Théo Zimmermann --- doc/sphinx/addendum/micromega.rst | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index d718454364..24e35dd85a 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -295,7 +295,7 @@ obtain :math:`-1`. By Theorem :ref:`Psatz `, the goal is valid. The :tacn:`zify` tactic can be extended with new types and operators by declaring and registering new typeclass instances using the following commands. The typeclass declarations can be found in the module ``ZifyClasses`` and the default instances can be found in the module ``ZifyInst``. -.. cmd:: Add Zify @add_zify @one_term +.. cmd:: Add Zify @add_zify @qualid .. insertprodn add_zify add_zify @@ -304,6 +304,9 @@ obtain :math:`-1`. By Theorem :ref:`Psatz `, the goal is valid. | {| PropOp | PropBinOp | PropUOp | Saturate } Registers an instance of the specified typeclass. + The typeclass type (e.g. :g:`BinOp Z.mul` or :g:`BinRel (@eq Z)`) has the additional constraint that + the non-implicit argument (here, :g:`Z.mul` or :g:`(@eq Z)`) + is either a :n:`@reference` (here, :g:`Z.mul`) or the application of a :n:`@reference` (here, :g:`@eq`) to a sequence of :n:`@one_term`. .. cmd:: Show Zify @show_zify -- cgit v1.2.3