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
43445137
Commit
43445137
authored
Dec 04, 2010
by
François Bobot
Browse files
petite correction de retour à la ligne
et retour à la normal
parent
337f8ad5
Changes
4
Hide whitespace changes
Inline
Side-by-side
src/transform/encoding_arrays.ml
View file @
43445137
...
@@ -352,7 +352,7 @@ let create_env env task thpoly tds =
...
@@ -352,7 +352,7 @@ let create_env env task thpoly tds =
add_ty_decl
task
[
ts
,
Tabstract
]
,
ts
in
add_ty_decl
task
[
ts
,
Tabstract
]
,
ts
in
let
task
,
tskey
=
add_ty
task
key
in
let
task
,
tskey
=
add_ty
task
key
in
let
task
,
tselt
=
add_ty
task
elt
in
let
task
,
tselt
=
add_ty
task
elt
in
let
ts_name
=
"bta_"
^
(
Pp
.
string_of
Pretty
.
print_ty
ty
)
in
let
ts_name
=
"bta_"
^
(
Pp
.
string_of
_wnl
Pretty
.
print_ty
ty
)
in
let
ts
=
create_tysymbol
(
id_fresh
ts_name
)
[]
None
in
let
ts
=
create_tysymbol
(
id_fresh
ts_name
)
[]
None
in
let
task
=
add_ty_decl
task
[
ts
,
Tabstract
]
in
let
task
=
add_ty_decl
task
[
ts
,
Tabstract
]
in
let
th_inst
=
create_inst
~
ts
:
[
ct
,
ts
;
ckey
,
tskey
;
celt
,
tselt
]
~
ls
:
[]
let
th_inst
=
create_inst
~
ts
:
[
ct
,
ts
;
ckey
,
tskey
;
celt
,
tselt
]
~
ls
:
[]
...
...
src/transform/libencoding.ml
View file @
43445137
...
@@ -74,7 +74,7 @@ let ls_of_const ty_base =
...
@@ -74,7 +74,7 @@ let ls_of_const ty_base =
fun
t
->
match
t
.
t_node
with
fun
t
->
match
t
.
t_node
with
|
Tconst
_
->
|
Tconst
_
->
begin
try
Hterm
.
find
ht
t
with
Not_found
->
begin
try
Hterm
.
find
ht
t
with
Not_found
->
let
s
=
"const_"
^
Pp
.
string_of
Pretty
.
print_term
t
in
let
s
=
"const_"
^
Pp
.
string_of
_wnl
Pretty
.
print_term
t
in
let
ls
=
create_fsymbol
(
id_fresh
s
)
[]
ty_base
in
let
ls
=
create_fsymbol
(
id_fresh
s
)
[]
ty_base
in
Hterm
.
add
ht
t
ls
;
Hterm
.
add
ht
t
ls
;
ls
ls
...
...
src/util/pp.ml
View file @
43445137
...
@@ -149,6 +149,13 @@ let rec print_list_opt sep print fmt = function
...
@@ -149,6 +149,13 @@ let rec print_list_opt sep print fmt = function
let
string_of
p
x
=
let
string_of
p
x
=
let
b
=
Buffer
.
create
100
in
let
fmt
=
formatter_of_buffer
b
in
fprintf
fmt
"%a@?"
p
x
;
Buffer
.
contents
b
let
string_of_wnl
p
x
=
let
b
=
Buffer
.
create
100
in
let
b
=
Buffer
.
create
100
in
let
fmt
=
formatter_of_buffer
b
in
let
fmt
=
formatter_of_buffer
b
in
let
out
,
flush
,_
newline
,
spaces
=
let
out
,
flush
,_
newline
,
spaces
=
...
...
src/util/pp.mli
View file @
43445137
...
@@ -120,3 +120,5 @@ val print_list_opt :
...
@@ -120,3 +120,5 @@ val print_list_opt :
val
string_of
:
(
Format
.
formatter
->
'
a
->
unit
)
->
'
a
->
string
val
string_of
:
(
Format
.
formatter
->
'
a
->
unit
)
->
'
a
->
string
val
string_of_wnl
:
(
Format
.
formatter
->
'
a
->
unit
)
->
'
a
->
string
(** same as {!string_of} but without newline *)
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