From a3b863935bfacffb76ccc913c737be53b840ffe4 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 14 Mar 2003 18:45:41 +0000 Subject: [PATCH] Comment fixed. --- helm/ocaml/tactics/proofEngineHelpers.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli index a1e4d21b6..0e2244f43 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.mli +++ b/helm/ocaml/tactics/proofEngineHelpers.mli @@ -30,8 +30,8 @@ val mk_fresh_name : ProofEngineTypes.mk_fresh_name_type (* identity_relocation_list_for_metavariable i canonical_context *) -(* returns the identity relocation list, which is the list [1 ; ... ; n] *) -(* where n = List.length [canonical_context] *) +(* returns the identity relocation list, which is the list *) +(* [Rel 1 ; ... ; Rel n] where n = List.length [canonical_context] *) val identity_relocation_list_for_metavariable : 'a option list -> Cic.term option list -- 2.39.2