added instance

[helm.git] / helm / matita / matitaScript.ml

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 5abba5207e05e0a90febf538dc95a0dd551237e8..c64653c798bde6e90382880bd5070e060657e260 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -117,7 +117,22 @@ let eval_statement status mathviewer user_goal s =
         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