+ | 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;
+