From 2c94457ca8586534b07c039ddcb1d7d54712dd65 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 5 Oct 2000 19:27:21 +0000
Subject: Suppression d'un Cast inutile

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

diff --git a/proofs/logic.ml b/proofs/logic.ml
index d7b67ba395..9aeff1f28a 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -436,7 +436,7 @@ let prim_refiner r sigma goal =
     | { name = Convert_concl; terms = [cl'] } ->
     	let cl'ty = type_of env sigma cl' in
 	if is_conv_leq env sigma cl' cl then
-          let sg = mk_goal info env (mkCast (cl',cl'ty)) in
+          let sg = mk_goal info env cl' in
           [sg]
 	else 
 	  error "convert-concl rule passed non-converting term"
-- 
cgit v1.2.3