naming tables: ensures that declarations are transversed bottom-up

src/parser/parser.mly

@@ -1123,6 +1123,5 @@ qualid_comma_list_eof:
 ident_comma_list_eof:
 | comma_list1(ident) EOF { $1 }
 
-(* TODO: Weird to not have any parser conflicts here *)
 term_comma_list_eof:
 | comma_list1(term) EOF { $1 }

src/transform/args_wrapper.ml

@@ -161,8 +161,9 @@ let build_naming_tables task : naming_table =
     This only works for things defined in .why/.mlw because things
     added by the user are renamed on the fly. *)
   (* TODO:imported theories should be added in the namespace too *)
-  let l = Mid.fold (fun _id d acc -> d :: acc) km [] in
-  List.fold_left (fun tables d -> add d tables) tables l
+  Task.task_fold
+    (fun t d ->
+     match d.td_node with Decl d -> add d t | _ -> t) tables task
 
 (************* wrapper  *************)