Mentions légales du service
Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
why3
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container registry
Monitor
Service Desk
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
Why3
why3
Commits
a1d7fd72
Commit
a1d7fd72
authored
14 years ago
by
François Bobot
Browse files
Options
Downloads
Patches
Plain Diff
Core : restreint the type in order to prevent ourselves from miss-spelling,
like the last commit
parent
293d9dd7
Branches
Branches containing commit
Tags
Tags containing commit
No related merge requests found
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
src/core/term.ml
+3
-3
3 additions, 3 deletions
src/core/term.ml
src/core/ty.ml
+2
-2
2 additions, 2 deletions
src/core/ty.ml
with
5 additions
and
5 deletions
src/core/term.ml
+
3
−
3
View file @
a1d7fd72
...
@@ -328,8 +328,8 @@ and expr =
...
@@ -328,8 +328,8 @@ and expr =
(* term and fmla equality *)
(* term and fmla equality *)
let
t_equal
=
(
==
)
let
t_equal
:
term
->
term
->
bool
=
(
==
)
let
f_equal
=
(
==
)
let
f_equal
:
fmla
->
fmla
->
bool
=
(
==
)
let
t_hash
t
=
t
.
t_tag
let
t_hash
t
=
t
.
t_tag
let
f_hash
f
=
f
.
f_tag
let
f_hash
f
=
f
.
f_tag
...
@@ -1702,7 +1702,7 @@ exception NoMatch
...
@@ -1702,7 +1702,7 @@ exception NoMatch
let
rec
t_match
s
t1
t2
=
let
rec
t_match
s
t1
t2
=
if
t_equal
t1
t2
then
s
else
if
t_equal
t1
t2
then
s
else
if
not
(
t_equal
t1
.
t_ty
t2
.
t_ty
)
then
raise
NoMatch
else
if
not
(
t
y
_equal
t1
.
t_ty
t2
.
t_ty
)
then
raise
NoMatch
else
match
t1
.
t_node
,
t2
.
t_node
with
match
t1
.
t_node
,
t2
.
t_node
with
|
Tconst
c1
,
Tconst
c2
when
c1
=
c2
->
s
|
Tconst
c1
,
Tconst
c2
when
c1
=
c2
->
s
|
Tvar
v1
,
_
->
|
Tvar
v1
,
_
->
...
...
This diff is collapsed.
Click to expand it.
src/core/ty.ml
+
2
−
2
View file @
a1d7fd72
...
@@ -68,8 +68,8 @@ module Mts = Tsym.M
...
@@ -68,8 +68,8 @@ module Mts = Tsym.M
module
Hts
=
Tsym
.
H
module
Hts
=
Tsym
.
H
module
Wts
=
Tsym
.
W
module
Wts
=
Tsym
.
W
let
ts_equal
=
(
==
)
let
ts_equal
:
tysymbol
->
tysymbol
->
bool
=
(
==
)
let
ty_equal
=
(
==
)
let
ty_equal
:
ty
->
ty
->
bool
=
(
==
)
let
ts_hash
ts
=
id_hash
ts
.
ts_name
let
ts_hash
ts
=
id_hash
ts
.
ts_name
let
ty_hash
ty
=
Hashweak
.
tag_hash
ty
.
ty_tag
let
ty_hash
ty
=
Hashweak
.
tag_hash
ty
.
ty_tag
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
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!
Save comment
Cancel
Please
register
or
sign in
to comment