From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 17 Dec 2003 10:47:40 +0000 (+0000)
Subject: * Reindentation
X-Git-Tag: V_0_5_1_3~62
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9ea87248101d774e1b4c4b706d8d99444b2e5907;p=helm.git

* Reindentation
* More comments
---

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
diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.mli b/helm/ocaml/cic_proof_checking/cicSubstitution.mli
index 038b5de3f..203286991 100644
--- 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