diff options
Diffstat (limited to 'plugins/subtac')
| -rw-r--r-- | plugins/subtac/subtac_command.ml | 3 | ||||
| -rw-r--r-- | plugins/subtac/subtac_obligations.ml | 6 |
2 files changed, 6 insertions, 3 deletions
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml index f02e83ad1a..ecae6759f0 100644 --- a/plugins/subtac/subtac_command.ml +++ b/plugins/subtac/subtac_command.ml @@ -325,7 +325,8 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = let body = it_mkLambda_or_LetIn (mkApp (constr_of_global gr, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in let ce = - { const_entry_body = Evarutil.nf_evar !isevars body; + { const_entry_body = Evarutil.nf_evar !isevars body; + const_entry_secctx = None; const_entry_type = Some ty; const_entry_opaque = false } in diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index a719a9f9af..64d9f72cae 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -248,6 +248,7 @@ let declare_definition prg = let (local, kind) = prg.prg_kind in let ce = { const_entry_body = body; + const_entry_secctx = None; const_entry_type = Some typ; const_entry_opaque = false } in @@ -347,6 +348,7 @@ let declare_obligation prg obl body = let opaque = if get_proofs_transparency () then false else opaque in let ce = { const_entry_body = body; + const_entry_secctx = None; const_entry_type = Some ty; const_entry_opaque = opaque } in @@ -661,8 +663,8 @@ let admit_obligations n = match x.obl_body with | None -> let x = subst_deps_obl obls x in - let kn = Declare.declare_constant x.obl_name (ParameterEntry (x.obl_type,None), - IsAssumption Conjectural) + let kn = Declare.declare_constant x.obl_name + (ParameterEntry (None, x.obl_type,None), IsAssumption Conjectural) in assumption_message x.obl_name; obls.(i) <- { x with obl_body = Some (mkConst kn) } |