]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_unification/cicMkImplicit.mli
Added an optional parameter to identity_relocation_list. The parameter
[helm.git] / helm / ocaml / cic_unification / cicMkImplicit.mli
index a698386b5656bf5b17be8206ce913a34f368fc79..6d9179d8e0e3c23e453c50e5d0856ba2b81c01e3 100644 (file)
@@ -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.                       *)