*** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1307 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 0 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 58fb8490e..97590bfb4 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -63,6 +63,12 @@ let conv_leq_goal env sigma arg ty conclty =
 let rec mk_refgoals sigma goal goalacc conclty trm =
   let env = evar_env goal in
   let hyps = goal.evar_hyps in
+(*  if  not (occur_meta trm) then
+    let t'ty = (unsafe_machine env sigma trm).uj_type in 	
+    let _ = conv_leq_goal env sigma trm t'ty conclty in
+      (goalacc,t'ty)
+  else
+*)
   match kind_of_term trm with
     | IsMeta mv ->
 	if occur_meta conclty then