From 49b788e968f88f6dcf20590d8bdb0788be87c4a4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 7 May 2007 11:38:56 +0000 Subject: [PATCH] a bit of sharing and the optimization of not folding trough the metasenv if the to_be_restrincted list is empty --- helm/software/components/cic_unification/cicMetaSubst.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/helm/software/components/cic_unification/cicMetaSubst.ml b/helm/software/components/cic_unification/cicMetaSubst.ml index a361b7a32..3767ac10b 100644 --- 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 -- 2.39.2