diff options
Diffstat (limited to 'plugins/derive')
| -rw-r--r-- | plugins/derive/derive.ml | 4 | ||||
| -rw-r--r-- | plugins/derive/g_derive.ml4 | 2 |
2 files changed, 4 insertions, 2 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index e39d17b52d..12d7f06603 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -28,12 +28,14 @@ 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 diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4 index d4dc7e0eed..deadb3b4d5 100644 --- a/plugins/derive/g_derive.ml4 +++ b/plugins/derive/g_derive.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Constrarg +open Stdarg (*i camlp4deps: "grammar/grammar.cma" i*) |