X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;ds=sidebyside;f=src%2Feval.ml;h=af5721348dcb8ec40bb3cbacc4739bfa8c26efb1;hb=7f776dee39a35732964a30091e55aa795169bca5;hp=46455f7a21aa3eb699201937727b2d2719c0ab69;hpb=c261da4d0efea4d86131abbbc2912edfa863995e;p=goals.git

diff --git a/src/eval.ml b/src/eval.ml
index 46455f7..af57213 100644
--- a/src/eval.ml
+++ b/src/eval.ml
@@ -85,8 +85,6 @@ and run_goal env loc name args (params, patterns, deps, code) =
         let expr_of_pattern = function
           | Ast.PTactic (loc, tactic, targs) ->
              Ast.ETactic (loc, tactic, List.map expr_of_substs targs)
-          | Ast.PVar (loc, name) ->
-             Ast.EVar (loc, name)
         in
         let pexprs = List.map expr_of_pattern patterns in
         let env = Ast.Env.add "@" (Ast.EList (Ast.noloc, pexprs)) env in
@@ -131,7 +129,6 @@ and needs_rebuild env loc deps pattern =
      assert (List.length targs = 1);
      let targ = List.hd targs in
      not (Sys.file_exists targ)
-  | Ast.PVar _ -> assert false (* XXX not implemented *)
 
 (* Find the goal which matches the given tactic and run it.
  * cargs is a list of parameters (all constants).
@@ -195,7 +192,6 @@ and run_tactic env loc tactic cargs =
  *)
 and matching_pattern env loc tactic cargs pattern params =
   match pattern with
-  | Ast.PVar (loc, name) -> assert false (* TODO! *)
   | Ast.PTactic (loc, ttactic, targs)
        when tactic <> ttactic ||
             List.length cargs <> List.length targs ->