diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-20 22:30:37 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-12 10:39:33 +0200 |
| commit | b006f10e7d591417844ffa1f04eeb926d6092d7b (patch) | |
| tree | 9253b32cb1adabafce28f123ef9eb11d4fa122f4 /proofs/clenv.ml | |
| parent | ca300977724a6b065a98c025d400c71f41b9df4b (diff) | |
Uniformisation of the order of arguments env and sigma.
Diffstat (limited to 'proofs/clenv.ml')
| -rw-r--r-- | proofs/clenv.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 6f607133d..612ef8d7d 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 |