* Reindentation.

* Useless code elimination.
* Debug code elimination.

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 306074ec983daf7b0adda12e594efb0bb5f7222a..ad1b47206b14aa16e4212e0cb7338ba9c326758d 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -220,8 +220,6 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
        raise UnificationFailed
    | (C.Rel _, _)
    | (_,  C.Rel _) 
-   | (C.Var _, _)
-   | (_, C.Var _) 
    | (C.Sort _ ,_)
    | (_, C.Sort _)
    | (C.Implicit, _)
@@ -309,114 +307,6 @@ prerr_endline ("@@@: " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst1)) ^
 " <==> " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst2))) ; raise e
 ;;
 
-(*CSC: ???????????????
-(* m is the index of a metavariable to restrict, k is nesting depth
-of the occurrence m, and l is its relocation list. canonical_context
-is the context of the metavariable we are instantiating - containing
-m - Only rel in the domain of canonical_context are accessible.
-This function takes in input a metasenv and gives back a metasenv.
-A rel(j) in the canonical context of m, is rel(List.nth l j) for the 
-instance of m under consideration, that is rel (List.nth l j) - k 
-in canonical_context. *)
-
-let restrict canonical_context m k l =
-  let rec erase i = 
-    function
-        [] -> []
-      |        None::tl -> None::(erase (i+1) tl)
-      |        he::tl -> 
-          let i' = (List.nth l (i-1)) in
-          if i' <= k 
-           then he::(erase (i+1) tl) (* local variable *) 
-           else 
-            let acc = 
-              (try List.nth canonical_context (i'-k-1)
-               with Failure _ -> None) in
-            if acc = None 
-             then None::(erase (i+1) tl)
-             else he::(erase (i+1) tl) in
-  let rec aux =
-    function 
-        [] -> []
-      |        (n,context,t)::tl when n=m -> (n,erase 1 context,t)::tl
-      |        hd::tl -> hd::(aux tl)
-  in
-   aux
-;;
-
-
-let check_accessibility metasenv i =
-  let module C = Cic in
-  let module S = CicSubstitution in
-  let (_,canonical_context,_) = 
-    List.find (function (m,_,_) -> m=i) metasenv in
-   List.map
-    (function t ->
-      let =
-       delift canonical_context metasenv ? t
-    ) canonical_context
-CSCSCS
-
-
-
-  let rec aux metasenv k =
-    function
-      C.Rel i -> 
-       if i <= k then
-        metasenv
-       else 
-        (try
-          match List.nth canonical_context (i-k-1) with
-            Some (_,C.Decl t) 
-          | Some (_,C.Def t) -> aux metasenv k (S.lift i t)
-          | None -> raise RelToHiddenHypothesis
-          with
-           Failure _ -> raise OpenTerm
-        )
-    | C.Var _  -> metasenv
-    | C.Meta (i,l) -> restrict canonical_context i k l metasenv 
-    | C.Sort _ -> metasenv
-    | C.Implicit -> metasenv
-    | C.Cast (te,ty) -> 
-        let metasenv' = aux metasenv k te in
-        aux metasenv' k ty
-    | C.Prod (_,s,t) 
-    | C.Lambda (_,s,t) 
-    | C.LetIn (_,s,t) ->
-        let metasenv' = aux metasenv k s in
-        aux metasenv' (k+1) t
-    | C.Appl l ->
-        List.fold_left
-          (function metasenv -> aux metasenv k) metasenv l
-    | C.Const _
-    | C.MutInd _ 
-    | C.MutConstruct _ -> metasenv
-    | C.MutCase (_,_,_,outty,t,pl) ->
-        let metasenv' = aux metasenv k outty in
-        let metasenv'' = aux metasenv' k t in
-        List.fold_left
-          (function metasenv -> aux metasenv k) metasenv'' pl
-    | C.Fix (i, fl) ->
-       let len = List.length fl in
-       List.fold_left
-         (fun metasenv f ->
-           let (_,_,ty,bo) = f in
-           let metasenv' = aux metasenv k ty in
-           aux metasenv' (k+len) bo
-         ) metasenv fl
-    | C.CoFix (i, fl) ->
-        let len = List.length fl in
-        List.fold_left
-         (fun metasenv f ->
-           let (_,ty,bo) = f in
-           let metasenv' = aux metasenv k ty in
-           aux metasenv' (k+len) bo
-         ) metasenv fl
-  in aux metasenv 0
-;;
-*)
-
-
 let unwind metasenv subst unwinded t =
  let unwinded = ref unwinded in
  let frozen = ref [] in
@@ -693,11 +583,6 @@ let apply_subst subst t =
 (* a new metasenv in which some hypothesis in the contexts of the            *)
 (* metavariables may have been restricted.                                   *)
 let fo_unif metasenv context t1 t2 =
-prerr_endline "INIZIO FASE 1" ; flush stderr ;
  let subst_to_unwind,metasenv' = fo_unif_subst [] context metasenv t1 t2 in
-prerr_endline "FINE FASE 1" ; flush stderr ;
-let res =
   unwind_subst metasenv' subst_to_unwind
-in
-prerr_endline "FINE FASE 2" ; flush stderr ; res
 ;;