diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-01 20:53:32 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:21:51 +0100 |
| commit | 8f6aab1f4d6d60842422abc5217daac806eb0897 (patch) | |
| tree | c36f2f963064f51fe1652714f4d91677d555727b /plugins/setoid_ring | |
| parent | 5143129baac805d3a49ac3ee9f3344c7a447634f (diff) | |
Reductionops API using EConstr.
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 657efe175..cf0f51911 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -82,6 +82,7 @@ let lookup_map map = user_err ~hdr:"lookup_map" (str"map "++qs map++str"not found") let protect_red map env sigma c = + let c = EConstr.Unsafe.to_constr c in kl (create_clos_infos all env) (mk_clos_but (lookup_map map c) (Esubst.subs_id 0) c);; @@ -347,7 +348,7 @@ let find_ring_structure env sigma l = let ty = Retyping.get_type_of env sigma t in let check c = let ty' = Retyping.get_type_of env sigma c in - if not (Reductionops.is_conv env sigma ty ty') then + if not (Reductionops.is_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr ty')) then user_err ~hdr:"ring" (str"arguments of ring_simplify do not have all the same type") in @@ -827,7 +828,7 @@ let find_field_structure env sigma l = let ty = Retyping.get_type_of env sigma t in let check c = let ty' = Retyping.get_type_of env sigma c in - if not (Reductionops.is_conv env sigma ty ty') then + if not (Reductionops.is_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr ty')) then user_err ~hdr:"field" (str"arguments of field_simplify do not have all the same type") in |