Coq：导入关于实例的信息

Question

Section Definitions. 

    Definition eq_dec X := forall x y : X, {x=y} + {x <> y}. 
    Existing Class eq_dec. 

    (* Any function that uses eq_dec. Doesn't matter -- ↓ ↓ ↓ *) 
    Definition f {X: Type} {DecX: eq_dec X} (x y: X) := x = y. 

End Definitions. 

Section MySection. 

    Context {T: Type}. 
    Hypothesis TEqDec: eq_dec T. 

    Inductive myType := 
    | C: T -> myType. 

    Instance myTypeEqDec : eq_dec myType. 
    Proof. ... Defined. 

    (* Everything is ok *) 
    Example example1: forall (t1 t2: myType), f t1 t2. 
    Proof. ... Qed. 

End MySection. 

Section AnotherSection. 

    Context {T: Type}. 
    Hypothesis TEqDec: eq_dec T. 

    (*   Now I must explicitly specify this -- ↓ ↓ ↓ ↓ ↓ ↓ ↓ ↓ ↓ ↓ ↓ ↓ 
    Example example2: forall (t1 t2: @myType T), @f _ (@myTypeEqDec _ TEqDec) t1 t2. 
    Proof. ... Qed. 

End AnotherSection. 

正如您在example1中看到的，Coq能够找到关于myType的实例信息。但是在我改变这个部分之后，关于实例的所有信息都消失了，我必须明确地指定它。所以，当我有很多类型和实例时，代码很快就会变得混乱。很显然，我应该以某种方式将这些信息回复到上下文中。这样做的正确方法是什么？

Answer 1

的Global修改只需添加到您的实例声明，就像这样：

Global Instance myTypeEqDec : eq_dec myType. 
(* ... *) 

正如reference manual指出，

人们可以使用Global修改器的部分，从而宣告实例它们的泛化在该部分关闭后自动重新声明。