Rocq9: add Stdlib to theories and fix deprecations

Author: shilangyu

engines/js/dune

@@ -10,7 +10,7 @@
 (coq.extraction
  (prelude Extraction)
  (extracted_modules Extracted)
- (theories Warblre Ltac2))
+ (theories Warblre Ltac2 Stdlib))
 
 ; Make a library out of it
 (library

engines/ocaml/dune

@@ -10,7 +10,7 @@
 (coq.extraction
  (prelude Extraction)
  (extracted_modules Extracted)
- (theories Warblre Ltac2))
+ (theories Warblre Ltac2 Stdlib))
 
 ; Make a library out of it
 (library
@@ -21,4 +21,4 @@
 (env
  (dev
   (flags
-   (:standard -w -27 -w -39 -w -67))))
+   (:standard -w -20 -w -27 -w -39 -w -67))))

mechanization/dune

@@ -3,4 +3,4 @@
 (coq.theory
  (name Warblre)
  (package warblre)
- (theories Ltac2))
+ (theories Ltac2 Stdlib))

mechanization/spec/Inst.v

@@ -528,7 +528,7 @@ Open Scope list_scope.
 Import NaiveEngine.
 (* Import FastEngine. *)
 
-Definition get_success {S F} (r: Result S F) : match r with Success _ => S | Error _ => unit end :=
+Definition get_success {S F: Type} (r: Result S F) : match r with Success _ => S | Error _ => unit end :=
   match r with
   | Success s => s
   | Error f => tt
@@ -548,8 +548,8 @@ Notation "$ c" := (character_of_Ascii c) (at level 0).
 Notation "$$ s" := (string_of_String s) (at level 0).
 
 (* Hide the matching functions in the outputs below*)
-Arguments Exotic {C S UP}%type_scope {H H0 H1} _ {_}.
-Arguments Null {C S UP}%type_scope {H H0 H1} {_}.
+Arguments Exotic {C S UP}%_type_scope {H H0 H1} _ {_}.
+Arguments Null {C S UP}%_type_scope {H H0 H1} {_}.
 
 Time Compute
   rmatch

mechanization/tactics/Tactics.v

@@ -34,8 +34,8 @@ Tactic Notation "exApplyW" hyp(H) hyp(w) "as" simple_intropattern(As) :=
 Ltac clean_injection H := injection H; clear H; intros.
 
 Ltac bookkeeper := repeat (
-      Stdlib.Program.Tactics.destruct_conjs 
-  ||  Stdlib.Program.Tactics.clear_dups 
+      destruct_conjs 
+  ||  clear_dups 
   ||  subst
   ||  lazymatch goal with
       | [ H: _ = _ |- _ ] => clean_injection H || discriminate H

mechanization/utils/List.v

@@ -49,7 +49,7 @@ Module List.
   Proof.
     intros l1 l2 p12 p21 Eq_l1 Eq_l2. 
     pose proof (@f_equal _ _ (@length _) _ _ Eq_l1). pose proof (@f_equal _ _ (@length _) _ _ Eq_l2).
-    rewrite -> app_length in *.
+    rewrite -> length_app in *.
     assert (length p12 = 0)%nat as Eq_p12 by lia. assert (length p21 = 0)%nat as Eq_p21 by lia.
     rewrite -> length_zero_iff_nil in *. subst. reflexivity.
   Qed.