From 99c8b69f5ef0f92b26ec23be06743312846f5af3 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 9 Apr 2014 15:31:39 +0200 Subject: Fix derive plugin to properly treat universes --- plugins/Derive/derive.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'plugins/Derive') diff --git a/plugins/Derive/derive.ml b/plugins/Derive/derive.ml index 906f5e383..160e905f8 100644 --- a/plugins/Derive/derive.ml +++ b/plugins/Derive/derive.ml @@ -14,8 +14,8 @@ let interp_init_def_and_relation env sigma init_def r = let open Term in mkProd (Names.Anonymous,init_type, mkProd (Names.Anonymous,init_type,mkProp)) in - let r, _ = Constrintern.interp_casted_constr sigma env r r_type in - init_def , init_type , r + let r, ctx = Constrintern.interp_casted_constr sigma env r r_type in + init_def , init_type , r, Evd.evar_universe_context_set ctx (** [start_deriving f init r lemma] starts a proof of [r init @@ -24,13 +24,13 @@ let interp_init_def_and_relation env sigma init_def r = let start_deriving f init_def r lemma = let env = Global.env () in let kind = Decl_kinds.(Global,false,DefinitionBody Definition) in - let ( init_def , init_type , r ) = + let ( init_def , init_type , r , ctx ) = interp_init_def_and_relation env Evd.empty init_def r in let goals = let open Proofview in - TCons ( env , init_type , (fun ef -> - TCons ( env , Term.mkApp ( r , [| init_def ; ef |] ) , (fun _ -> TNil)))) + TCons ( env , (init_type , ctx ) , (fun ef -> + TCons ( env , ( Term.mkApp ( r , [| init_def ; ef |] ) , Univ.ContextSet.empty) , (fun _ -> TNil)))) in let terminator com = let open Proof_global in -- cgit v1.2.3