Added an optional parameter to identity_relocation_list. The parameter

[helm.git] / helm / ocaml / cic_unification / cicMkImplicit.ml

diff --git a/helm/ocaml/cic_unification/cicMkImplicit.ml b/helm/ocaml/cic_unification/cicMkImplicit.ml
index 6944a4fc210dfe1a68d016dcf513e5f4d9a86d09..2da0b5a19001db9c0f55288bf4b9c8a63f4fc650 100644 (file)
--- 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.                       *)