Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
092ca94c
Commit
092ca94c
authored
Mar 11, 2010
by
Francois Bobot
Browse files
inversion des cloned et logic,type,prop
parent
afdb7da2
Changes
2
Hide whitespace changes
Inline
Side-by-side
lib/drivers/alt_ergo.drv
View file @
092ca94c
...
...
@@ -54,9 +54,9 @@ theory prelude.Int
end
theory algebra.AC
tag
logic
cloned op "AC"
remove
prop
cloned Comm
remove
prop
cloned Assoc
tag cloned
logic
op "AC"
remove cloned
prop
Comm
remove cloned
prop
Assoc
end
(*
...
...
src/output/driver_parser.mly
View file @
092ca94c
...
...
@@ -77,12 +77,12 @@ list0_trule:
trule
:
|
PRELUDE
STRING
{
Rprelude
(
loc
()
,$
2
)
}
|
REMOVE
PROP
cloned
qualid
{
Rremove
(
$
3
,
$
4
)
}
|
REMOVE
cloned
PROP
qualid
{
Rremove
(
$
2
,
$
4
)
}
|
SYNTAX
TYPE
qualid
STRING
{
Rsyntaxty
(
$
3
,
$
4
)
}
|
SYNTAX
LOGIC
qualid
STRING
{
Rsyntaxls
(
$
3
,
$
4
)
}
|
TAG
TYPE
cloned
qualid
STRING
{
Rtagty
(
$
3
,
$
4
,
$
5
)
}
|
TAG
LOGIC
cloned
qualid
STRING
{
Rtagls
(
$
3
,
$
4
,
$
5
)
}
|
TAG
PROP
cloned
qualid
STRING
{
Rtagpr
(
$
3
,
$
4
,
$
5
)
}
|
TAG
cloned
TYPE
qualid
STRING
{
Rtagty
(
$
2
,
$
4
,
$
5
)
}
|
TAG
cloned
LOGIC
qualid
STRING
{
Rtagls
(
$
2
,
$
4
,
$
5
)
}
|
TAG
cloned
PROP
qualid
STRING
{
Rtagpr
(
$
2
,
$
4
,
$
5
)
}
;
cloned
:
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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