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 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.                       *)

diff --git a/helm/ocaml/cic_unification/cicMkImplicit.mli b/helm/ocaml/cic_unification/cicMkImplicit.mli
index a698386b5656bf5b17be8206ce913a34f368fc79..6d9179d8e0e3c23e453c50e5d0856ba2b81c01e3 100644 (file)
--- 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.                       *)