From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 7 May 2007 11:38:56 +0000 (+0000)
Subject: a bit of sharing and the optimization of not folding trough the metasenv if the to_be... 
X-Git-Tag: 0.4.95@7852~486
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e790aae7c451b81b629f61b15335d7cfe629e845;p=helm.git

a bit of sharing and the optimization of not folding trough the metasenv if the to_be_restrincted list is empty
---

diff --git a/components/cic_unification/cicMetaSubst.ml b/components/cic_unification/cicMetaSubst.ml
index a361b7a32..3767ac10b 100644
--- a/components/cic_unification/cicMetaSubst.ml
+++ b/components/cic_unification/cicMetaSubst.ml
@@ -480,6 +480,7 @@ 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
   let names_of_context_indexes context indexes =
     String.concat ", "
       (List.map
@@ -637,9 +638,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 +784,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