diff options
| author | Pierre-Marie Pédrot | 2016-11-05 21:36:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:23:53 +0100 |
| commit | b7fd585b89ac5e0b7770f52739c33fe179f2eed8 (patch) | |
| tree | 83ab6fe2ccecb503691c9842ba7eec27690ad975 /tactics | |
| parent | 147afe827dc83602cc160a8b1357e84ecea910ff (diff) | |
Evarsolve API using EConstr.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 22d01e4011..1c10cdfea2 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -788,7 +788,7 @@ let check_types env sigma mayneedglobalcheck deep newc origc = if deep then begin let t2 = Retyping.get_type_of env sigma (EConstr.of_constr origc) in let sigma, t2 = Evarsolve.refresh_universes - ~onlyalg:true (Some false) env sigma t2 in + ~onlyalg:true (Some false) env sigma (EConstr.of_constr t2) in let sigma, b = infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 in if not b then if @@ -2604,7 +2604,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = let Sigma (t, sigma, p) = match ty with | Some t -> Sigma.here t sigma | None -> - let t = typ_of env sigma (EConstr.of_constr c) in + let t = EConstr.of_constr (typ_of env sigma (EConstr.of_constr c)) in let sigma, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env (Sigma.to_evar_map sigma) t in Sigma.Unsafe.of_pair (c, sigma) in @@ -3621,7 +3621,7 @@ let abstract_args gl generalize_vars dep id defined f args = RelDecl.get_name decl, RelDecl.get_type decl, c in let argty = Tacmach.pf_unsafe_type_of gl arg in - let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma ty in + let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma (EConstr.of_constr ty) in let () = sigma := sigma' in let lenctx = List.length ctx in let liftargty = lift lenctx argty in |