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
967d56ca
Commit
967d56ca
authored
Aug 19, 2010
by
Francois Bobot
Browse files
functionnal value : utilise tag weak comme clé...
parent
34b26f90
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/core/term.ml
View file @
967d56ca
...
...
@@ -1088,15 +1088,7 @@ and f_gen_map fnT fnB fnV fnL f =
let
br
(
p
,
b
,
f
)
=
pat_gen_map
fnT
fnB
fnL
p
,
bnd_map
fn_t
b
,
fn_f
f
in
f_case
(
fn_t
t
)
(
List
.
map
br
bl
))
let
get_fnT
fn
=
let
ht
=
Hashtbl
.
create
17
in
let
fnT
ty
=
try
Hashtbl
.
find
ht
ty
.
ty_tag
with
Not_found
->
let
nt
=
ty_s_map
fn
ty
in
Hashtbl
.
add
ht
ty
.
ty_tag
nt
;
nt
in
fnT
let
get_fnT
fn
=
Wty
.
memoize
17
(
fun
ty
->
ty_s_map
fn
ty
)
let
get_fnB
()
=
let
ht
=
Hid
.
create
17
in
...
...
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