diff options
author | 2005-01-31 14:34:14 +0000 | |
---|---|---|
committer | 2005-01-31 14:34:14 +0000 | |
commit | e669490d0d5e6ed4bb45c895194791f01d038637 (patch) | |
tree | 4eb40b447e6573dbaa1cf593a2cae6758850cb7c /tactics/tactics.ml | |
parent | d334716fb2d09dd3304f98ee0dbf39275eac010b (diff) | |
parent | 6497f27021fec4e01f2182014f2bb1989b4707f9 (diff) |
Merge commit 'upstream/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 |