diff options
Diffstat (limited to 'vernac/indschemes.ml')
| -rw-r--r-- | vernac/indschemes.ml | 20 |
1 files changed, 5 insertions, 15 deletions
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 18955c2ba3..a6c577a878 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -98,19 +98,11 @@ let () = (* Util *) -let define ~poly name sigma c t = +let define ~poly name sigma c types = let f = declare_constant ~kind:Decls.(IsDefinition Scheme) in let univs = Evd.univ_entry ~poly sigma in - let kn = f ~name - (DefinitionEntry - { proof_entry_body = c; - proof_entry_secctx = None; - proof_entry_type = t; - proof_entry_universes = univs; - proof_entry_opaque = false; - proof_entry_inline_code = false; - proof_entry_feedback = None; - }) in + let entry = Declare.definition_entry ~univs ?types c in + let kn = f ~name (DefinitionEntry entry) in definition_message name; kn @@ -411,8 +403,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort = let declare decl fi lrecref = let decltype = Retyping.get_type_of env0 sigma (EConstr.of_constr decl) in let decltype = EConstr.to_constr sigma decltype in - let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Evd.empty_side_effects) in - let cst = define ~poly fi sigma proof_output (Some decltype) in + let cst = define ~poly fi sigma decl (Some decltype) in GlobRef.ConstRef cst :: lrecref in let _ = List.fold_right2 declare listdecl lrecnames [] in @@ -533,7 +524,6 @@ let do_combined_scheme name schemes = schemes in let sigma,body,typ = build_combined_scheme (Global.env ()) csts in - let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Evd.empty_side_effects) in (* It is possible for the constants to have different universe polymorphism from each other, however that is only when the user manually defined at least one of them (as Scheme would pick the @@ -541,7 +531,7 @@ let do_combined_scheme name schemes = some other polymorphism they can also manually define the combined scheme. *) let poly = Global.is_polymorphic (GlobRef.ConstRef (List.hd csts)) in - ignore (define ~poly name.v sigma proof_output (Some typ)); + ignore (define ~poly name.v sigma body (Some typ)); fixpoint_message None [name.v] (**********************************************************************) |