Export new Tactics

Author: mattam82

plugin/plugin-bootstrap/Extraction.v

@@ -1,4 +1,9 @@
+(** The plugin loader *)
 From VerifiedExtraction Require Export Loader.
-From Malfunction Require Export PrintMli.
+(* From Malfunction Require Export PrintMli. *)
 
+(** Bindings to primitive type implementations. *)
 From VerifiedExtraction Require Export PrimInt63 PrimFloat PrimArray PrimString RocqMsgFFI.
+
+(** Ltac2 tactics using the erasure cast for reflexive proofs. *)
+From VerifiedExtraction Require Export Tactics.

plugin/plugin-bootstrap/_RocqProject

@@ -14,4 +14,5 @@ PrimString.v
 PrimArray.v
 OCamlFFI.v
 RocqMsgFFI.v
+Tactics.v
 Extraction.v