diff options
| -rw-r--r-- | kernel/safe_typing.ml | 4 | ||||
| -rw-r--r-- | kernel/term_typing.mli | 1 |
2 files changed, 3 insertions, 2 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 09f7bd75c..95d9c75d3 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -213,8 +213,8 @@ type private_constant_role = Term_typing.side_effect_role = | Schema of inductive * string let empty_private_constants = [] -let add_private x xs = x :: xs -let concat_private xs ys = xs @ ys +let add_private x xs = if List.mem_f Term_typing.equal_eff x xs then xs else x :: xs +let concat_private xs ys = List.fold_right add_private xs ys let mk_pure_proof = Term_typing.mk_pure_proof let inline_private_constants_in_constr = Term_typing.inline_side_effects let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index fcd95576c..89b5fc40e 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -30,6 +30,7 @@ val inline_entry_side_effects : yet type checked proof. *) val uniq_seff : side_effects -> side_effects +val equal_eff : side_effect -> side_effect -> bool val translate_constant : structure_body -> env -> constant -> side_effects constant_entry -> |