Merge pull request #127 from coq-community/stdlib_repo

proux01 · web-flow · commit 992c3a53b49b · 2024-09-17T13:26:56.000+02:00
Adapt to coq/coq#19530
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)`