X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicSubstitution.ml;h=2abce6a0edc635fbfffc3df5bd40c4bf990fc78d;hb=8aaf525856e25bcd8f355e505fd00f45c62bc18f;hp=431fa4b50d1303c6b64a3a90462fea9f3fd8d90f;hpb=e8236af508187f6446f5af481d545d433628ee00;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index 431fa4b50..2abce6a0e 100644
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
@@ -30,6 +30,8 @@ exception ReferenceToConstant;;
 exception ReferenceToCurrentProof;;
 exception ReferenceToInductiveDefinition;;
 
+let debug_print = fun _ -> ()
+
 let lift_from k n =
  let rec liftaux k =
   let module C = Cic in
@@ -189,7 +191,7 @@ let subst arg =
 (*CSC: per la roba che proviene da Coq questo non serve!                 *)
 let subst_vars exp_named_subst =
 (*
-prerr_endline ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS") ;
+debug_print ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS") ;
 *)
  let rec substaux k =
   let module C = Cic in
@@ -214,17 +216,17 @@ prerr_endline ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS") ;
            )
           in
 (*
-prerr_endline "\n\n---- BEGIN " ;
-prerr_endline ("----params: " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
-prerr_endline ("----S(" ^ UriManager.string_of_uri uri ^ "): " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst)) ;
-prerr_endline ("----P: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst')) ;
+debug_print "\n\n---- BEGIN " ;
+debug_print ("----params: " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
+debug_print ("----S(" ^ UriManager.string_of_uri uri ^ "): " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst)) ;
+debug_print ("----P: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst')) ;
 *)
            let exp_named_subst'' =
             substaux_in_exp_named_subst uri k exp_named_subst' params
            in
 (*
-prerr_endline ("----D: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst'')) ;
-prerr_endline "---- END\n\n " ;
+debug_print ("----D: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst'')) ;
+debug_print "---- END\n\n " ;
 *)
             C.Var (uri,exp_named_subst'')
        )
@@ -329,10 +331,11 @@ prerr_endline "---- END\n\n " ;
     | _::tl -> filter_and_lift tl
 (*
     | (uri,_)::tl ->
-prerr_endline ("---- SKIPPO " ^ UriManager.string_of_uri uri) ;
-if List.for_all (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst' then prerr_endline "---- OK1" ;
-prerr_endline ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
-if List.mem uri params then prerr_endline "---- OK2" ;
+debug_print ("---- SKIPPO " ^ UriManager.string_of_uri uri) ;
+if List.for_all (function (uri',_) -> not (UriManager.eq uri uri'))
+exp_named_subst' then debug_print "---- OK1" ;
+debug_print ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
+if List.mem uri params then debug_print "---- OK2" ;
         filter_and_lift tl
 *)
   in
@@ -342,10 +345,10 @@ if List.mem uri params then prerr_endline "---- OK2" ;
   substaux 1
 ;;
 
-(* lift_meta [t_1 ; ... ; t_n] t                                *)
+(* subst_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 subst_meta l t = 
  let module C = Cic in
   if l = [] then t else 
    let rec aux k = function
@@ -419,3 +422,4 @@ let lift_meta l t =
  in
   aux 0 t          
 ;;
+