* Reindentation

* More comments

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

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.mli b/helm/ocaml/cic_proof_checking/cicSubstitution.mli
index 038b5de3f63c12d364640d9a51728c1a88968b96..2032869911d35fa6154298b7c1bb10d1fa77dff0 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.mli
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.mli
@@ -42,5 +42,7 @@ val subst : Cic.term -> Cic.term -> Cic.term
 val subst_vars :
  Cic.term Cic.explicit_named_substitution -> Cic.term -> Cic.term
 
-(* ?????????? *)
+(* 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      *)
 val lift_meta : (Cic.term option) list -> Cic.term -> Cic.term