* Reindentation

[helm.git] / helm / ocaml / cic_proof_checking / cicSubstitution.ml

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index 4a938acb9c209be1cbbab3e338f35c6bbf19538e..704a8325ad806803c99f3990726e772fd794b4c5 100644 (file)
--- 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