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
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
121
Issues
121
List
Boards
Labels
Service Desk
Milestones
Merge Requests
17
Merge Requests
17
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
fc14a67a
Commit
fc14a67a
authored
Sep 18, 2012
by
Claude Marche
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
suppressed a few ocaml 4.00 warnings
parent
1b86a3f4
Changes
16
Hide whitespace changes
Inline
Side-by-side
Showing
16 changed files
with
7 additions
and
22 deletions
+7
-22
src/printer/alt_ergo.ml
src/printer/alt_ergo.ml
+0
-1
src/printer/cvc3.ml
src/printer/cvc3.ml
+0
-1
src/printer/gappa.ml
src/printer/gappa.ml
+0
-1
src/printer/pvs.ml
src/printer/pvs.ml
+1
-1
src/printer/simplify.ml
src/printer/simplify.ml
+0
-2
src/printer/smtv1.ml
src/printer/smtv1.ml
+0
-2
src/printer/smtv2.ml
src/printer/smtv2.ml
+0
-1
src/printer/yices.ml
src/printer/yices.ml
+0
-1
src/session/termcode.ml
src/session/termcode.ml
+0
-1
src/transform/abstraction.ml
src/transform/abstraction.ml
+0
-1
src/transform/close_epsilon.ml
src/transform/close_epsilon.ml
+0
-1
src/transform/encoding_guard.ml
src/transform/encoding_guard.ml
+1
-1
src/transform/encoding_instantiate.ml
src/transform/encoding_instantiate.ml
+5
-3
src/transform/eval_match.ml
src/transform/eval_match.ml
+0
-2
src/transform/introduction.ml
src/transform/introduction.ml
+0
-1
src/transform/smoke_detector.ml
src/transform/smoke_detector.ml
+0
-2
No files found.
src/printer/alt_ergo.ml
View file @
fc14a67a
...
...
@@ -26,7 +26,6 @@ open Ident
open
Ty
open
Term
open
Decl
open
Task
open
Printer
let
meta_ac
=
Theory
.
register_meta
"AC"
[
Theory
.
MTlsymbol
]
...
...
src/printer/cvc3.ml
View file @
fc14a67a
...
...
@@ -27,7 +27,6 @@ open Ty
open
Term
open
Decl
open
Theory
open
Task
open
Printer
let
ident_printer
=
...
...
src/printer/gappa.ml
View file @
fc14a67a
...
...
@@ -24,7 +24,6 @@ open Format
open
Pp
open
Printer
open
Ident
open
Ty
open
Term
open
Decl
open
Theory
...
...
src/printer/pvs.ml
View file @
fc14a67a
...
...
@@ -524,7 +524,7 @@ let re_why3 = Str.regexp "% Why3 \\([^ ]+\\)"
let
read_old_script
ch
=
let
chunks
=
ref
[]
in
let
contents
=
ref
[]
in
let
re
c
re
ad_line
()
=
let
read_line
()
=
let
s
=
input_line
ch
in
clean_line
s
in
...
...
src/printer/simplify.ml
View file @
fc14a67a
...
...
@@ -23,10 +23,8 @@
open
Format
open
Pp
open
Ident
open
Ty
open
Term
open
Decl
open
Task
open
Printer
let
ident_printer
=
...
...
src/printer/smtv1.ml
View file @
fc14a67a
...
...
@@ -26,8 +26,6 @@ open Ident
open
Ty
open
Term
open
Decl
open
Theory
open
Task
open
Printer
let
ident_printer
=
...
...
src/printer/smtv2.ml
View file @
fc14a67a
...
...
@@ -27,7 +27,6 @@ open Ty
open
Term
open
Decl
open
Theory
open
Task
open
Printer
let
ident_printer
=
...
...
src/printer/yices.ml
View file @
fc14a67a
...
...
@@ -27,7 +27,6 @@ open Ty
open
Term
open
Decl
open
Theory
open
Task
open
Printer
let
ident_printer
=
...
...
src/session/termcode.ml
View file @
fc14a67a
...
...
@@ -18,7 +18,6 @@
(* *)
(**************************************************************************)
open
Ty
open
Term
type
checksum
=
string
...
...
src/transform/abstraction.ml
View file @
fc14a67a
...
...
@@ -22,7 +22,6 @@
open
Ident
open
Term
open
Decl
open
Task
let
abstraction
(
keep
:
lsymbol
->
bool
)
=
let
term_table
=
Hterm_alpha
.
create
257
in
...
...
src/transform/close_epsilon.ml
View file @
fc14a67a
...
...
@@ -20,7 +20,6 @@
open
Theory
open
Decl
open
Task
open
Term
let
is_func_ty
t
=
...
...
src/transform/encoding_guard.ml
View file @
fc14a67a
...
...
@@ -153,7 +153,7 @@ module Transform = struct
and
f_type_close_select
kept
f'
=
let
tvs
=
t_ty_freevars
Stv
.
empty
f'
in
let
rec
trans
fn
acc
f
=
match
f
.
t_node
with
let
trans
fn
acc
f
=
match
f
.
t_node
with
|
Tquant
(
Tforall
as
q
,_
)
->
(* Exists same thing? *)
let
vsl
,
trl
,
fmla
=
f_open_all_quant
q
f
in
let
add
acc
vs
=
(
t_var
vs
)
::
acc
in
...
...
src/transform/encoding_instantiate.ml
View file @
fc14a67a
...
...
@@ -23,11 +23,9 @@ open Util
open
Ident
open
Ty
open
Term
open
Task
open
Theory
open
Task
open
Decl
open
Encoding
exception
TooMuchInstantiation
of
int
let
max_instantiation
=
512
(* 7 ** 3 = 343 *)
...
...
@@ -66,9 +64,11 @@ type tty =
|
Tyterm
of
ty
|
Tyty
of
ty
(* dead code
let print_tty fmt = function
| Tyterm ty -> Format.fprintf fmt "(Tyterm %a)" Pretty.print_ty ty
| Tyty ty -> Format.fprintf fmt "(Tyty %a)" Pretty.print_ty ty
*)
(* It can be backprojected to type, ty_dumb is like a bottom type it
never appear in final formulas *)
...
...
@@ -102,7 +102,9 @@ type env = {
edefined_tsymbol
:
tysymbol
Mtyl
.
t
Mts
.
t
;
}
(* dead code
type auto_clone = task -> tenv -> Sty.t -> task * env
*)
(* The environnement of the transformation during
the transformation of a formula *)
...
...
@@ -130,7 +132,7 @@ let print_env fmt menv =
type
tvar
=
ty
Mtv
.
t
let
rec
projty
menv
tvar
ty
=
let
projty
menv
tvar
ty
=
let
rec
aux
ty
=
match
ty
.
ty_node
with
|
Tyvar
_
->
Tyterm
ty
...
...
src/transform/eval_match.ml
View file @
fc14a67a
...
...
@@ -18,12 +18,10 @@
(* *)
(**************************************************************************)
open
Format
open
Ident
open
Ty
open
Term
open
Decl
open
Pretty
type
inline
=
known_map
->
lsymbol
->
ty
list
->
ty
option
->
bool
...
...
src/transform/introduction.ml
View file @
fc14a67a
...
...
@@ -28,7 +28,6 @@ open Ident
open
Ty
open
Term
open
Decl
open
Task
let
rec
intros
pr
f
=
match
f
.
t_node
with
|
Tbinop
(
Timplies
,
f1
,
f2
)
->
...
...
src/transform/smoke_detector.ml
View file @
fc14a67a
...
...
@@ -24,10 +24,8 @@
universal quantification (replace implication by conjunction).
*)
open
Ident
open
Term
open
Decl
open
Task
let
create
app
=
Trans
.
goal
(
fun
pr
t
->
[
create_prop_decl
Pgoal
pr
(
app
t
)])
...
...
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