Adapt to coq/coq#19530

proux01 · proux01 · commit c048b4262f5b · 2024-09-16T17:27:42.000+02:00
diff --git a/test-suite/exmNotParametric.v b/test-suite/exmNotParametric.v
@@ -1,4 +1,4 @@
-Require Import Coq.Logic.ClassicalFacts.
+From Coq Require Import ClassicalFacts.
 Inductive False_R : False -> False -> Prop :=.
 
 Inductive or_R (A₁ A₂ : Prop) (A_R : A₁ -> A₂ -> Prop) (B₁ B₂ : Prop)

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-Require Import Coq.Logic.ClassicalFacts.`
	`1`	`+From Coq Require Import ClassicalFacts.`
`2`	`2`	`Inductive False_R : False -> False -> Prop :=.`
`3`	`3`
`4`	`4`	`Inductive or_R (A₁ A₂ : Prop) (A_R : A₁ -> A₂ -> Prop) (B₁ B₂ : Prop)`