aboutsummaryrefslogtreecommitdiff
path: root/toplevel/obligations.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/obligations.ml')
-rw-r--r--toplevel/obligations.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 456a6f9d0f..523134b50f 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -658,7 +658,7 @@ let init_prog_info ?(opaque = false) n b t ctx deps fixkind notations obls impls
Array.mapi
(fun i (n, t, l, o, d, tac) ->
{ obl_name = n ; obl_body = None;
- obl_location = l; obl_type = reduce t; obl_status = o;
+ obl_location = l; obl_type = t; obl_status = o;
obl_deps = d; obl_tac = tac })
obls, b
in