diff options
| author | Pierre-Marie Pédrot | 2019-09-26 17:02:26 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-04 18:00:26 +0200 |
| commit | 69551b566a1339543967a41ff4aaa4580e7394fc (patch) | |
| tree | 4b60e8a6bb3c25c029e43fd40fd56e5839db6e68 /kernel/cooking.ml | |
| parent | d5f2e13e51c3404d326f04513a50d264790a7a4c (diff) | |
Merge Direct and Indirect nodes in Opaqueproof.
Diffstat (limited to 'kernel/cooking.ml')
| -rw-r--r-- | kernel/cooking.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 0951b07d49..087453c31c 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -239,7 +239,7 @@ let cook_constant { from = cb; info } = | Undef _ as x -> x | Def cs -> Def (Mod_subst.from_val (map (Mod_subst.force_constr cs))) | OpaqueDef o -> - OpaqueDef (Opaqueproof.discharge_direct_opaque info o) + OpaqueDef (Opaqueproof.discharge_opaque info o) | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked") in let const_hyps = |