diff options
| author | Maxime Dénès | 2019-10-12 13:28:35 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-10-12 13:28:35 +0200 |
| commit | cc4cddda2eb2a05f685c8404e4864ea0bcdac6eb (patch) | |
| tree | 134dc9c5bb95fd26789556231f73c69896b5255f /kernel/cooking.ml | |
| parent | e8d0b5a8856a695dc3f6a28e2d305c095ef50c19 (diff) | |
| parent | 69551b566a1339543967a41ff4aaa4580e7394fc (diff) | |
Merge PR #10818: Merge Direct and Indirect nodes in Opaqueproof.
Reviewed-by: gares
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 b88a2e6194..fae06f7163 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 = Id.Set.diff (Context.Named.to_vars cb.const_hyps) (Context.Named.to_vars hyps0) in |