Rocq/Stdlib rename

Author: nchappe

Readme.md

@@ -13,7 +13,7 @@ We develop a cousin of Interaction Trees, dubbed _ctrees_ with native support fo
   - Yannick Zakowski
   - Steve Zdancewic
 - License: MIT License
-- Compatible Coq versions: 8.19
+- Compatible Rocq versions: 9.0
 - Additional dependencies:
   - dune
   - [Extlib](https://github.com/coq-community/coq-ext-lib)
@@ -22,7 +22,7 @@ We develop a cousin of Interaction Trees, dubbed _ctrees_ with native support fo
   - [Coinduction](https://github.com/damien-pous/coinduction)
   - [RelationAlgebra](https://github.com/damien-pous/relation-algebra)
   - [Alectryon](https://github.com/cpitclaudel/alectryon)
-- Coq namespace: `CTree`
+- Rocq namespace: `CTree`
 
 ## Building instructions
 

examples/CCS/Denotation.v

@@ -7,10 +7,10 @@ Denotation of [ccs] into [ctree]s
 |*)
 Unset Universe Checking.
 
-From Coq Require Export
+From Stdlib Require Export
      List
      Strings.String.
-From Coq Require Import RelationClasses Program.
+From Stdlib Require Import RelationClasses Program.
 
 From RelationAlgebra Require Import
      monoid
@@ -117,7 +117,7 @@ Section Combinators.
 
 (*|
 We would like to define [bang] directly as in the following.
-Unfortunately, it is not syntactically guarded and convincing Coq
+Unfortunately, it is not syntactically guarded and convincing Rocq
 seems challenging.
 We therefore instead define a more general function [parabang] expressing
 at once the parallel composition of a process [p] with a server of [q].

examples/CCS/Syntax.v

@@ -8,7 +8,7 @@ No recursion nor replication at the moment, todo.
 .. coq:: none
 |*)
 
-From Coq Require Export
+From Stdlib Require Export
   List
   Strings.String.
 

examples/ImpBr/ImpBr.v

@@ -1,6 +1,6 @@
 Unset Universe Checking.
 
-From Coq Require Import
+From Stdlib Require Import
      Arith.PeanoNat
      Lists.List
      Strings.String

examples/Yield/Lang.v

@@ -1,4 +1,4 @@
-From Coq Require Import
+From Stdlib Require Import
      Arith.PeanoNat
      Lists.List
      Strings.String

examples/Yield/Par.v

@@ -1,4 +1,4 @@
-From Coq Require Import
+From Stdlib Require Import
      Program
      List
      Logic.FunctionalExtensionality

examples/Yield/Util.v

@@ -1,4 +1,4 @@
-From Coq Require Import
+From Stdlib Require Import
      Program
      List
      Logic.FunctionalExtensionality

tests/ImpBrTest/ImpBrEx/ImpBrEx.v

@@ -1,6 +1,6 @@
 Unset Universe Checking.
 
-From Coq Require Import
+From Stdlib Require Import
      Strings.String.
 From ExtLib Require Import
      Data.Map.FMapAList.

theories/Core/Utils.v

@@ -1,7 +1,7 @@
 #[global] Set Warnings "-intuition-auto-with-star".
 
-From Coq Require Import Fin.
-From Coq Require Export Program.Equality.
+From Stdlib Require Import Fin.
+From Stdlib Require Export Program.Equality.
 From Coinduction Require Import all.
 From ITree Require Import Basics.Basics.
 

theories/Eq.v

@@ -6,7 +6,7 @@ This file reexports everything that's necessary to reason w.r.t.
 Tactics are redefined locally to support both relations.
 |*)
 
-From Coq Require Export Basics.
+From Stdlib Require Export Basics.
 
 From RelationAlgebra Require Export
      rel srel.