fix compatibility with Coq 8.9

coq-community · Oct 4, 2019 · f74852f · f74852f
1 parent 8f13f3b
commit f74852f
Show file tree

Hide file tree

Showing 3 changed files with 1 addition and 3 deletions.
diff --git a/_CoqProject b/_CoqProject
@@ -3,7 +3,7 @@
 -Q coq/Algorithms Chapar
 -Q coq/Examples Chapar
 
--arg -w -arg extraction-axiom-to-realize
+-arg -w -arg -extraction-axiom-to-realize
 
 coq/Lib/extralib.v
 coq/Lib/Predefs.v

diff --git a/coq/Examples/Clients.v b/coq/Examples/Clients.v
@@ -33,7 +33,6 @@ Module Clients (AlgDef: AlgDef) (Parametric: Parametric AlgDef) (CauseObl: Cause
   End AECarrier.
 
   Module Import RAS:= ReflAbsSem SyntaxArg AECarrier.
-  Declare Scope Prog.
   Delimit Scope Prog with Prog.
   Bind Scope Prog with Prog.
   Bind Scope Prog with PProg.

diff --git a/coq/Examples/ListClient.v b/coq/Examples/ListClient.v
@@ -25,7 +25,6 @@ Module ListClient (AlgDef: AlgDef) (Parametric: Parametric AlgDef) (CauseObl: Ca
   End AECarrier.
 
   Module Import RAS:= ReflAbsSem SyntaxArg AECarrier.
-  Declare Scope Prog.
   Delimit Scope Prog with Prog.
   Bind Scope Prog with Prog.
   Bind Scope Prog with PProg.