let addDebugSeparator () =
ignore (GMenu.separator_item ~packing:gui#main#debugMenu_menu#append ())
in
+ addDebugItem "dump aliases" (fun _ ->
+ let status = script#lexicon_status in
+ HLog.debug (DisambiguatePp.pp_environment status.LexiconEngine.aliases));
addDebugItem "dump environment to \"env.dump\"" (fun _ ->
let oc = open_out "env.dump" in
CicEnvironment.dump_to_channel oc;
(MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status
with
| GrafiteTypes.No_proof -> (Cic.Implicit None)
- | Incomplete_proof i -> let _,_,_subst,p,_, _ = i.GrafiteTypes.proof in p
- | Proof p -> let _,_,_subst,p,_, _ = p in p
+ | Incomplete_proof i ->
+ let _,_,_subst,p,_, _ = i.GrafiteTypes.proof in
+ Lazy.force p
+ | Proof p -> let _,_,_subst,p,_, _ = p in Lazy.force p
| Intermediate _ -> assert false)));
addDebugItem "Print current proof (natural language) to stderr"
(fun _ ->
| GrafiteTypes.No_proof -> assert false
| Incomplete_proof i ->
let _,m,_subst,p,ty, attrs = i.GrafiteTypes.proof in
- Cic.CurrentProof ("current (incomplete) proof",m,p,ty,[],attrs)
+ Cic.CurrentProof ("current (incomplete) proof",m,Lazy.force p,ty,[],attrs)
| Proof (_,m,_subst,p,ty, attrs) ->
- Cic.CurrentProof ("current proof",m,p,ty,[],attrs)
+ Cic.CurrentProof ("current proof",m,Lazy.force p,ty,[],attrs)
| Intermediate _ -> assert false)));
(* addDebugItem "ask record choice"
(fun _ ->