Merge pull request #128 from SkySkimmer/ltacX-obligations

Adapt to rocq-prover/rocq#19690 (generic_tactic avoids dependency on ltac(?))

Author: ppedrot

src/abstraction.mlg

@@ -15,20 +15,18 @@
 DECLARE PLUGIN "coq-paramcoq.plugin"
 
 {
-open Ltac_plugin
 open Feedback
 open Stdarg
-open Tacarg
 open Parametricity
 open Declare_translation
 }
 
 VERNAC COMMAND EXTEND SetParametricityTactic CLASSIFIED AS SIDEFF
 | #[ locality = Tactic_option.tac_option_locality; ]
- [ "Parametricity" "Tactic" ":=" tactic(t) ] -> {
+ [ "Parametricity" "Tactic" ":=" generic_tactic(t) ] -> {
  Relations.set_parametricity_tactic
  locality
- (Tacintern.glob_tactic t) }
+ (Gentactic.intern (Global.env()) t) }
 END
 
 VERNAC COMMAND EXTEND ShowTable CLASSIFIED AS QUERY

src/dune

@@ -3,6 +3,6 @@
  (public_name coq-paramcoq.plugin)
  (synopsis "Plugin for generating parametricity statements to perform refinement proofs")
  (flags :standard -rectypes -w -9-27)
- (libraries coq-core.plugins.ltac))
+ (libraries coq-core.plugins.ltac)) ; not sure if ltac dep is real
 
 (coq.pp (modules abstraction))

src/relations.ml

@@ -10,7 +10,6 @@
 (**************************************************************************)
 
 
-open Ltac_plugin
 open Names
 open Globnames
 open Libobject