From 45134de9fd50a1285d75f5891e376eae09fdd20a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 13 Aug 2002 16:20:47 +0000
Subject: Renoncement à distinguer les types "constr" et "types"; nettoyage

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

(limited to 'tactics/tactics.ml')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 37da503fd8..62c95b53fe 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -396,8 +396,8 @@ let rec intros_move = function
 
 let dependent_in_decl a (_,c,t) =
   match c with
-    | None -> dependent a (body_of_type t)
-    | Some body -> dependent a body || dependent a (body_of_type t)
+    | None -> dependent a t
+    | Some body -> dependent a body || dependent a t
 
 let move_to_rhyp rhyp gl =
   let rec get_lhyp lastfixed depdecls = function
@@ -757,7 +757,7 @@ let (assumption : tactic) = fun gl ->
   let rec arec = function
     | [] -> error "No such assumption"
     | (id,c,t)::rest -> 
-	if pf_conv_x_leq gl (body_of_type t) concl then refine (mkVar id) gl
+	if pf_conv_x_leq gl t concl then refine (mkVar id) gl
 	else arec rest
   in
   arec (pf_hyps gl)
-- 
cgit v1.2.3