From: Claudio Sacerdoti Coen Date: Tue, 3 Feb 2004 13:03:49 +0000 (+0000) Subject: Added an optional parameter to identity_relocation_list. The parameter X-Git-Tag: V_0_2_3~100 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=502628b87ff30f2c4955ffaa4da7a6ebc0c4119b;p=helm.git Added an optional parameter to identity_relocation_list. The parameter is the "starting" rel. --- diff --git a/helm/ocaml/cic_unification/cicMkImplicit.ml b/helm/ocaml/cic_unification/cicMkImplicit.ml index 6944a4fc2..2da0b5a19 100644 --- a/helm/ocaml/cic_unification/cicMkImplicit.ml +++ b/helm/ocaml/cic_unification/cicMkImplicit.ml @@ -3,7 +3,7 @@ (* returns the identity relocation list, which is the list [1 ; ... ; n] *) (* where n = List.length [canonical_context] *) (*CSC: ma mi basta la lunghezza del contesto canonico!!!*) -let identity_relocation_list_for_metavariable canonical_context = +let identity_relocation_list_for_metavariable ?(start = 1) canonical_context = let canonical_context_length = List.length canonical_context in let rec aux = function @@ -11,7 +11,7 @@ let identity_relocation_list_for_metavariable canonical_context = | (n,None::tl) -> None::(aux ((n+1),tl)) | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl)) in - aux (1,canonical_context) + aux (start,canonical_context) (* Returns the first meta whose number is above the *) (* number of the higher meta. *) diff --git a/helm/ocaml/cic_unification/cicMkImplicit.mli b/helm/ocaml/cic_unification/cicMkImplicit.mli index a698386b5..6d9179d8e 100644 --- a/helm/ocaml/cic_unification/cicMkImplicit.mli +++ b/helm/ocaml/cic_unification/cicMkImplicit.mli @@ -3,7 +3,7 @@ (* 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 + ?start: int -> 'a option list -> Cic.term option list (* Returns the first meta whose number is above the *) (* number of the higher meta. *)