Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
O
Ocarina
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
2
Issues
2
List
Boards
Labels
Service Desk
Milestones
Merge Requests
0
Merge Requests
0
Operations
Operations
Incidents
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
TASTE
Ocarina
Commits
46cd5ac2
Commit
46cd5ac2
authored
Jun 17, 2016
by
Jerome Hugues
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
* Reset list of theorems to run
parent
18ff7fb6
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
3 additions
and
2 deletions
+3
-2
src/core/model/ocarina-analyzer-real.adb
src/core/model/ocarina-analyzer-real.adb
+3
-2
No files found.
src/core/model/ocarina-analyzer-real.adb
View file @
46cd5ac2
...
...
@@ -148,7 +148,6 @@ package body Ocarina.Analyzer.REAL is
procedure
Register_Library_Theorems
(
REAL_Library
:
Node_Id
)
is
pragma
Assert
(
Kind
(
REAL_Library
)
=
K_Root_Node
);
package
RNU
renames
Ocarina
.
ME_REAL
.
REAL_Tree
.
Nutils
;
N
:
Node
;
T
:
Node_Id
;
...
...
@@ -211,7 +210,9 @@ package body Ocarina.Analyzer.REAL is
else
-- Otherwise, iterate over Library theorems and fetch the
-- corresponding theorems.
-- corresponding theorem.
RNU
.
Node_List
.
Init
(
To_Run_Theorem_List
);
-- Reset list of theorems
for
J
in
RNU
.
Node_List
.
First
..
RNU
.
Node_List
.
Last
(
Library_Theorems
)
loop
...
...
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