Adapt w.r.t. coq/coq#15159.

src/gappatac.c

@@ -10,7 +10,11 @@ open Format
 open Util
 open Pp
 open Term
+#if COQVERSION >= 81500
+open Tacmach.Old
+#else
 open Tacmach
+#endif
 open Names
 open Coqlib
 open Libnames
@@ -91,9 +95,13 @@ let keep a = Proofview.V82.of_tactic (Tactics.keep a)
 #if COQVERSION >= 81500
 let convert_concl_no_check a =
   Proofview.V82.of_tactic (Tactics.convert_concl ~cast:false ~check:false a Constr.DEFAULTcast)
+
+let tclTHEN = Tacticals.Old.tclTHEN
 #else
 let convert_concl_no_check a =
   Proofview.V82.of_tactic (Tactics.convert_concl ~check:false a Constr.DEFAULTcast)
+
+let tclTHEN = Tacticals.tclTHEN
 #endif
 
 #if COQVERSION < 80900
@@ -560,8 +568,8 @@ let gappa_quote gl =
     (*Pp.msgerrnl (pr_constr e);*)
     Hashtbl.clear var_terms;
     var_list := [];
-    Tacticals.tclTHEN
-      (Tacticals.tclTHEN
+    tclTHEN
+      (tclTHEN
         (generalize (List.map (fun (n, _) -> mkVar (binder_name n)) (List.rev l)))
         (keep []))
       (convert_concl_no_check e) gl