diff options
| author | Hugo Herbelin | 2018-09-05 21:56:06 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-05 22:26:59 +0200 |
| commit | 899f3eb1f65ad2e6a3fababa0213ac63e2501bbe (patch) | |
| tree | 301b3ecc7729b38ef1f2066910ff6ea298db8e6c /vernac | |
| parent | 579f30a53809f9cf73aa3d7c69960b50fc51c7fc (diff) | |
Fixing #8416 (Print Assumptions missing module information from compiled files).
This fixes the fix 1522b989 to #7192.
The remaining Not_found after 1522b989 should have rung a bell that
something was still strange.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/assumptions.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 765f962e99..e5d2382e46 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -70,7 +70,7 @@ let rec fields_of_functor f subs mp0 args = function let rec lookup_module_in_impl mp = match mp with - | MPfile _ -> raise Not_found + | MPfile _ -> Global.lookup_module mp | MPbound _ -> assert false | MPdot (mp',lab') -> if ModPath.equal mp' (Global.current_modpath ()) then |