Slightly more efficient patch.

diff --git a/helm/software/components/cic_unification/cicMetaSubst.ml b/helm/software/components/cic_unification/cicMetaSubst.ml
index 3767ac10bc728df500fddd5ab0e83db01519c14c..f082fc23092d6aa1074e54426dbb4ad2994ac170 100644 (file)
--- 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*)