diff options
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 10 |
1 files changed, 3 insertions, 7 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index af53f16e1f..0179215d6a 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -394,10 +394,7 @@ let jmeq_refl () = @@ Coqlib.lib_ref "core.JMeq.refl" with e when CErrors.noncritical e -> raise (ToShow e) -let h_intros l = - Proofview.V82.of_tactic - (Tacticals.New.tclMAP (fun x -> Tactics.Simple.intro x) l) - +let h_intros l = Tacticals.New.tclMAP (fun x -> Tactics.Simple.intro x) l let h_id = Id.of_string "h" let hrec_id = Id.of_string "hrec" @@ -428,13 +425,12 @@ let evaluable_of_global_reference r = | _ -> assert false let list_rewrite (rev : bool) (eqs : (EConstr.constr * bool) list) = - let open Tacticals in + let open Tacticals.New in (tclREPEAT (List.fold_right (fun (eq, b) i -> tclORELSE - (Proofview.V82.of_tactic - ((if b then Equality.rewriteLR else Equality.rewriteRL) eq)) + ((if b then Equality.rewriteLR else Equality.rewriteRL) eq) i) (if rev then List.rev eqs else eqs) (tclFAIL 0 (mt ()))) [@ocaml.warning "-3"]) |