Merge pull request #139 from coq-community/coq_20028

ppedrot · web-flow · commit 74ced1b11a8d · 2025-01-13T08:21:48.000+01:00
Adapt to rocq-prover/rocq#20028
diff --git a/Makefile.in b/Makefile.in
@@ -222,7 +222,7 @@ $(TESTDIR)/PrimitiveProjections.dpd $(TESTDIR)/PrimitiveProjections2.dpd: \
 
 $(TESTDIR)/search.log : $(TESTDIR)/Test.vo $(TESTDIR)/search.cmd $(DPDPLUGIN)
 	cat $(TESTDIR)/search.cmd | coqtop -R . dpdgraph -I . 2> /dev/null \
-	  | sed -e 's/Welcome to Coq.*/Welcome to Coq/' > $@
+	  | sed -e 's/Welcome to Rocq.*/Welcome to Rocq/' > $@
 
 %.dot : %.dpd  $(DPD2DOT)
 	$(DPD2DOT) $< > /dev/null
diff --git a/tests/search.oracle b/tests/search.oracle
@@ -1,4 +1,4 @@
-Welcome to Coq
+Welcome to Rocq
 [Loading ML file coq-dpdgraph.plugin ... done]
 [Loading ML file rocq-runtime.plugins.ring ... done]
 Fetching opaque proofs from disk for dpdgraph.tests.Test

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-Welcome to Coq`
	`1`	`+Welcome to Rocq`
`2`	`2`	`[Loading ML file coq-dpdgraph.plugin ... done]`
`3`	`3`	`[Loading ML file rocq-runtime.plugins.ring ... done]`
`4`	`4`	`Fetching opaque proofs from disk for dpdgraph.tests.Test`