-
François Clément authoredsub_nodeF_alt -> sub_nodeF. Rm useless sub_node_ref_eq, T_geom_sub_nodeF. The proof of sub_node_out_Hface_0 is now based on sub_node_ref_out_Hface_ref_0.
aeca3cd6
LagP_node.v 7.30 KiB
sub_nodeF_alt -> sub_nodeF. Rm useless sub_node_ref_eq, T_geom_sub_nodeF. The proof of sub_node_out_Hface_0 is now based on sub_node_ref_out_Hface_ref_0.