Code simplified.

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index b69984f3d5c2c15a0e6d761529c2cd69fe935c04..f63aa9a30759d4a36acae98f99f892738e444dfd 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -105,41 +105,36 @@ let rec force_does_not_occur metasenv subst restrictions t =
         in
         if amount > 0 then ms, NCic.Rel (r - amount) else ms, orig
     | NCic.Meta (n, (shift,lc as l)) as orig ->
-       let meta_chain =
-        try
-         Some (NCicUtils.lookup_subst n subst)
+       (try
+         let _,_,bo,_ = NCicUtils.lookup_subst n subst in
+          aux k ms (NCicSubstitution.subst_meta l bo)
         with
-         NCicUtils.Subst_not_found _ -> None
-       in
-        (match meta_chain with
-            Some (_,_,bo,_) ->
-             aux k ms (NCicSubstitution.subst_meta l bo)
-          | None ->
-             (* we ignore the subst since restrict will take care of already
-              * instantiated/restricted metavariabels *)
-             let (metasenv,subst as ms), restrictions_for_n, l' =
-               let l = NCicUtils.expand_local_context lc in
+         NCicUtils.Subst_not_found _ ->
+          (* we ignore the subst since restrict will take care of already
+           * instantiated/restricted metavariabels *)
+          let (metasenv,subst as ms), restrictions_for_n, l' =
+            let l = NCicUtils.expand_local_context lc in
          
-               let ms, _, restrictions_for_n, l =
-                List.fold_right
-                  (fun t (ms, i, restrictions_for_n, l) ->
-                    try 
-                      let ms, t = aux (k-shift) ms t in
-                      ms, i-1, restrictions_for_n, t::l
-                    with Occur ->
-                      ms, i-1, i::restrictions_for_n, l)
-                  l (ms, List.length l, [], [])
-               in
-                   
-                ms, restrictions_for_n, pack_lc (shift, NCic.Ctx l)
-             in
-             if restrictions_for_n = [] then
-               ms, if l = l' then orig else NCic.Meta (n, l')
-             else
-               let metasenv, subst, newmeta = 
-                 restrict metasenv subst n restrictions_for_n 
-               in
-                 (metasenv, subst), NCic.Meta (newmeta, l'))
+            let ms, _, restrictions_for_n, l =
+             List.fold_right
+               (fun t (ms, i, restrictions_for_n, l) ->
+                 try 
+                   let ms, t = aux (k-shift) ms t in
+                   ms, i-1, restrictions_for_n, t::l
+                 with Occur ->
+                   ms, i-1, i::restrictions_for_n, l)
+               l (ms, List.length l, [], [])
+            in
+                
+             ms, restrictions_for_n, pack_lc (shift, NCic.Ctx l)
+          in
+          if restrictions_for_n = [] then
+            ms, if l = l' then orig else NCic.Meta (n, l')
+          else
+            let metasenv, subst, newmeta = 
+              restrict metasenv subst n restrictions_for_n 
+            in
+              (metasenv, subst), NCic.Meta (newmeta, l'))
     | t -> NCicUntrusted.map_term_fold_a (fun _ k -> k+1) k aux ms t
  in
    aux 0 (metasenv,subst) t