diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-02-13 17:49:21 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-03-04 15:13:02 +0100 |
| commit | 16c884413bbf2f0b5fb43bd0be7da0bf7c5e4e75 (patch) | |
| tree | a0685d4245d355104d2c84feaf0950df6fb18e02 /plugins/setoid_ring | |
| parent | df9d3a36e71d6d224286811fdc529ad5a955deb7 (diff) | |
Pass the constant cache as a separate argument in kernel reduction.
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 125afb1a0..0fb79ff25 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -88,7 +88,7 @@ let lookup_map map = let protect_red map env sigma c0 = let evars ev = Evarutil.safe_evar_value sigma ev in let c = EConstr.Unsafe.to_constr c0 in - EConstr.of_constr (kl (create_clos_infos ~evars all env) + EConstr.of_constr (kl (create_clos_infos ~evars all env) (create_tab ()) (mk_clos_but (lookup_map map sigma c0) (Esubst.subs_id 0) c));; let protect_tac map = |