diff options
| author | Pierre-Marie Pédrot | 2020-05-06 19:04:11 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-07 17:30:33 +0200 |
| commit | ffda464321e856e44c7f99e6aab201770781c806 (patch) | |
| tree | e9e05c835f49c401254bad0646ae0db8fff3a4e2 /plugins/funind/indfun_common.ml | |
| parent | 36f8369d948720de61194596015a80731dcc6198 (diff) | |
Remove call to Refiner API from Funind.
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 -> |