X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicSubstitution.ml;fp=helm%2Focaml%2Fcic_proof_checking%2FcicSubstitution.ml;h=704a8325ad806803c99f3990726e772fd794b4c5;hb=9ea87248101d774e1b4c4b706d8d99444b2e5907;hp=4a938acb9c209be1cbbab3e338f35c6bbf19538e;hpb=98c54cc2f059805350f56811eff8a41934a41460;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index 4a938acb9..704a8325a 100644
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
@@ -335,13 +335,15 @@ if List.mem uri params then prerr_endline "---- OK2" ;
   substaux 1
 ;;
 
-(* l is the relocation list *)
+(* lift_meta [t_1 ; ... ; t_n] t                                *)
+(* returns the term [t] where [Rel i] is substituted with [t_i] *)
+(* [t_i] is lifted as usual when it crosses an abstraction      *)
 let lift_meta l t = 
-    let module C = Cic in
-    if l = [] then t else 
-    let rec aux k = function
+ let module C = Cic in
+  if l = [] then t else 
+   let rec aux k = function
       C.Rel n as t -> 
-	if n <= k then t else 
+        if n <= k then t else 
          (try
            match List.nth l (n-k-1) with
               None -> raise RelToHiddenHypothesis