From 76735c56a213efa570fd98336aac2524ff4d36e5 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 22 May 2007 14:39:12 +0000
Subject: [PATCH] Slightly more efficient patch.

---
 .../cic_unification/cicMetaSubst.ml           | 22 +++++++++++++------
 1 file changed, 15 insertions(+), 7 deletions(-)

diff --git a/helm/software/components/cic_unification/cicMetaSubst.ml b/helm/software/components/cic_unification/cicMetaSubst.ml
index 3767ac10b..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,7 +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 =
-        if to_be_restricted = [] then (metasenv,subst) else
+ match to_be_restricted with
+ | [] -> metasenv, subst
+ | _ ->
   let names_of_context_indexes context indexes =
     String.concat ", "
       (List.map
@@ -609,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*)
-- 
2.39.2