diff options
author | 2008-10-28 18:31:47 +0000 | |
---|---|---|
committer | 2008-10-28 18:31:47 +0000 | |
commit | 578f31889234edba078e14f4152421123c1bc466 (patch) | |
tree | 666100c2e569e471ceebb9cc3a3fa045a33d4960 | |
parent | adc2d160c5ee9f750a5a360f97a01fc500bbae78 (diff) |
petite modif du commit 11513.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11517 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | kernel/modops.ml | 22 |
1 files changed, 13 insertions, 9 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index 84c47c003..f904bab54 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -235,15 +235,19 @@ let add_retroknowledge msid mp = let strengthen_const env mp l cb = - let const = mkConst (make_con mp empty_dirpath l) in - let const_subs = Some (Declarations.from_val const) in - {cb with - const_body = const_subs; - const_opaque = false; - const_body_code = Cemitcodes.from_val - (compile_constant_body env const_subs false false) - } - + match cb.const_opaque, cb.const_body with + | false, Some _ -> cb + | true, Some _ + | _, None -> + let const = mkConst (make_con mp empty_dirpath l) in + let const_subs = Some (Declarations.from_val const) in + {cb with + const_body = const_subs; + const_opaque = false; + const_body_code = Cemitcodes.from_val + (compile_constant_body env const_subs false false) + } + let strengthen_mind env mp l mib = match mib.mind_equiv with | Some _ -> mib | None -> {mib with mind_equiv = Some (make_kn mp empty_dirpath l)} |