diff options
Diffstat (limited to 'contrib/funind/tacinv.ml4')
| -rw-r--r-- | contrib/funind/tacinv.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4 index 717cf6421..7d7de9de4 100644 --- a/contrib/funind/tacinv.ml4 +++ b/contrib/funind/tacinv.ml4 @@ -815,7 +815,8 @@ let declareFunScheme f fname mutflist = let ce = { const_entry_body = scheme; const_entry_type = None; - const_entry_opaque = false } in + const_entry_opaque = false; + const_entry_boxed = true } in let _= ignore (declare_constant fname (DefinitionEntry ce,IsDefinition)) in () |