diff options
| author | herbelin | 2002-08-13 16:20:47 +0000 |
|---|---|---|
| committer | herbelin | 2002-08-13 16:20:47 +0000 |
| commit | 45134de9fd50a1285d75f5891e376eae09fdd20a (patch) | |
| tree | 5e80fb25c3065ba1489d513cc09a695fb7da8d51 /tactics/tactics.ml | |
| parent | 5c668276b37f09077231c314b03254df6dce3c48 (diff) | |
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
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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) |