adapt to rocq-9.0

Author: kyoDralliam

Makefile

@@ -1,4 +1,4 @@
-.PHONY: all clean 
+.PHONY: all clean
 COQMAKEFILE := Makefile.coq
 ifneq "$(COQBIN)" ""
   COQBIN := $(COQBIN)/
@@ -12,7 +12,7 @@ clean:
 	rm -f $(COQMAKEFILE)
 
 $(COQMAKEFILE): Makefile _CoqProject
-	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
+	$(COQBIN)rocq makefile -f _CoqProject -o Makefile.coq
 
 %:
 	-$(MAKE) -f $(COQMAKEFILE) $@

src/META.smpl

@@ -2,7 +2,7 @@ package "smpl" (
     directory = "."
     version = "dev"
     description = "smpl plugin"
-    requires = "coq-core.plugins.ltac"
+    requires = "rocq-runtime.plugins.ltac"
     archive(byte) = "smpl_plugin.cma"
     archive(native) = "smpl_plugin.cmxa"
     plugin(byte) = "smpl_plugin.cma"

src/smpl.mlg

@@ -17,7 +17,7 @@ open Extraargs
 open Pp
 open Tacarg
 open Ltac_plugin
-open Pcoq.Prim
+open Procq.Prim
 open Taccoerce
 
 module StringMap = Map.Make(String)
@@ -126,7 +126,7 @@ let smpl_create db_name db =
 let pr_progress b =
   str "(" ++ (if b then str "" else str "no") ++ str "progress)"
 
-let fresh_env () = 
+let fresh_env () =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   env, sigma
@@ -143,7 +143,7 @@ let smpl_print_entry e =
 
 let smpl_db_exists db_name =
   try let db = StringMap.find db_name (!smpl_dbs) in db
-  with Not_found -> CErrors.user_err 
+  with Not_found -> CErrors.user_err
 				     (str "Unknown Smpl Database " ++ str db_name ++ str ".")
 
 let smpl_print db_name =
@@ -152,7 +152,7 @@ let smpl_print db_name =
 				   str " "  ++ pr_progress db.progress_default ++ str ".") in
       let _ = Feedback.msg_info (str "Tactics in priority order:") in
       List.iter (smpl_print_entry) db.queue; ()
-  with Not_found -> CErrors.user_err 
+  with Not_found -> CErrors.user_err
 				     (str "Unknown Smpl Database " ++ str db_name ++ str ".")
 
 let smpl_print_dbs () =
@@ -222,7 +222,7 @@ let pr_smpldb _prc _prlc _prt s = str s
 }
 
 ARGUMENT EXTEND smpldb
-  TYPED AS preident 
+  TYPED AS preident
   PRINTED BY { pr_smpldb }
 | [ preident(i) ] -> { let _ = smpl_db_exists i in i }
 END

theories/Demo.v

@@ -19,12 +19,12 @@ Goal False.
   Fail smpl len.
 Abort.
 
-Require Import List.
+From Stdlib Require Import List.
 
 Ltac len_simpl_app :=
   match goal with
-  | [ |- context [ length (?L ++ ?L') ] ] => rewrite (@app_length _ L L')
-  | [ H : context [ length (?L ++ ?L') ] |- _ ] => rewrite (@app_length _ L L') in H
+  | [ |- context [ length (?L ++ ?L') ] ] => rewrite (@length_app _ L L')
+  | [ H : context [ length (?L ++ ?L') ] |- _ ] => rewrite (@length_app _ L L') in H
   end.
 
 (* This adds the tactic at priority 100. *)
@@ -37,8 +37,8 @@ Notation "f ⊝ L" := (List.map f L) (at level 50, L at level 50, left associati
 
 Ltac len_simpl_map :=
   match goal with
-  | [ |- context [ length (?f ⊝ ?L) ] ] => rewrite (@map_length _ _ f L)
-  | [ H : context [ length (?f ⊝ ?L) ] |- _ ] => rewrite (@map_length _ _ f L) in H
+  | [ |- context [ length (?f ⊝ ?L) ] ] => rewrite (@length_map _ _ f L)
+  | [ H : context [ length (?f ⊝ ?L) ] |- _ ] => rewrite (@length_map _ _ f L) in H
   end.
 
 Smpl Add 99 len_simpl_map : len.

theories/Smpl.v

@@ -1 +1 @@
-Declare ML Module "smpl_plugin:smpl.smpl".
+Declare ML Module "smpl.smpl".