diff options
Diffstat (limited to 'contrib/extraction')
| -rw-r--r-- | contrib/extraction/modutil.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml index eb5c274502..519565888a 100644 --- a/contrib/extraction/modutil.ml +++ b/contrib/extraction/modutil.ml @@ -49,7 +49,10 @@ let rec subst_module sub mb = mod_type=mtb'; mod_user_type=mtb''; mod_equiv=mpo'; - mod_constraints=mb.mod_constraints } + mod_constraints=mb.mod_constraints; + mod_retroknowledge=[] } (* spiwack: since I'm lazy and it's unused at + this point. I forget about retroknowledge, + this may need a change later *) and subst_meb sub = function | MEBident mp -> MEBident (subst_mp sub mp) |