!(Lazy.force basedir));
Quiet
| TacticAst.Command (TacticAst.Check term) ->
- let (_, _, term,ugraph) =
+ let (_, metasenv, term,ugraph) =
MatitaCicMisc.disambiguate ~disambiguator ~currentProof term
in
- let (context, metasenv) =
+ let (context, _) =
MatitaCicMisc.get_context_and_metasenv currentProof
in
(* this is the Eval Compute
(* TASSI: here ugraph1 is unused.... FIXME *)
let expr = Cic.Cast (term, ty) in
(match mathViewer with
- | Some v -> v#checkTerm (`Cic expr)
+ | Some v -> v#checkTerm (`Cic (expr, metasenv))
| _ -> ());
Quiet
| TacticAst.Command (TacticAst.Search_pat (search_kind, pat)) ->