diff options
Diffstat (limited to 'toplevel/obligations.ml')
| -rw-r--r-- | toplevel/obligations.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index b4384e77b..74b387dfe 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -590,7 +590,8 @@ let declare_obligation prg obl body = const_entry_opaque = opaque; const_entry_inline_code = false} in - let constant = Declare.declare_constant obl.obl_name + (** ppedrot: seems legit to have obligations as local *) + let constant = Declare.declare_constant obl.obl_name ~local:true (DefinitionEntry ce,IsProof Property) in if not opaque then @@ -945,7 +946,8 @@ let admit_prog prg = match x.obl_body with | None -> let x = subst_deps_obl obls x in - let kn = Declare.declare_constant x.obl_name + (** ppedrot: seems legit to have admitted obligations as local *) + let kn = Declare.declare_constant x.obl_name ~local:true (ParameterEntry (None, x.obl_type,None), IsAssumption Conjectural) in assumption_message x.obl_name; |