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/coercion.ml | |
| parent | a5499688bd76def8de3d8e1089a49c7a08430903 (diff) | |
Removing various compatibility layers of tactics.
Diffstat (limited to 'pretyping/coercion.ml')
| -rw-r--r-- | pretyping/coercion.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index f569d9fc4..ead44cee2 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -194,7 +194,7 @@ and coerce loc env evdref (x : EConstr.constr) (y : EConstr.constr) (subst1 hdy restT') (succ i) (fun x -> eq_app (co x)) else Some (fun x -> let term = co x in - EConstr.of_constr (Typing.e_solve_evars env evdref term)) + Typing.e_solve_evars env evdref term) in if isEvar !evdref c || isEvar !evdref c' || not (Program.is_program_generalized_coercion ()) then (* Second-order unification needed. *) @@ -302,7 +302,7 @@ and coerce loc env evdref (x : EConstr.constr) (y : EConstr.constr) with NoSubtacCoercion -> let typ = Typing.unsafe_type_of env evm c in let typ' = Typing.unsafe_type_of env evm c' in - coerce_application (EConstr.of_constr typ) (EConstr.of_constr typ') c c' l l') + coerce_application typ typ' c c' l l') else subco () | x, y when EConstr.eq_constr !evdref c c' -> @@ -310,7 +310,7 @@ and coerce loc env evdref (x : EConstr.constr) (y : EConstr.constr) let evm = !evdref in let lam_type = Typing.unsafe_type_of env evm c in let lam_type' = Typing.unsafe_type_of env evm c' in - coerce_application (EConstr.of_constr lam_type) (EConstr.of_constr lam_type') c c' l l' + coerce_application lam_type lam_type' c c' l l' else subco () | _ -> subco ()) | _, _ -> subco () @@ -341,7 +341,7 @@ let app_coercion env evdref coercion v = | None -> v | Some f -> let v' = Typing.e_solve_evars env evdref (f v) in - whd_betaiota !evdref (EConstr.of_constr v') + whd_betaiota !evdref v' let coerce_itf loc env evd v t c1 = let evdref = ref evd in |