diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/critical-bugs | 12 | ||||
| -rw-r--r-- | dev/top_printers.ml | 1 |
2 files changed, 13 insertions, 0 deletions
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index f532e1b68f..01c2b574a2 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -195,6 +195,18 @@ Conversion machines GH issue number: ? risk: + component: "virtual machine" (compilation to bytecode ran by a C-interpreter) + summary: primitive integer emulation layer on 32 bits not robust to garbage collection + introduced: master (before v8.10 in GH pull request #6914) + impacted released versions: none + impacted development branches: + impacted coqchk versions: none (no virtual machine in coqchk) + fixed in: + found by: Roux, Melquiond + exploit: + GH issue number: #9925 + risk: + component: "native" conversion machine (translation to OCaml which compiles to native code) summary: translation of identifier from Coq to OCaml was not bijective, leading to identify True and False introduced: V8.5 diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 74be300134..816316487c 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -65,6 +65,7 @@ let get_current_context () = with Vernacstate.Proof_global.NoCurrentProof -> let env = Global.env() in Evd.from_env env, env + [@@ocaml.warning "-3"] (* term printers *) let envpp pp = let sigma,env = get_current_context () in pp env sigma |