diff options
| author | Matthieu Sozeau | 2015-04-13 16:44:22 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-04-13 16:48:07 +0200 |
| commit | a3d686a3bd1ac4256279a77c291949a3b15abc18 (patch) | |
| tree | 8b856f81fbf3edd04c21595e5ec970d07b2ce55a | |
| parent | 546e2454f244340694f8fca460598499359afe28 (diff) | |
Program: Do not reduce obligation types preemptively, only at
definition time. The obligation tactic or user can still choose to do so.
| -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 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 |