diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index da4233c72..209331185 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -579,7 +579,7 @@ let clenv_merge with_types = else let mc,ec = let mvty = clenv_instance_type clenv mv in - if with_types or occur_meta mvty then + if with_types (* or occur_meta mvty *) then let nty = clenv_type_of clenv (clenv_instance clenv (mk_freelisted n)) in unify_0 [] clenv.hook mvty nty |