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