From 3202740c95ba4b662b7f96533fccdff522e67e24 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 26 Jul 2005 15:25:47 +0000 Subject: [PATCH] Implementation of locate_in finished. --- helm/ocaml/tactics/proofEngineHelpers.ml | 43 +++++++++--------------- 1 file changed, 16 insertions(+), 27 deletions(-) diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index 4224eb5b1..a0fef6037 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -574,40 +574,29 @@ let locate_in_term what ~where = | Cic.Prod (name, s, t) | Cic.Lambda (name, s, t) -> aux context s @ aux (add_ctx context name (Cic.Decl s)) t + | Cic.LetIn (name, s, t) -> + aux context s @ aux (add_ctx context name (Cic.Def (s,None))) t | Cic.Appl tl -> auxs context tl -(* - | Cic.LetIn (Cic.Anonymous, s1, t1), Cic.LetIn (name, s2, t2) -> - aux context s1 s2 @ aux (add_ctx context name (Cic.Def (s2,None))) t1 t2 - | Cic.LetIn (Cic.Name n1, s1, t1), - Cic.LetIn ((Cic.Name n2) as name, s2, t2) when n1 = n2-> - aux context s1 s2 @ aux (add_ctx context name (Cic.Def (s2,None))) t1 t2 - | Cic.LetIn (name1, s1, t1), Cic.LetIn (name2, s2, t2) -> [] - | Cic.MutCase (_, _, out1, t1, pat1), Cic.MutCase (_ , _, out2, t2, pat2) -> - aux context out1 out2 @ aux context t1 t2 @ auxs context pat1 pat2 - | Cic.Fix (_, funs1), Cic.Fix (_, funs2) -> + | Cic.MutCase (_, _, out, t, pat) -> + aux context out @ aux context t @ auxs context pat + | Cic.Fix (_, funs) -> let tys = - List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs2 + List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs in List.concat - (List.map2 - (fun (_, _, ty1, bo1) (_, _, ty2, bo2) -> - aux context ty1 ty2 @ aux (tys @ context) bo1 bo2) - funs1 funs2) - | Cic.CoFix (_, funs1), Cic.CoFix (_, funs2) -> + (List.map + (fun (_, _, ty, bo) -> + aux context ty @ aux (tys @ context) bo) + funs) + | Cic.CoFix (_, funs) -> let tys = - List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs2 + List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs in List.concat - (List.map2 - (fun (_, ty1, bo1) (_, ty2, bo2) -> - aux context ty1 ty2 @ aux (tys @ context) bo1 bo2) - funs1 funs2) - | x,y -> - raise (Bad_pattern - (Printf.sprintf "Pattern %s versus term %s" - (CicPp.ppterm x) - (CicPp.ppterm y))) -*) + (List.map + (fun (_, ty, bo) -> + aux context ty @ aux (tys @ context) bo) + funs) and auxs context tl = (* as aux for list of terms *) List.concat (List.map (fun t -> aux context t) tl) in -- 2.39.2