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修改器的部分，從而宣告實例它們的泛化在該部分關閉後自動重新聲明。