From c45a64eab908d5309c8bb04b7c8f51734da3d1cc Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Fri, 3 Jan 2020 07:28:10 +0000 Subject: [PATCH] Revert "eval: Expand goal args before running the goal." This reverts commit 8509cad9b10205b7bec23eb59ba63e88c3d0fcb3. --- src/eval.ml | 17 ----------------- 1 file changed, 17 deletions(-) diff --git a/src/eval.ml b/src/eval.ml index 1b622b4..f00ce29 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -72,23 +72,6 @@ and run_goal env loc name args (params, patterns, deps, code) = Cmdline.debug "%a: running goal %s %a" Ast.string_loc loc name Ast.string_expr (Ast.EList (Ast.noloc, args)); - (* Expand any variables in the args first. *) - let rec expand = function - | Ast.EVar (loc, name) -> - let expr = Ast.getvar env loc name in - expand expr - | Ast.ETacticConstructor (loc, name, exprs) -> - Ast.ETacticConstructor (loc, name, List.map expand exprs) - | Ast.EList (loc, exprs) -> - Ast.EList (loc, List.map expand exprs) - | Ast.EGoalDefn _ - | Ast.ETacticDefn _ - | Ast.ECallGoal _ - | Ast.ESubsts _ - | Ast.EConstant _ as e -> e - in - let args = List.map expand args in - (* Create a new environment which maps the parameter names to * the args. *) -- 1.8.3.1