From a3d686a3bd1ac4256279a77c291949a3b15abc18 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 13 Apr 2015 16:44:22 +0200
Subject: Program: Do not reduce obligation types preemptively, only at
 definition time. The obligation tactic or user can still choose to do so.

---
 toplevel/obligations.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
cgit v1.2.3