From ca3131d423dd32a8b02a2ca5eb9074dff2cae1b7 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sat, 25 Oct 2008 11:41:58 +0000
Subject: Fix for bug #1981, correct the mismatch between the meta types used
 in clenv and the ones found in the refiner.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11502 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/logic.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 0368e97446..48ed610b94 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -251,9 +251,10 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 *)
   match kind_of_term trm with
     | Meta _ ->
-	if !check && occur_meta conclty then
-	  raise (RefinerError (MetaInType conclty));
-	(mk_goal hyps (nf_betaiota conclty))::goalacc, conclty
+	let conclty = nf_betaiota conclty in
+	  if !check && occur_meta conclty then
+	    raise (RefinerError (MetaInType conclty));
+	  (mk_goal hyps conclty)::goalacc, conclty
 
     | Cast (t,_, ty) ->
 	check_typability env sigma ty;
-- 
cgit v1.2.3