self#_loadTermAst (disambiguator#parserr#parseTerm (Stream.of_string s))
method private _loadTermAst ast =
- let (_, _, term, _) =
+ let (_, metasenv, term, _) =
MatitaCicMisc.disambiguate ~disambiguator ~currentProof ast
in
- self#_loadTermCic term
+ self#_loadTermCic term metasenv
- method private _loadTermCic term =
- let (context, metasenv) =
+ method private _loadTermCic term metasenv =
+ let (context, _) =
MatitaCicMisc.get_context_and_metasenv currentProof
in
let dummyno = CicMkImplicit.new_meta metasenv [] in
handle_error (fun () ->
(match src with
| `Ast ast -> self#_loadTermAst ast
- | `Cic cic -> self#_loadTermCic cic
+ | `Cic (cic, metasenv) -> self#_loadTermCic cic metasenv
| `String s -> self#_loadTerm s);
self#setUri "check")