Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
0a224a4a
Commit
0a224a4a
authored
Jul 12, 2010
by
Andrei Paskevich
Browse files
no more "Kept" theories
parent
e6c48023
Changes
4
Hide whitespace changes
Inline
Side-by-side
drivers/cvc3.drv
View file @
0a224a4a
...
...
@@ -107,11 +107,6 @@ theory bool.Bool
end
*)
theory transform.encoding_decorate.Kept
meta cloned "encoding_decorate : kept" type t
end
(*
Local Variables:
mode: why
...
...
drivers/simplify.drv
View file @
0a224a4a
...
...
@@ -66,10 +66,6 @@ theory int.Int
remove prop Total
end
theory transform.encoding_decorate.Kept
meta cloned "encoding_decorate : kept" type t
end
(*
Local Variables:
mode: why
...
...
drivers/z3.drv
View file @
0a224a4a
...
...
@@ -121,10 +121,6 @@ theory int.EuclideanDivision
remove prop Div_1
end
theory transform.encoding_decorate.Kept
meta cloned "encoding_decorate : kept" type t
end
(*
Local Variables:
mode: why
...
...
theories/transform/encoding_decorate.why
View file @
0a224a4a
...
...
@@ -16,11 +16,6 @@ theory Builtin
t2u (d2t (sort tty x)) = x
end
theory Kept
(* If a driver tags this type by "encoding decorate : kept", all the type which clone this one will be kept by the encoding*)
type t
end
theory Prelude_mono
logic sort int int : int
logic int : int
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment