diff options
| -rw-r--r-- | engine/geninterp.ml | 5 | ||||
| -rw-r--r-- | engine/geninterp.mli | 2 | ||||
| -rw-r--r-- | ltac/rewrite.ml | 6 | ||||
| -rw-r--r-- | ltac/tacinterp.ml | 3 | ||||
| -rw-r--r-- | tactics/auto.ml | 4 | ||||
| -rw-r--r-- | tactics/autorewrite.ml | 4 |
6 files changed, 11 insertions, 13 deletions
diff --git a/engine/geninterp.ml b/engine/geninterp.ml index 0d6721367..be4011cb6 100644 --- a/engine/geninterp.ml +++ b/engine/geninterp.ml @@ -28,8 +28,3 @@ module Interp = Register(InterpObj) let interp = Interp.obj let register_interp0 = Interp.register0 - -let generic_interp ist (GenArg (Glbwit wit, v)) = - let open Ftactic.Notations in - interp wit ist v >>= fun ans -> - Ftactic.return (Val.inject (val_tag (topwit wit)) ans) diff --git a/engine/geninterp.mli b/engine/geninterp.mli index 0992db7a2..0e7ed1847 100644 --- a/engine/geninterp.mli +++ b/engine/geninterp.mli @@ -21,7 +21,5 @@ type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun -val generic_interp : (glob_generic_argument, Val.t) interp_fun - val register_interp0 : ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun -> unit diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 97b2393a8..cd8ce7e87 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -613,8 +613,10 @@ let solve_remaining_by env sigma holes by = (** Only solve independent holes *) let indep = List.map_filter map holes in let ist = { Geninterp.lfun = Id.Map.empty; extra = Geninterp.TacStore.empty } in - let solve_tac = Geninterp.generic_interp ist tac in - let solve_tac = Ftactic.run solve_tac (fun _ -> Proofview.tclUNIT ()) in + let solve_tac = match tac with + | Genarg.GenArg (Genarg.Glbwit tag, tac) -> + Ftactic.run (Geninterp.interp tag ist tac) (fun _ -> Proofview.tclUNIT ()) + in let solve_tac = Tacticals.New.tclCOMPLETE solve_tac in let solve sigma evk = let evi = diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 90784f5e8..b9d074a3d 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1569,7 +1569,8 @@ and interp_genarg ist x : Val.t Ftactic.t = let q = Value.cast (topwit wit2) q in Ftactic.return (Value.of_pair (val_tag wit1) (val_tag wit2) (p, q)) | ExtraArg s -> - Geninterp.generic_interp ist (Genarg.in_gen (glbwit wit) x) + Geninterp.interp wit ist x >>= fun x -> + Ftactic.return (in_gen (Topwit wit) x) (** returns [true] for genargs which have the same meaning independently of goals. *) diff --git a/tactics/auto.ml b/tactics/auto.ml index d7ce0d4c1..46f484bf0 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -160,7 +160,9 @@ let conclPattern concl pat tac = let fold id c accu = Id.Map.add id (inj c) accu in let lfun = Id.Map.fold fold constr_bindings Id.Map.empty in let ist = { lfun; extra = TacStore.empty } in - Ftactic.run (Geninterp.generic_interp ist tac) (fun _ -> Proofview.tclUNIT ()) + match tac with + | GenArg (Glbwit wit, tac) -> + Ftactic.run (Geninterp.interp wit ist tac) (fun _ -> Proofview.tclUNIT ()) end } (***********************************************************) diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 4816f8a45..950eeef52 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -106,9 +106,9 @@ let one_base general_rewrite_maybe_in tac_main bas = let lrul = List.map (fun h -> let tac = match h.rew_tac with | None -> Proofview.tclUNIT () - | Some tac -> + | Some (Genarg.GenArg (Genarg.Glbwit wit, tac)) -> let ist = { Geninterp.lfun = Id.Map.empty; extra = Geninterp.TacStore.empty } in - Ftactic.run (Geninterp.generic_interp ist tac) (fun _ -> Proofview.tclUNIT ()) + Ftactic.run (Geninterp.interp wit ist tac) (fun _ -> Proofview.tclUNIT ()) in (h.rew_ctx,h.rew_lemma,h.rew_l2r,tac)) lrul in Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS (List.fold_left (fun tac (ctx,csr,dir,tc) -> |