Backport Ltac2 to Coq 8.7.

_CoqProject

@@ -1,6 +1,5 @@
 -R theories/ Ltac2
 -I src/
--bypass-API
 
 src/tac2dyn.ml
 src/tac2dyn.mli

src/g_ltac2.ml4

@@ -91,8 +91,7 @@ let tac2def_mut = Gram.entry_create "tactic:tac2def_mut"
 let tac2def_run = Gram.entry_create "tactic:tac2def_run"
 let tac2mode = Gram.entry_create "vernac:ltac2_command"
 
-(** FUCK YOU API *)
-let ltac1_expr = (Obj.magic Pltac.tactic_expr : Tacexpr.raw_tactic_expr Gram.entry)
+let ltac1_expr = Pltac.tactic_expr
 
 let inj_wit wit loc x = Loc.tag ~loc @@ CTacExt (wit, x)
 let inj_open_constr loc c = inj_wit Tac2quote.wit_open_constr loc c
@@ -831,11 +830,10 @@ let classify_ltac2 = function
 | StrSyn _ -> Vernacexpr.VtUnknown, Vernacexpr.VtNow
 | StrMut _ | StrVal _ | StrPrm _  | StrTyp _ | StrRun _ -> Vernac_classifier.classify_as_sideeff
 
-VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTactic2Definition
+VERNAC COMMAND EXTEND VernacDeclareTactic2Definition
 | [ "Ltac2" ltac2_entry(e) ] => [ classify_ltac2 e ] -> [
-    fun ~atts ~st -> let open Vernacinterp in
-    Tac2entries.register_struct ?local:atts.locality e;
-    st
+    let local = Locality.LocalityFixme.consume () in
+    Tac2entries.register_struct ?local e
   ]
 END
 

src/tac2core.ml

@@ -561,7 +561,7 @@ let () = define2 "pattern_matches_subterm" pattern constr begin fun pat c ->
     Proofview.tclOR (return ans) (fun _ -> of_ans s)
   in
   pf_apply begin fun env sigma ->
-    let ans = Constr_matching.match_subterm env sigma (Id.Set.empty,pat) c in
+    let ans = Constr_matching.match_appsubterm env sigma pat c in
     of_ans ans
   end
 end
@@ -593,7 +593,7 @@ let () = define2 "pattern_matches_subterm_vect" pattern constr begin fun pat c -
     Proofview.tclOR (return ans) (fun _ -> of_ans s)
   in
   pf_apply begin fun env sigma ->
-    let ans = Constr_matching.match_subterm env sigma (Id.Set.empty,pat) c in
+    let ans = Constr_matching.match_appsubterm env sigma pat c in
     of_ans ans
   end
 end
@@ -828,7 +828,7 @@ let open_constr_no_classes_flags () =
 let to_lvar ist =
   let open Glob_ops in
   let lfun = Tac2interp.set_env ist Id.Map.empty in
-  { empty_lvar with Ltac_pretype.ltac_genargs = lfun }
+  { empty_lvar with Glob_term.ltac_genargs = lfun }
 
 let gtypref kn = GTypRef (Other kn, [])
 
@@ -945,16 +945,15 @@ let () =
     let ist = { env_ist = Id.Map.empty } in
     let lfun = Tac2interp.set_env ist Id.Map.empty in
     let ist = Ltac_plugin.Tacinterp.default_ist () in
-    (** FUCK YOU API *)
-    let ist = { ist with API.Geninterp.lfun = (Obj.magic lfun) } in
-    let tac = (Obj.magic Ltac_plugin.Tacinterp.eval_tactic_ist ist tac : unit Proofview.tactic) in
+    let ist = { ist with Geninterp.lfun = lfun } in
+    let tac = Ltac_plugin.Tacinterp.eval_tactic_ist ist tac in
     let wrap (e, info) = set_bt info >>= fun info -> Proofview.tclZERO ~info e in
     Proofview.tclOR tac wrap >>= fun () ->
     return v_unit
   in
   let subst s tac = Genintern.substitute Ltac_plugin.Tacarg.wit_tactic s tac in
   let print env tac =
-    str "ltac1:(" ++ Ltac_plugin.Pptactic.pr_glob_tactic (Obj.magic env) tac ++ str ")"
+    str "ltac1:(" ++ Ltac_plugin.Pptactic.pr_glob_tactic env tac ++ str ")"
   in
   let obj = {
     ml_intern = intern;
@@ -987,25 +986,22 @@ let () =
   Pretyping.register_constr_interp0 wit_ltac2_quotation interp
 
 let () =
-  let pr_raw id = Genprint.PrinterBasic mt in
-  let pr_glb id = Genprint.PrinterBasic (fun () -> str "$" ++ Id.print id) in
-  let pr_top _ = Genprint.TopPrinterBasic mt in
+  let pr_raw id = mt () in
+  let pr_glb id = str "$" ++ Id.print id in
+  let pr_top _ = mt () in
   Genprint.register_print0 wit_ltac2_quotation pr_raw pr_glb pr_top
 
 (** Ltac2 in Ltac1 *)
 
 let () =
-  (** FUCK YOU API *)
-  let e = (Obj.magic Tac2entries.Pltac.tac2expr : _ API.Pcoq.Gram.entry) in
+  let e = Tac2entries.Pltac.tac2expr in
   let inject (loc, v) = Tacexpr.TacGeneric (in_gen (rawwit wit_ltac2) v) in
   Ltac_plugin.Tacentries.create_ltac_quotation "ltac2" inject (e, None)
 
 let () =
   let open Ltac_plugin in
   let open Tacinterp in
   let idtac = Value.of_closure (default_ist ()) (Tacexpr.TacId []) in
-  (** FUCK YOU API *)
-  let idtac = (Obj.magic idtac : Geninterp.Val.t) in
   let interp ist tac =
 (*     let ist = Tac2interp.get_env ist.Geninterp.lfun in *)
     let ist = { env_ist = Id.Map.empty } in
@@ -1015,9 +1011,9 @@ let () =
   Geninterp.register_interp0 wit_ltac2 interp
 
 let () =
-  let pr_raw _ = Genprint.PrinterBasic mt in
-  let pr_glb e = Genprint.PrinterBasic (fun () -> Tac2print.pr_glbexpr e) in
-  let pr_top _ = Genprint.TopPrinterBasic mt in
+  let pr_raw _ = mt () in
+  let pr_glb e = Tac2print.pr_glbexpr e in
+  let pr_top _ = mt () in
   Genprint.register_print0 wit_ltac2 pr_raw pr_glb pr_top
 
 (** Built-in notation scopes *)

src/tac2entries.ml

@@ -750,7 +750,7 @@ let perform_eval e =
   let v = Tac2interp.interp Tac2interp.empty_environment e in
   let selector, proof =
     try
-      Proof_bullet.get_default_goal_selector (),
+      Proof_global.get_default_goal_selector (),
       Proof_global.give_me_the_proof ()
     with Proof_global.NoCurrentProof ->
       let sigma = Evd.from_env env in
@@ -866,7 +866,7 @@ let print_ltac ref =
 let solve default tac =
   let status = Proof_global.with_current_proof begin fun etac p ->
     let with_end_tac = if default then Some etac else None in
-    let g = Proof_bullet.get_default_goal_selector () in
+    let g = Proof_global.get_default_goal_selector () in
     let (p, status) = Pfedit.solve g None tac ?with_end_tac p in
     (* in case a strict subtree was completed,
        go back to the top of the prooftree *)

src/tac2env.ml

@@ -280,8 +280,6 @@ let std_prefix =
 
 let wit_ltac2 = Genarg.make0 "ltac2:value"
 let wit_ltac2_quotation = Genarg.make0 "ltac2:quotation"
-let () = Geninterp.register_val0 wit_ltac2 None
-let () = Geninterp.register_val0 wit_ltac2_quotation None
 
 let is_constructor qid =
   let (_, id) = repr_qualid qid in

src/tac2interp.mli

@@ -20,8 +20,8 @@ val interp : environment -> glb_tacexpr -> valexpr Proofview.tactic
 
 (** {5 Cross-boundary encodings} *)
 
-val get_env : Ltac_pretype.unbound_ltac_var_map -> environment
-val set_env : environment -> Ltac_pretype.unbound_ltac_var_map -> Ltac_pretype.unbound_ltac_var_map
+val get_env : Glob_term.unbound_ltac_var_map -> environment
+val set_env : environment -> Glob_term.unbound_ltac_var_map -> Glob_term.unbound_ltac_var_map
 
 (** {5 Exceptions} *)
 

src/tac2match.ml

@@ -14,7 +14,7 @@ module NamedDecl = Context.Named.Declaration
 type context = EConstr.t
 
 type result = {
-  subst : Ltac_pretype.patvar_map ;
+  subst : Pattern.patvar_map ;
 }
 
 type match_pattern =
@@ -173,7 +173,7 @@ module PatternMatching (E:StaticEnvironment) = struct
             | Some nctx -> Proofview.tclOR (k (Some m_ctx) nctx) (fun e -> (map s e).stream k ctx)
         }
       in
-      map (Constr_matching.match_subterm E.env E.sigma (Id.Set.empty,p) term) imatching_error
+      map (Constr_matching.match_appsubterm E.env E.sigma p term) imatching_error
 
   let hyp_match_type pat hyps =
     pick hyps >>= fun decl ->

src/tac2match.mli

@@ -30,4 +30,4 @@ val match_goal:
   match_rule ->
     ((Id.t * context option) list * (** List of hypotheses matching: name + context *)
     context option * (** Context for conclusion *)
-    Ltac_pretype.patvar_map (** Pattern variable substitution *)) Proofview.tactic
+    Pattern.patvar_map (** Pattern variable substitution *)) Proofview.tactic

src/tac2quote.ml

@@ -421,7 +421,7 @@ let of_goal_matching (loc, gm) =
       let vars = pattern_vars pat in
       (Id.Set.union vars accu, (na, ctx, pat, knd))
     in
-    let (vars, hyps_pats) = List.fold_left_map map vars hyps_pats in
+    let (vars, hyps_pats) = List.fold_map map vars hyps_pats in
     let map (_, _, pat, knd) = of_tuple [knd; of_pattern pat] in
     let concl = of_tuple [concl_knd; of_pattern concl_pat] in
     let r = of_tuple [of_list ?loc map hyps_pats; concl] in

src/tac2tactics.ml

@@ -361,7 +361,7 @@ let discriminate ev arg =
 let injection ev ipat arg =
   let arg = Option.map (fun arg -> None, arg) arg in
   let ipat = Option.map mk_intro_patterns ipat in
-  let tac ev arg = Equality.injClause None ipat ev arg in
+  let tac ev arg = Equality.injClause ipat ev arg in
   on_destruction_arg tac ev arg
 
 let autorewrite ~all by ids cl =
@@ -448,10 +448,6 @@ let contradiction c =
 
 let firstorder tac refs ids =
   let open Ground_plugin in
-  (** FUCK YOU API *)
   let ids = List.map Id.to_string ids in
   let tac = Option.map (fun tac -> thaw Tac2ffi.unit tac) tac in
-  let tac : unit API.Proofview.tactic option = Obj.magic (tac : unit Proofview.tactic option) in
-  let refs : API.Globnames.global_reference list = Obj.magic (refs : Globnames.global_reference list) in
-  let ids : API.Hints.hint_db_name list = Obj.magic (ids : Hints.hint_db_name list) in
-  (Obj.magic (G_ground.gen_ground_tac true tac refs ids : unit API.Proofview.tactic) : unit Proofview.tactic)
+  G_ground.gen_ground_tac true tac refs ids