diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-26 00:12:09 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-26 00:12:09 +0200 |
| commit | 64041ca0c17430085c20b7754277313fdb439a6a (patch) | |
| tree | 9691a886243539f35ad7e93a2bb9bc6427d91307 /pretyping | |
| parent | 109c90efd0dd2bfbeb6c29b263ccd9b2e84e5b9e (diff) | |
Fix compilation error due to commented code in previous commit by Hugo.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/unification.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 34fac5e75..5f7e2916b 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1193,8 +1193,8 @@ let indirect_dependency d decls = pi1 (List.hd (List.filter (fun (id,_,_) -> dependent_in_decl (mkVar id) d) decls)) let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env initial_sigma (sigma,c) = -(* let sigma = Pretyping.solve_remaining_evars flags env initial_sigma sigma -in*) Evd.evar_universe_context sigma, nf_evar sigma c + let sigma = Pretyping.solve_remaining_evars flags env initial_sigma sigma + in Evd.evar_universe_context sigma, nf_evar sigma c let default_matching_flags sigma = { modulo_conv_on_closed_terms = Some empty_transparent_state; |