From 9cb3549db6a56cae14c0aec0de999b78dd2e0fce Mon Sep 17 00:00:00 2001
From: mohring
Date: Thu, 1 Feb 2001 09:09:41 +0000
Subject: *** empty log message ***

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

(limited to 'proofs')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 58fb8490e2..97590bfb4b 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
-- 
cgit v1.2.3