Ast: Rename ECallTactic to ETacticConstructor.

This is a constructor, it's not 'calling' anything.

diff --git a/src/ast.ml b/src/ast.ml
index 1f67413..c3e530e 100644 (file)
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -45,7 +45,7 @@ and expr =
   | EGoalDefn of loc * goal
   | ETacticDefn of loc * tactic
   | ECallGoal of loc * id * expr list
-  | ECallTactic of loc * id * expr list
+  | ETacticConstructor of loc * id * expr list
   | EVar of loc * id
   | EList of loc * expr list
   | ESubsts of loc * substs
@@ -112,7 +112,7 @@ let rec to_constant env = function
      failwithf "%a: cannot use goal ‘%s’ in constant expression"
        string_loc loc name
 
-  | ECallTactic (loc, name, _) ->
+  | ETacticConstructor (loc, name, _) ->
      failwithf "%a: cannot use tactic ‘%s’ in constant expression"
        string_loc loc name
 
@@ -168,8 +168,8 @@ and expr_to_shell_string env = function
        string_loc loc name
 
   (* Tactics expand to the first parameter. *)
-  | ECallTactic (loc, _, []) -> Filename.quote ""
-  | ECallTactic (loc, _, (arg :: _)) -> expr_to_shell_string env arg
+  | ETacticConstructor (loc, _, []) -> Filename.quote ""
+  | ETacticConstructor (loc, _, (arg :: _)) -> expr_to_shell_string env arg
 
   | EGoalDefn (loc, _) ->
      failwithf "%a: cannot use goal in shell expansion"
@@ -252,7 +252,7 @@ and string_expr () = function
   | ECallGoal (loc, name, params) ->
      sprintf "%s (%s)"
        name (String.concat ", " (List.map (string_expr ()) params))
-  | ECallTactic (loc, name, params) ->
+  | ETacticConstructor (loc, name, params) ->
      sprintf "%s (%s)"
        name (String.concat ", " (List.map (string_expr ()) params))
   | EVar (loc, var) -> var

diff --git a/src/ast.mli b/src/ast.mli
index 1fee78e..b42294c 100644 (file)
--- a/src/ast.mli
+++ b/src/ast.mli
@@ -51,7 +51,7 @@ and expr =
   (** call goalname (params) etc. *)
   | ECallGoal of loc * id * expr list
   (** call *tactic (params) etc. *)
-  | ECallTactic of loc * id * expr list
+  | ETacticConstructor of loc * id * expr list
   (** variable, or goal call with no parameters *)
   | EVar of loc * id
   (** list *)

diff --git a/src/eval.ml b/src/eval.ml
index 770acf1..f00ce29 100644 (file)
--- a/src/eval.ml
+++ b/src/eval.ml
@@ -33,7 +33,7 @@ and evaluate_target env = function
      run_goal env loc name args goal
 
   (* Call a tactic. *)
-  | Ast.ECallTactic (loc, name, args) ->
+  | Ast.ETacticConstructor (loc, name, args) ->
      (* All parameters of tactics must be simple constant expressions
       * (strings, in future booleans, numbers, etc).
       *)
@@ -98,7 +98,7 @@ and run_goal env loc name args (params, patterns, deps, code) =
         let expr_of_substs s = Ast.ESubsts (Ast.noloc, s) in
         let expr_of_pattern = function
           | Ast.PTactic (loc, tactic, targs) ->
-             Ast.ECallTactic (loc, tactic, List.map expr_of_substs targs)
+             Ast.ETacticConstructor (loc, tactic, List.map expr_of_substs targs)
         in
         let pexprs = List.map expr_of_pattern patterns in
         let env = Ast.Env.add "@" (Ast.EList (Ast.noloc, pexprs)) env in
@@ -218,7 +218,7 @@ and run_tactic env loc tactic cargs =
      let targs = List.map (function Ast.CString s -> [Ast.SString s]) cargs in
      let p = Ast.PTactic (loc, tactic, targs) in
      if needs_rebuild env loc [] p then (
-       let t = Ast.ECallTactic (loc, tactic,
+       let t = Ast.ETacticConstructor (loc, tactic,
                                 List.map (fun c -> Ast.EConstant (loc, c))
                                   cargs) in
        failwithf "%a: don't know how to build %a"

diff --git a/src/parser.mly b/src/parser.mly
index 6cb48f7..347c072 100644 (file)
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -140,7 +140,7 @@ pattern_param:
 expr:
     | ID params  { Ast.ECallGoal ($loc, $1, $2) }
     | ID         { Ast.EVar ($loc, $1) }
-    | TACTIC params { Ast.ECallTactic ($loc, $1, $2) }
+    | TACTIC params { Ast.ETacticConstructor ($loc, $1, $2) }
     | STRING     { Ast.ESubsts ($loc, $1) }
     | LEFT_ARRAY barelist RIGHT_ARRAY { Ast.EList ($loc, $2) }
     ;