diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-25 18:34:53 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:41 +0100 |
| commit | 02dd160233adc784eac732d97a88356d1f0eaf9b (patch) | |
| tree | d2baacdc2a4ae06e4607bfe09b48ba2c23a78a0f /pretyping/typing.ml | |
| parent | a5499688bd76def8de3d8e1089a49c7a08430903 (diff) | |
Removing various compatibility layers of tactics.
Diffstat (limited to 'pretyping/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index d24160ea5..7baff421f 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -376,7 +376,7 @@ let unsafe_type_of env evd c = let evdref = ref evd in let env = enrich_env env evdref in let j = execute env evdref c in - EConstr.Unsafe.to_constr j.uj_type + j.uj_type (* Sort of a type *) @@ -411,6 +411,6 @@ let e_solve_evars env evdref c = let env = enrich_env env evdref in let c = (execute env evdref c).uj_val in (* side-effect on evdref *) - nf_evar !evdref (EConstr.Unsafe.to_constr c) + EConstr.of_constr (nf_evar !evdref (EConstr.Unsafe.to_constr c)) -let _ = Evarconv.set_solve_evars (fun env evdref c -> EConstr.of_constr (e_solve_evars env evdref c)) +let _ = Evarconv.set_solve_evars (fun env evdref c -> e_solve_evars env evdref c) |