Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
490f7095
Commit
490f7095
authored
Apr 14, 2010
by
Jean-Christophe Filliâtre
Browse files
coq-plugin: type definitions
parent
694704db
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/coq-plugin/whytac.ml
View file @
490f7095
...
...
@@ -256,7 +256,7 @@ and tr_global_ts env r =
let
b
=
force
b
in
let
(
tv
,
vars
)
,
env
,
t
=
decomp_type_lambdas
env
b
in
let
def
=
Some
(
tr_type
tv
env
t
)
in
Ty
.
create_tysymbol
id
vars
def
Ty
.
create_tysymbol
id
vars
None
(* FIXME: is it correct to use None when NotFO? *)
|
None
->
let
tv
=
...
...
Write
Preview
Supports
Markdown
0%
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!
Cancel
Please
register
or
sign in
to comment