Fix Open/Close scope

Use Open/Close Scope without Local (i.e., export the scope opening) only when the scope corresponds to the main purpose of the module.

theories/countable.v

@@ -269,7 +269,7 @@ Next Obligation.
 Qed.
 
 (** ** Generic trees *)
-Close Scope positive.
+Local Close Scope positive.
 
 Inductive gen_tree (T : Type) : Type :=
   | GenLeaf : T → gen_tree T