- let initial_lexicon_status =
- CicNotation2.load_notation ~include_paths:[] BuildTimeConf.core_notation_script
- in
- let b,x =
- try
- GrafiteSync.push ();
- LexiconSync.time_travel ~present:x ~past:initial_lexicon_status;
- let rc = MatitacLib.Make.make root [tgt] in
- GrafiteSync.pop ();
- CicNotation.reset ();
- ignore(CicNotation2.load_notation ~include_paths:[]
- BuildTimeConf.core_notation_script);
- let x = List.fold_left (fun s c -> LexiconEngine.eval_command s c)
- initial_lexicon_status (List.rev
- x.LexiconEngine.lexicon_content_rev)
- in
- rc,x
- with
- | exn ->
- HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));
- assert false
- in