aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/obligations.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/obligations.ml')
-rw-r--r--toplevel/obligations.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 18e85266e..9694c2d7f 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -629,7 +629,6 @@ let declare_obligation prg obl body ty 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 ty else None;
- const_entry_proj = None;
const_entry_polymorphic = poly;
const_entry_universes = uctx;
const_entry_opaque = opaque;