Fix instantiation of a module containing USE.

[kape1395]

It was failing before with tlapm ending abnormally with Failure("unknown bound variable").

This fixes a case mentioned in #151 (comment)

[muenchnerkindl]

I am afraid I know nothing about this part of the code, and I'd prefer if @damiendoligez or @johnyf could have a look.

[johnyf]

The change looks good to me, based on Module.Elab.normalize, which appends the hypotheses of the module-scope USE statement to the context via let cx = Deque.append_list cx (hyps_of_modunit mu) in which is used in the case of Mutate statements. In Module.T.hyps_of_modunit the case of USE statements returns the USE facts, with indices shifted depending on the fact's position.

The cause of the error appears to be that the context used during the module traversal did not have the USE facts, so the indexing of Op within OpAll would not point to where Op is defined. The error message "unknown bound variable" appears to originate from Expr.T.get_val_from_id, which is used to retrieve hypotheses from the context, based on their index. By adding let cx = update_cx cx mu in to the Mutate case, the USE facts are appended to the traversal's context, so that the occurrence Op in \A x : Op(x) will resolve to where Op is defined, which is before the USE statement.