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 /proofs | |
| parent | ca300977724a6b065a98c025d400c71f41b9df4b (diff) | |
Uniformisation of the order of arguments env and sigma.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 3 | ||||
| -rw-r--r-- | proofs/evar_refiner.ml | 2 | ||||
| -rw-r--r-- | proofs/proofview.ml | 6 |
3 files changed, 5 insertions, 6 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 6f607133d7..612ef8d7da 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -335,8 +335,7 @@ let clenv_pose_metas_as_evars clenv dep_mvs = else let src = evar_source_of_meta mv clenv.evd in let src = adjust_meta_source clenv.evd mv src in - let (evd,evar) = - new_evar clenv.evd (cl_env clenv) ~src ty in + let (evd,evar) = new_evar (cl_env clenv) clenv.evd ~src ty in let clenv = clenv_assign mv evar {clenv with evd=evd} in fold clenv mvs in fold clenv dep_mvs diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 5f97e72fab..564ea4dd8a 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -50,7 +50,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = Pretyping.fail_evar = false; Pretyping.expand_evars = true } in try Pretyping.understand_ltac flags - sigma env ltac_var (Pretyping.OfType evi.evar_concl) rawc + env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc with e when Errors.noncritical e -> let loc = Glob_ops.loc_of_glob_constr rawc in user_err_loc diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 0acfda3d80..a5cb2edb85 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -40,7 +40,7 @@ let init sigma = | (env, typ) :: l -> let ret, { solution = sol; comb = comb } = aux l in let src = (Loc.ghost,Evar_kinds.GoalEvar) in - let (new_defs , econstr) = Evarutil.new_evar sol env ~src typ in + let (new_defs , econstr) = Evarutil.new_evar env sol ~src typ in let (e, _) = Term.destEvar econstr in let gl = Goal.build e in let entry = (econstr, typ) :: ret in @@ -59,7 +59,7 @@ let dependent_init = let rec aux = function | TNil sigma -> [], { solution = sigma; comb = []; } | TCons (env, sigma, typ, t) -> - let (sigma, econstr ) = Evarutil.new_evar sigma env typ in + let (sigma, econstr ) = Evarutil.new_evar env sigma typ in let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in let (e, _) = Term.destEvar econstr in let gl = Goal.build e in @@ -950,7 +950,7 @@ struct let new_evar (evd, evs) env typ = let src = (Loc.ghost, Evar_kinds.GoalEvar) in - let (evd, ev) = Evarutil.new_evar evd env ~src typ in + let (evd, ev) = Evarutil.new_evar env evd ~src typ in let evd = Typeclasses.mark_unresolvables ~filter:(fun ev' _ -> Evar.equal (fst (Term.destEvar ev)) ev') evd in let (evk, _) = Term.destEvar ev in |