diff options
| author | Hugo Herbelin | 2014-08-20 22:30:37 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-09-12 10:39:33 +0200 |
| commit | b006f10e7d591417844ffa1f04eeb926d6092d7b (patch) | |
| tree | 9253b32cb1adabafce28f123ef9eb11d4fa122f4 /stm | |
| parent | ca300977724a6b065a98c025d400c71f41b9df4b (diff) | |
Uniformisation of the order of arguments env and sigma.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/lemmas.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/stm/lemmas.ml b/stm/lemmas.ml index bec80f70da..36f2b14cb2 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -434,8 +434,8 @@ let start_proof_com kind thms hook = let env0 = Global.env () in let evdref = ref (Evd.from_env env0) in let thms = List.map (fun (sopt,(bl,t,guard)) -> - let impls, ((env, ctx), imps) = interp_context_evars evdref env0 bl in - let t', imps' = interp_type_evars_impls ~impls evdref env t in + let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in + let t', imps' = interp_type_evars_impls ~impls env evdref t in check_evars_are_solved env Evd.empty !evdref; let ids = List.map pi1 ctx in (compute_proof_name (pi1 kind) sopt, |