From c8c8ccdaaffefdbd3d78c844552a08bcb7b4f915 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 02:12:40 +0100 Subject: Evar-normalizing functions now act on EConstrs. --- plugins/derive/derive.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'plugins/derive') diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index f23f4ce7d..12d7f0660 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -28,16 +28,17 @@ let start_deriving f suchthat lemma = (* spiwack: I don't know what the rigidity flag does, picked the one that looked the most general. *) let (sigma,f_type_sort) = Evd.new_sort_variable Evd.univ_flexible_alg sigma in - let f_type_type = Term.mkSort f_type_sort in + let f_type_type = EConstr.mkSort f_type_sort in (** create the initial goals for the proof: |- Type ; |- ?1 ; f:=?2 |- suchthat *) let goals = let open Proofview in TCons ( env , sigma , f_type_type , (fun sigma f_type -> TCons ( env , sigma , f_type , (fun sigma ef -> + let f_type = EConstr.Unsafe.to_constr f_type in + let ef = EConstr.Unsafe.to_constr ef in let env' = Environ.push_named (LocalDef (f, ef, f_type)) env in let evdref = ref sigma in let suchthat = Constrintern.interp_type_evars env' evdref suchthat in - let suchthat = EConstr.Unsafe.to_constr suchthat in TCons ( env' , !evdref , suchthat , (fun sigma _ -> TNil sigma)))))) in -- cgit v1.2.3