added Match (partially) and sync with the count table

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

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 2d1c4d702f023c59b83439e69a62126d4cc83667..5abba5207e05e0a90febf538dc95a0dd551237e8 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -102,6 +102,22 @@ let eval_statement status mathviewer user_goal 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.Check (_,t) ->
             let metasenv = MatitaMisc.get_proof_metasenv status in
             let context = MatitaMisc.get_proof_context status in
@@ -109,8 +125,7 @@ let eval_statement status mathviewer user_goal s =
             let db = MatitaDb.instance () in
             let (_env,_metasenv,term,_graph) = 
               let interps = 
-                MatitaDisambiguator.disambiguate_term db context metasenv 
-                  aliases t 
+                MatitaDisambiguator.disambiguate_term db context metasenv aliases t 
               in
               match interps with 
               | [x] -> x