diff options
| author |  Samuel Mimram <samuel.mimram@ens-lyon.org> | 2005-01-31 14:34:14 +0000 |
|---|---|---|
| committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2005-01-31 14:34:14 +0000 |
| commit | 6497f27021fec4e01f2182014f2bb1989b4707f9 (patch) | |
| tree | 473be7e63895a42966970ab6a70998113bc1bd59 /tactics/tactics.ml | |
| parent | 6b649aba925b6f7462da07599fe67ebb12a3460e (diff) | |
Imported Upstream version 8.0pl2upstream/8.0pl2
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cab4f025..b6eaf015 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tactics.ml,v 1.162.2.2 2004/07/16 19:30:55 herbelin Exp $ *) +(* $Id: tactics.ml,v 1.162.2.4 2004/12/04 10:26:46 herbelin Exp $ *) open Pp open Util @@ -654,7 +654,7 @@ let occurrences_of_hyp id cls = let occurrences_of_goal cls = if cls.onconcl then Some cls.concl_occs else None -let everywhere cls = (cls=allClauses) +let in_every_hyp cls = (cls.onhyps = None) (* (* Implementation with generalisation then re-intro: introduces noise *) @@ -721,8 +721,8 @@ let letin_abstract id c occs gl = | None -> depdecls | Some occ -> let newdecl = subst_term_occ_decl occ c d in - if d = newdecl then - if not (everywhere occs) + if occ = [] & d = newdecl then + if not (in_every_hyp occs) then raise (RefinerError (DoesNotOccurIn (c,hyp))) else depdecls else @@ -1175,7 +1175,7 @@ let induct_discharge statuslists destopt avoid' ((avoid7,avoid8),ra) (names,forc (match kind_of_term (pf_concl gl) with | Prod (name,t,_) -> (name,None,t) | LetIn (name,b,t,_) -> (name,Some b,t) - | _ -> assert false)) gl in + | _ -> raise (RefinerError IntroNeedsProduct))) gl in if Options.do_translate() & id7 <> id8 then force := true; let id = if !Options.v7 then id7 else id8 in rnames := !rnames @ [IntroIdentifier id]; @@ -1192,12 +1192,12 @@ let induct_discharge statuslists destopt avoid' ((avoid7,avoid8),ra) (names,forc (match kind_of_term (pf_concl gl) with | Prod (name,t,_) -> (name,None,t) | LetIn (name,b,t,_) -> (name,Some b,t) - | _ -> assert false)) gl in + | _ -> raise (RefinerError IntroNeedsProduct))) gl in let id8 = fresh_id avoid8 (default_id gl (match kind_of_term (pf_concl gl) with | Prod (name,t,_) -> (name,None,t) | LetIn (name,b,t,_) -> (name,Some b,t) - | _ -> assert false)) gl in + | _ -> raise (RefinerError IntroNeedsProduct))) gl in if Options.do_translate() & id7 <> id8 then force := true; let id = if !Options.v7 then id7 else id8 in let avoid = if !Options.v7 then avoid7 else avoid8 in |