X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicMetaSubst.ml;h=f082fc23092d6aa1074e54426dbb4ad2994ac170;hb=99727f61d0a718e34d4282f9b9b45fce4336af84;hp=a361b7a32bc3a9ee6fe1c8a1bc24fd4c6095a81b;hpb=65c0b57c0b8566b4cb256ec2533554b9c5105b8c;p=helm.git

diff --git a/helm/software/components/cic_unification/cicMetaSubst.ml b/helm/software/components/cic_unification/cicMetaSubst.ml
index a361b7a32..f082fc230 100644
--- a/helm/software/components/cic_unification/cicMetaSubst.ml
+++ b/helm/software/components/cic_unification/cicMetaSubst.ml
@@ -247,9 +247,11 @@ let apply_subst =
        | _ -> t'
      end
   in
-  fun s t ->
+  fun subst t ->
 (*     incr apply_subst_counter; *)
-    apply_subst_gen ~appl_fun s t
+match subst with
+   [] -> t
+ | _ -> apply_subst_gen ~appl_fun subst t
 ;;
 
 let profiler = HExtlib.profile "U/CicMetaSubst.apply_subst"
@@ -257,7 +259,10 @@ let apply_subst s t =
   profiler.HExtlib.profile (apply_subst s) t
 
 
-let rec apply_subst_context subst context =
+let apply_subst_context subst context =
+ match subst with
+    [] -> context
+  | _ ->
 (*
   incr apply_subst_context_counter;
   context_length := !context_length + List.length context;
@@ -284,6 +289,9 @@ let apply_subst_metasenv subst metasenv =
   incr apply_subst_metasenv_counter;
   metasenv_length := !metasenv_length + List.length metasenv;
 *)
+match subst with
+   [] -> metasenv
+ | _ ->
   List.map
     (fun (n, context, ty) ->
       (n, apply_subst_context subst context, apply_subst subst ty))
@@ -480,6 +488,9 @@ let rec force_does_not_occur subst to_be_restricted t =
  (!more_to_be_restricted, res)
  
 let rec restrict subst to_be_restricted metasenv =
+ match to_be_restricted with
+ | [] -> metasenv, subst
+ | _ ->
   let names_of_context_indexes context indexes =
     String.concat ", "
       (List.map
@@ -608,9 +619,7 @@ let rec restrict subst to_be_restricted metasenv =
           raise (MetaSubstFailure error_msg))) 
       subst ([], []) 
   in
-  match more_to_be_restricted @ more_to_be_restricted' with
-  | [] -> (metasenv, subst)
-  | l -> restrict subst l metasenv
+   restrict subst (more_to_be_restricted @ more_to_be_restricted') metasenv
 ;;
 
 (*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)(*Andrea: maybe not*)
@@ -637,9 +646,9 @@ let delift n subst context metasenv l t =
   let rec deliftaux k =
    let module C = Cic in
     function
-       C.Rel m -> 
+     | C.Rel m as t-> 
          if m <=k then
-          C.Rel m
+          t
          else
            (try
             match List.nth context (m-k-1) with
@@ -783,9 +792,9 @@ let delift_rels_from subst metasenv k n =
  let rec liftaux subst metasenv k =
   let module C = Cic in
    function
-      C.Rel m ->
+      C.Rel m as t ->
        if m < k then
-        C.Rel m, subst, metasenv
+        t, subst, metasenv
        else if m < k + n then
          raise DeliftingARelWouldCaptureAFreeVariable
        else