diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-08 19:02:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:27:26 +0100 |
| commit | 85ab3e298aa1d7333787c1fa44d25df189ac255c (patch) | |
| tree | 32f661f4ccd3fb36657bb9ac8104a08df9cd1d87 /proofs/clenv.ml | |
| parent | 67dc22d8389234d0c9b329944ff579e7056b7250 (diff) | |
Pretyping API using EConstr.
Diffstat (limited to 'proofs/clenv.ml')
| -rw-r--r-- | proofs/clenv.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 0515e4198..68aeaef5e 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -337,7 +337,7 @@ let clenv_pose_metas_as_evars clenv dep_mvs = let src = evar_source_of_meta mv clenv.evd in let src = adjust_meta_source clenv.evd mv src in let evd = Sigma.Unsafe.of_evar_map clenv.evd in - let Sigma (evar, evd, _) = new_evar (cl_env clenv) evd ~src ty in + let Sigma (evar, evd, _) = new_evar (cl_env clenv) evd ~src (EConstr.of_constr ty) in let evd = Sigma.to_evar_map evd in let clenv = clenv_assign mv evar {clenv with evd=evd} in fold clenv mvs in @@ -610,7 +610,7 @@ let make_evar_clause env sigma ?len t = | Prod (na, t1, t2) -> let store = Typeclasses.set_resolvable Evd.Store.empty false in let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma (ev, sigma, _) = new_evar ~store env sigma t1 in + let Sigma (ev, sigma, _) = new_evar ~store env sigma (EConstr.of_constr t1) in let sigma = Sigma.to_evar_map sigma in let dep = not (EConstr.Vars.noccurn sigma 1 (EConstr.of_constr t2)) in let hole = { |