+ | 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.Match (_,term) ->
+ let dbd = MatitaDb.instance () in
+ 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 (_env,_metasenv,term,_graph) =
+ let interps =
+ MatitaDisambiguator.disambiguate_term dbd context metasenv aliases term
+ in
+ match interps with
+ | [x] -> x
+ | _ -> assert false
+ in
+ List.iter prerr_endline (MetadataQuery.match_term ~dbd:dbd term);
+ assert false;
+ | TacticAst.Instance (_,term) ->
+ let dbd = MatitaDb.instance () in
+ 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 (_env,_metasenv,term,_graph) =
+ let interps =
+ MatitaDisambiguator.disambiguate_term dbd context metasenv aliases term
+ in
+ match interps with
+ | [x] -> x
+ | _ -> assert false
+ in
+ List.iter prerr_endline (MetadataQuery.instance ~dbd term);
+ 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