diff options
| author | Pierre-Marie Pédrot | 2017-09-05 21:51:59 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-05 21:51:59 +0200 |
| commit | 217bd80b651d2d12b05f74cf21485eb0fea8e3e3 (patch) | |
| tree | 7a24bab2b35db7a35d7a69804e5c3f2c445c4f7c | |
| parent | 53c63e43a3daf99cf8bd44498b1c53798a8ba876 (diff) | |
Refine does not evar-normalizes the goal preemptively.
| -rw-r--r-- | src/tac2core.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml index 37f1c99b15..cd39cb6f27 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -734,7 +734,8 @@ end (** (unit -> constr) -> unit *) let () = define1 "refine" begin fun bt c -> let c = thaw bt c >>= fun c -> Proofview.tclUNIT ((), Value.to_constr c) in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> + let gl = Proofview.Goal.assume gl in Refine.generic_refine ~typecheck:true c gl end >>= fun () -> return v_unit end |