Commit 811887fa authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

fix an invariant violation in the previous commit:

the [Duse] declaration are preserved on Context.use_export,
so that ctxt_known can be always restored from ctxt_decls.
parent 1c21c061
......@@ -443,7 +443,7 @@ module Context = struct
let d = create_use th in
let kn = add_known ctxt.ctxt_known th.th_name d in
let ctxt = Hctxt.hashcons { ctxt with ctxt_known = kn } in
let ctxt = push_kn_decl ctxt kn d in
let add_decl ctxt d = match d.d_node with
| Dtype _ | Dlogic _ | Dprop _ -> add_decl ctxt d
| Duse th -> use_export ctxt th
(* test file *)
theory Test
inductive p(int) =
| A : 0=0
theory ThA
type 'a t = None | Some ('a)
type s
logic c : s
theory TestPrelude
use prelude.Int
use prelude.List
theory ThB
use export prelude.List
clone ThA with type s = int
theory ThC
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment