Remove Equations<question mark> command

Beluga-lang · Jun 8, 2024 · fbac860 · fbac860
1 parent 07f490f
commit fbac860
Showing 1 changed file with 2 additions and 4 deletions.
diff --git a/theories/Extraction/TypeCheck.v b/theories/Extraction/TypeCheck.v
@@ -54,17 +54,15 @@ Section conversion_dec.
     end.
 
   #[tactic="impl_obl_tac"]
-  Equations? conversion_dec G A M (HM : {{ G ⊢ M : A }}) M' (HM' : {{ G ⊢ M' : A }}) : { {{ G ⊢ M ≈ M' : A }} } + { ~ {{ G ⊢ M ≈ M' : A }} } :=
+  Equations conversion_dec G A M (HM : {{ G ⊢ M : A }}) M' (HM' : {{ G ⊢ M' : A }}) : { {{ G ⊢ M ≈ M' : A }} } + { ~ {{ G ⊢ M ≈ M' : A }} } :=
   | G, A, M, HM, M', HM' =>
       let (W, HW) := nbe_impl G M A _ in
       let (W', HW') := nbe_impl G M' A _ in
       match nf_eq_dec W W' with
       | left _ => left _
       | right _ => right _
       end.
-  Proof.
-    intro. impl_obl_tac.
-  Qed.
+  Next Obligation. impl_obl_tac. Qed.
 End conversion_dec.
 
 Section typ_subsumption_dec.