summaryrefslogtreecommitdiff
path: root/proofs/refiner.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/refiner.ml')
-rw-r--r--proofs/refiner.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index a9a1f51d..7ce256bf 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: refiner.ml 11865 2009-01-28 17:34:30Z herbelin $ *)
+(* $Id: refiner.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Pp
open Util
@@ -763,7 +763,7 @@ let extract_pftreestate pts =
else
str "Attempt to save a proof with existential variables still non-instantiated");
let env = Global.env_of_context pts.tpf.goal.evar_hyps in
- nf_betaiotaevar_preserving_vm_cast env pts.tpfsigma pfterm
+ nf_betaiota_preserving_vm_cast env pts.tpfsigma pfterm
(* strong whd_betaiotaevar env pts.tpfsigma pfterm *)
(***
local_strong (Evarutil.whd_ise (ts_it pts.tpfsigma)) pfterm