compatibility with coq 8.6

.gitignore

@@ -16,4 +16,5 @@ _build
 src/myocamlbuild.ml
 *~
 *.glob
-*.vo
+*.vo
+*.aux

src/use_ltac.ml

@@ -9,11 +9,22 @@ let ltac_lcall tac args =
 let ltac_letin (x, e1) e2 =
   Tacexpr.TacLetIn(false,[(Loc.dummy_loc,Names.id_of_string x),e1],e2)
 
-let ltac_apply (f:Tacexpr.glob_tactic_expr) (args:Tacexpr.glob_tactic_arg list) =
-  Tacinterp.eval_tactic
-    (ltac_letin ("F", Tacexpr.Tacexp f) (ltac_lcall "F" args))
+(* Copied from coq/plugins/setoid_ring/newring.ml *)
+let ltac_apply (f : Tacinterp.Value.t) (args: Tacinterp.Value.t list) =
+  let open Names in
+  let open Tacexpr in
+  let open Misctypes in
+  let fold arg (i, vars, lfun) =
+    let id = Id.of_string ("x" ^ string_of_int i) in
+    let x = Reference (ArgVar (Loc.ghost, id)) in
+    (succ i, x :: vars, Id.Map.add id arg lfun)
+  in
+  let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in
+  let lfun = Id.Map.add (Id.of_string "F") f lfun in
+  let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun = lfun; } in
+  Tacinterp.eval_tactic_ist ist (ltac_lcall "F" args)
 
-let to_ltac_val c = Tacexpr.TacDynamic(Loc.dummy_loc,Pretyping.constr_in c)
+let to_ltac_val c = Tacinterp.Value.of_constr c
 
 (** Pose **)
 
@@ -26,10 +37,11 @@ let nowhere =
 
 let pose (name : string) (value : Term.constr)
     (k : Term.constr -> 'a Proofview.tactic) : 'a Proofview.tactic =
-  Proofview.Goal.enter (fun gl ->
-     let name = Names.id_of_string name in
-     let fresh_name =
-       Tactics.fresh_id_in_env [] name (Proofview.Goal.env gl)
-     in
-     Proofview.tclTHEN (Tactics.letin_tac None (Names.Name fresh_name) value None nowhere)
-		       (k (Term.mkVar fresh_name)))
+  Proofview.Goal.enter { enter = begin fun gl ->
+      let name = Names.id_of_string name in
+      let fresh_name =
+        Tactics.fresh_id_in_env [] name (Proofview.Goal.env gl)
+      in
+      Proofview.tclTHEN (Tactics.letin_tac None (Names.Name fresh_name) value None nowhere)
+	(k (Term.mkVar fresh_name))
+    end }

src/use_ltac.mli

@@ -2,12 +2,12 @@
  ** [xs] arguments. The result is a tactic that can be run by passing it
  ** an appropriate [goal sigma].
  **)
-val ltac_apply : Tacexpr.glob_tactic_expr -> Tacexpr.glob_tactic_arg list -> unit Proofview.tactic
+val ltac_apply : Tacinterp.Value.t -> Tacinterp.Value.t list -> unit Proofview.tactic
 
 (** Convert a Gallina term (Term.constr) into an Ltac value which
  ** can be passed to an Ltac function.
  **)
-val to_ltac_val : Term.constr -> Tacexpr.glob_tactic_arg
+val to_ltac_val : Term.constr -> Tacinterp.Value.t
 
 
 (** [pose n c k] ~ ltac:(pose (n := c) ; k n) **)