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 /plugins/decl_mode/decl_proof_instr.ml | |
| parent | ca300977724a6b065a98c025d400c71f41b9df4b (diff) | |
Uniformisation of the order of arguments env and sigma.
Diffstat (limited to 'plugins/decl_mode/decl_proof_instr.ml')
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index c5a474d39f..422b7c4995 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1278,7 +1278,7 @@ let understand_my_constr c gls = | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand,None) | rc -> map_glob_constr frob rc in - Pretyping.understand_tcc (sig_sig gls) env ~expected_type:(Pretyping.OfType (pf_concl gls)) (frob rawc) + Pretyping.understand_tcc env (sig_sig gls) ~expected_type:(Pretyping.OfType (pf_concl gls)) (frob rawc) let my_refine c gls = let oc = understand_my_constr c gls in @@ -1458,7 +1458,7 @@ let do_instr raw_instr pts = let ist = {ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; genv = env} in let glob_instr = intern_proof_instr ist raw_instr in let instr = - interp_proof_instr (get_its_info gl) sigma env glob_instr in + interp_proof_instr (get_its_info gl) env sigma glob_instr in ignore (Pfedit.by (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp))) else () end; postprocess pts raw_instr.instr; |