diff options
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index e83fe56cc9..0e7d3c2f3b 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -2,7 +2,7 @@ open Names open Pp open Constr open Libnames -open Refiner +open Tacmach let mk_prefix pre id = Id.of_string (pre ^ Id.to_string id) let mk_rel_id = mk_prefix "R_" @@ -427,6 +427,7 @@ let evaluable_of_global_reference r = | _ -> assert false let list_rewrite (rev : bool) (eqs : (EConstr.constr * bool) list) = + let open Tacticals in tclREPEAT (List.fold_right (fun (eq, b) i -> |