From 2289472271cf56d3af77fbbe634b643eac474a13 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 5 Sep 2005 16:47:07 +0000 Subject: [PATCH] locate_in_* functions generalized to handle equalities in a context. Usually only the context length is used (to compute some lifting factor). --- helm/ocaml/tactics/proofEngineHelpers.ml | 8 ++++---- helm/ocaml/tactics/proofEngineHelpers.mli | 10 +++++----- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index 284098f3b..5c9b1f7a0 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -570,11 +570,11 @@ exception Fail of string * [equality] defaults to physical equality * [context] must be the context of [where] *) -let locate_in_term ?(equality=(==))what ~where context = +let locate_in_term ?(equality=(fun _ -> (==))) what ~where context = let add_ctx context name entry = (Some (name, entry)) :: context in let rec aux context where = - if equality what where then [context,where] + if equality context what where then [context,where] else match where with | Cic.Implicit _ @@ -617,13 +617,13 @@ let locate_in_term ?(equality=(==))what ~where context = in aux context where -(** locate_in_term equality what where context +(** locate_in_conjecture equality what where context * [what] must match a subterm of [where] according to [equality] * It returns the matched terms together with their contexts in [where] * [equality] defaults to physical equality * [context] must be the context of [where] *) -let locate_in_conjecture ?(equality=(==)) what (_,context,ty) = +let locate_in_conjecture ?(equality=fun _ -> (==)) what (_,context,ty) = let context,res = List.fold_right (fun entry (context,res) -> diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli index 4dad92917..6d1c7ffaa 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.mli +++ b/helm/ocaml/tactics/proofEngineHelpers.mli @@ -90,18 +90,18 @@ val select: * [context] must be the context of [where] *) val locate_in_term: - ?equality:(Cic.term -> Cic.term -> bool) -> Cic.term -> where:Cic.term -> - Cic.context -> (Cic.context * Cic.term) list + ?equality:(Cic.context -> Cic.term -> Cic.term -> bool) -> + Cic.term -> where:Cic.term -> Cic.context -> (Cic.context * Cic.term) list -(** locate_in_term equality what where context +(** locate_in_conjecture equality what where context * [what] must match a subterm of [where] according to [equality] * It returns the matched terms together with their contexts in [where] * [equality] defaults to physical equality * [context] must be the context of [where] *) val locate_in_conjecture: - ?equality:(Cic.term -> Cic.term -> bool) -> Cic.term -> Cic.conjecture -> - (Cic.context * Cic.term) list + ?equality:(Cic.context -> Cic.term -> Cic.term -> bool) -> + Cic.term -> Cic.conjecture -> (Cic.context * Cic.term) list (* saturate_term newmeta metasenv context ty *) (* Given a type [ty] (a backbone), it returns its head and a new metasenv in *) -- 2.39.2