diff options
Diffstat (limited to 'toplevel/indschemes.ml')
| -rw-r--r-- | toplevel/indschemes.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index ae8ee7670..0b021254e 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -371,7 +371,7 @@ let do_mutual_induction_scheme lnamedepindsort = let declare decl fi lrecref = let decltype = Retyping.get_type_of env0 sigma decl in (* let decltype = refresh_universes decltype in *) - let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Declareops.no_seff) in + let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in let cst = define fi UserIndividualRequest sigma proof_output (Some decltype) in ConstRef cst :: lrecref in @@ -469,7 +469,7 @@ let do_combined_scheme name schemes = schemes in let body,typ = build_combined_scheme (Global.env ()) csts in - let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Declareops.no_seff) in + let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in ignore (define (snd name) UserIndividualRequest Evd.empty proof_output (Some typ)); fixpoint_message None [snd name] |