+ | TacticAst.Hint _ ->
+ let s = MatitaMisc.get_proof_status status in
+ let l = List.map fst
+ (MetadataQuery.experimental_hint ~dbd:(MatitaDb.instance ()) s)
+ in
+ List.iter prerr_endline l;
+ prerr_endline "FINITA LA HINT"; assert false
+ | TacticAst.Check (_,t) ->
+ let metasenv = MatitaMisc.get_proof_metasenv status in
+ let context = MatitaMisc.get_proof_context status in
+ let aliases = MatitaMisc.get_proof_aliases status in
+ let db = MatitaDb.instance () in
+ let (_env,_metasenv,term,_graph) =
+ let interps =
+ MatitaDisambiguator.disambiguate_term db context metasenv
+ aliases t
+ in
+ match interps with
+ | [x] -> x
+ | _ -> assert false
+ in
+ let ty,_ =
+ CicTypeChecker.type_of_aux' metasenv context term
+ CicUniv.empty_ugraph
+ in
+ mathviewer # show_term (`Cic (ty,metasenv) );
+ [ status, "" ] , parsed_text_length