diff options
| author | Pierre-Marie Pédrot | 2016-11-06 17:21:44 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:25:30 +0100 |
| commit | e27949240f5b1ee212e7d0fe3326a21a13c4abb0 (patch) | |
| tree | bf076ea31e6ca36cc80e0f978bc63d112e183725 /ltac/tacinterp.ml | |
| parent | b365304d32db443194b7eaadda63c784814f53f1 (diff) | |
Typing API using EConstr.
Diffstat (limited to 'ltac/tacinterp.ml')
| -rw-r--r-- | ltac/tacinterp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 34faa028f2..8f5ac7e766 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -791,7 +791,7 @@ let interp_may_eval f ist env sigma = function let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in let evdref = ref sigma in let c = subst_meta [Constr_matching.special_meta,ic] ctxt in - let c = Typing.e_solve_evars env evdref c in + let c = Typing.e_solve_evars env evdref (EConstr.of_constr c) in !evdref , c with | Not_found -> @@ -799,7 +799,7 @@ let interp_may_eval f ist env sigma = function (str "Unbound context identifier" ++ pr_id s ++ str".")) | ConstrTypeOf c -> let (sigma,c_interp) = f ist env sigma c in - Typing.type_of ~refresh:true env sigma c_interp + Typing.type_of ~refresh:true env sigma (EConstr.of_constr c_interp) | ConstrTerm c -> try f ist env sigma c |