a bit of sharing and the optimization of not folding trough the metasenv if the to_be...

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