diff options
Diffstat (limited to 'toplevel/obligations.ml')
| -rw-r--r-- | toplevel/obligations.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 1543c5e87..067b92554 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -636,7 +636,7 @@ let declare_obligation prg obl body uctx = { const_entry_body = Future.from_val((body,Univ.ContextSet.empty),Declareops.no_seff); const_entry_secctx = None; const_entry_type = if List.is_empty ctx then Some ty else None; - const_entry_proj = None; + const_entry_proj = false; const_entry_polymorphic = poly; const_entry_universes = uctx; const_entry_opaque = opaque; |