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

1 files changed, 4 insertions, 3 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 0368e9744..48ed610b9 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;