From a3ed9ca5ff6563d05d2940727e4fa335fdaaeb0f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 26 Jul 2005 16:47:18 +0000 Subject: [PATCH] Comments added. --- helm/ocaml/tactics/proofEngineHelpers.ml | 3 +++ helm/ocaml/tactics/proofEngineHelpers.mli | 3 +++ 2 files changed, 6 insertions(+) diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index a0fef6037..4bb46fc4c 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -554,6 +554,9 @@ exception Fail of string in subst,metasenv,ugraph,context_terms, ty_terms +(** locate_in_term what where +* [what] must be a physical pointer to a subterm of [where] +* It returns the context of [what] in [where] *) let locate_in_term what ~where = let add_ctx context name entry = (Some (name, entry)) :: context diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli index b04f13139..78dc22c1c 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.mli +++ b/helm/ocaml/tactics/proofEngineHelpers.mli @@ -80,6 +80,9 @@ val select: ] option list * (Cic.context * Cic.term) list +(** locate_in_term what where +* [what] must be a physical pointer to a subterm of [where] +* It returns the context of [what] in [where] *) val locate_in_term: Cic.term -> where:Cic.term -> Cic.context (* saturate_term newmeta metasenv context ty *) -- 2.39.2