diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-05-31 16:24:15 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-06-09 18:56:41 +0200 |
| commit | 55cd7e662ecdcf0f82bc76bdff2ad28f2cdef01c (patch) | |
| tree | 55501954dd115a91d154f49259ef4a0fee078a38 /plugins/setoid_ring | |
| parent | 7527751d9772656b4680df311546825cc2dd3d8f (diff) | |
newring: fix for hack using evars as integers.
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 19 |
1 files changed, 4 insertions, 15 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 154ec6e1b..5b626debd 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -34,15 +34,6 @@ open Proofview.Notations (****************************************************************************) (* controlled reduction *) -(** ppedrot: something dubious here, we're obviously using evars the wrong - way. FIXME! *) - -let mark_arg i c = mkEvar(Evar.unsafe_of_int i,[|c|]) -let unmark_arg f c = - match destEvar c with - | (i,[|c|]) -> f (Evar.repr i) c - | _ -> assert false - type protect_flag = Eval|Prot|Rec let tag_arg tag_rec map subs i c = @@ -75,12 +66,10 @@ and mk_clos_app_but f_map subs f args n = let fargs, args' = Array.chop n args in let f' = mkApp(f,fargs) in match f_map (global_of_constr_nofail f') with - Some map -> - mk_clos_deep - (fun s' -> unmark_arg (tag_arg (mk_clos_but f_map s') map s')) - subs - (mkApp (mark_arg (-1) f', Array.mapi mark_arg args')) - | None -> mk_clos_app_but f_map subs f args (n+1) + | Some map -> + let f i t = tag_arg (mk_clos_but f_map subs) map subs i t in + mk_red (FApp (f (-1) f', Array.mapi f args')) + | None -> mk_atom (mkApp (f, args)) let interp_map l t = try Some(List.assoc_f eq_gr t l) with Not_found -> None |