diff options
Diffstat (limited to 'plugins/micromega/g_zify.mlg')
| -rw-r--r-- | plugins/micromega/g_zify.mlg | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/plugins/micromega/g_zify.mlg b/plugins/micromega/g_zify.mlg index 74b0708743..d18065088c 100644 --- a/plugins/micromega/g_zify.mlg +++ b/plugins/micromega/g_zify.mlg @@ -24,17 +24,17 @@ let warn_deprecated_Spec = DECLARE PLUGIN "zify_plugin" VERNAC COMMAND EXTEND DECLAREINJECTION CLASSIFIED AS SIDEFF -| ["Add" "Zify" "InjTyp" constr(t) ] -> { Zify.InjTable.register t } -| ["Add" "Zify" "BinOp" constr(t) ] -> { Zify.BinOp.register t } -| ["Add" "Zify" "UnOp" constr(t) ] -> { Zify.UnOp.register t } -| ["Add" "Zify" "CstOp" constr(t) ] -> { Zify.CstOp.register t } -| ["Add" "Zify" "BinRel" constr(t) ] -> { Zify.BinRel.register t } -| ["Add" "Zify" "PropOp" constr(t) ] -> { Zify.PropBinOp.register t } -| ["Add" "Zify" "PropBinOp" constr(t) ] -> { Zify.PropBinOp.register t } -| ["Add" "Zify" "PropUOp" constr(t) ] -> { Zify.PropUnOp.register t } -| ["Add" "Zify" "BinOpSpec" constr(t) ] -> { Zify.BinOpSpec.register t } -| ["Add" "Zify" "UnOpSpec" constr(t) ] -> { Zify.UnOpSpec.register t } -| ["Add" "Zify" "Saturate" constr(t) ] -> { Zify.Saturate.register t } +| ["Add" "Zify" "InjTyp" reference(t) ] -> { Zify.InjTable.register t } +| ["Add" "Zify" "BinOp" reference(t) ] -> { Zify.BinOp.register t } +| ["Add" "Zify" "UnOp" reference(t) ] -> { Zify.UnOp.register t } +| ["Add" "Zify" "CstOp" reference(t) ] -> { Zify.CstOp.register t } +| ["Add" "Zify" "BinRel" reference(t) ] -> { Zify.BinRel.register t } +| ["Add" "Zify" "PropOp" reference(t) ] -> { Zify.PropBinOp.register t } +| ["Add" "Zify" "PropBinOp" reference(t) ] -> { Zify.PropBinOp.register t } +| ["Add" "Zify" "PropUOp" reference(t) ] -> { Zify.PropUnOp.register t } +| ["Add" "Zify" "BinOpSpec" reference(t) ] -> { Zify.BinOpSpec.register t } +| ["Add" "Zify" "UnOpSpec" reference(t) ] -> { Zify.UnOpSpec.register t } +| ["Add" "Zify" "Saturate" reference(t) ] -> { Zify.Saturate.register t } END TACTIC EXTEND ITER |