From 13f09096c1dc75898e32e915161b928a68b45346 Mon Sep 17 00:00:00 2001 From: Frédéric Besson Date: Sun, 17 May 2020 19:48:58 +0200 Subject: Update theories/micromega/ZifyBool.v Co-authored-by: Kazuhiko Sakaguchi - insert boolean constraint (b = true \/ b = false) - add specs for b2z - zify_post_hook performs a case-analysis over boolean constraints - Stricter typing constraints for `zify` declared operators The type is syntactically checked against the declaration of injections. Some explicit casts may need to be inserted. --- plugins/micromega/zify.mli | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'plugins/micromega/zify.mli') diff --git a/plugins/micromega/zify.mli b/plugins/micromega/zify.mli index 7960475def..537e652fd0 100644 --- a/plugins/micromega/zify.mli +++ b/plugins/micromega/zify.mli @@ -21,7 +21,8 @@ module CstOp : S module BinRel : S module PropBinOp : S module PropUnOp : S -module Spec : S +module BinOpSpec : S +module UnOpSpec : S module Saturate : S val zify_tac : unit Proofview.tactic -- cgit v1.2.3