X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaScript.ml;h=c64653c798bde6e90382880bd5070e060657e260;hb=195cc290eb6e6dc5d5dc9b34bddef083c5c5b0b8;hp=5abba5207e05e0a90febf538dc95a0dd551237e8;hpb=5e4659bb1bd31c92fa7c82fe502aabb1dc9dbb75;p=helm.git

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 5abba5207..c64653c79 100644
--- 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