-open CicNotationPt
-
-(* 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 *)