X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationFwd.ml;h=3ef1ff7e0deada79265cf44c8d6628b231facd5b;hb=2ecd65dbcc1388bb2dfe6425e6ef1b2e3f45c4ac;hp=1c83c2c459c0e410ee8fb9669a2927a731fbe26a;hpb=1ca0ec89cfc2c3f85af95d5b1bdad07597d976bd;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationFwd.ml b/helm/ocaml/cic_notation/cicNotationFwd.ml
index 1c83c2c45..3ef1ff7e0 100644
--- a/helm/ocaml/cic_notation/cicNotationFwd.ml
+++ b/helm/ocaml/cic_notation/cicNotationFwd.ml
@@ -28,74 +28,6 @@ open Printf
 module Ast = CicNotationPt
 module Env = CicNotationEnv
 
-(* XXX ZACK: switched to CicNotationUtil.names_of_term, commented code below to
- * be removes as soon as we believe implementation are equivalent *)
-(* let meta_names_of term =
-  let rec names = ref [] in
-  let add_name n =
-    if List.mem n !names then ()
-    else names := n :: !names
-  in
-  let rec aux = function
-    | AttributedTerm (_, term) -> aux term
-    | Appl terms -> List.iter aux terms
-    | Binder (_, _, body) -> aux body
-    | Case (term, indty, outty_opt, patterns) ->
-        aux term ;
-        aux_opt outty_opt ;
-        List.iter aux_branch patterns
-    | LetIn (_, t1, t2) ->
-        aux t1 ;
-        aux t2
-    | LetRec (_, definitions, body) ->
-        List.iter aux_definition definitions ;
-        aux body
-    | Uri (_, Some substs) -> aux_substs substs
-    | Ident (_, Some substs) -> aux_substs substs
-    | Meta (_, substs) -> aux_meta_substs substs
-
-    | Implicit
-    | Ident _
-    | Num _
-    | Sort _
-    | Symbol _
-    | Uri _
-    | UserInput -> ()
-
-    | Magic magic -> aux_magic magic
-    | Variable var -> aux_variable var
-
-    | _ -> assert false
-  and aux_opt = function
-    | Some term -> aux term
-    | None -> ()
-  and aux_capture_var (_, ty_opt) = aux_opt ty_opt
-  and aux_branch (pattern, term) =
-    aux_pattern pattern ;
-    aux term
-  and aux_pattern (head, vars) = 
-    List.iter aux_capture_var vars
-  and aux_definition (var, term, i) =
-    aux_capture_var var ;
-    aux term
-  and aux_substs substs = List.iter (fun (_, term) -> aux term) substs
-  and aux_meta_substs meta_substs = List.iter aux_opt meta_substs
-  and aux_variable = function
-    | NumVar name -> add_name name
-    | IdentVar name -> add_name name
-    | TermVar name -> add_name name
-    | FreshVar _ -> ()
-    | Ascription _ -> assert false
-  and aux_magic = function
-    | Default (t1, t2)
-    | Fold (_, t1, _, t2) ->
-        aux t1 ;
-        aux t2
-    | _ -> assert false
-  in
-  aux term ;
-  !names *)
-
 let unopt_names names env =
   let rec aux acc = function
     | (name, (ty, v)) :: tl when List.mem name names ->
@@ -182,8 +114,8 @@ let instantiate_level2 env term =
   and aux_capture_var env (name, ty_opt) = (aux env name, aux_opt env ty_opt)
   and aux_branch env (pattern, term) =
     (aux_pattern env pattern, aux env term)
-  and aux_pattern env (head, vars) =
-    (head, List.map (aux_capture_var env) vars)
+  and aux_pattern env (head, hrefs, vars) =
+    (head, hrefs, List.map (aux_capture_var env) vars)
   and aux_definition env (var, term, i) =
     (aux_capture_var env var, aux env term, i)
   and aux_substs env substs =