Simplify Constructor -> Ctor.

diff --git a/src/ast.ml b/src/ast.ml
index c3e530e..c3b3969 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
-  | ETacticConstructor of loc * id * expr list
+  | ETacticCtor 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
 
-  | ETacticConstructor (loc, name, _) ->
+  | ETacticCtor (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. *)
-  | ETacticConstructor (loc, _, []) -> Filename.quote ""
-  | ETacticConstructor (loc, _, (arg :: _)) -> expr_to_shell_string env arg
+  | ETacticCtor (loc, _, []) -> Filename.quote ""
+  | ETacticCtor (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))
-  | ETacticConstructor (loc, name, params) ->
+  | ETacticCtor (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 406a829..e47ddc3 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. *)
-  | ETacticConstructor of loc * id * expr list
+  | ETacticCtor 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 8657b2c..5e271a7 100644 (file)
--- a/src/eval.ml
+++ b/src/eval.ml
@@ -37,7 +37,7 @@ let rec to_constant env = function
      failwithf "%a: cannot use goal ‘%s’ in constant expression"
        Ast.string_loc loc name
 
-  | ETacticConstructor (loc, name, _) ->
+  | ETacticCtor (loc, name, _) ->
      failwithf "%a: cannot use tactic ‘%s’ in constant expression"
        Ast.string_loc loc name
 
@@ -93,8 +93,8 @@ and expr_to_shell_string env = function
        Ast.string_loc loc name
 
   (* Tactics expand to the first parameter. *)
-  | ETacticConstructor (loc, _, []) -> Filename.quote ""
-  | ETacticConstructor (loc, _, (arg :: _)) -> expr_to_shell_string env arg
+  | ETacticCtor (loc, _, []) -> Filename.quote ""
+  | ETacticCtor (loc, _, (arg :: _)) -> expr_to_shell_string env arg
 
   | EGoalDefn (loc, _) ->
      failwithf "%a: cannot use goal in shell expansion"
@@ -116,8 +116,8 @@ let rec evaluate_goal_arg env = function
   | EList (loc, exprs) ->
      Ast.EList (loc, List.map (evaluate_goal_arg env) exprs)
 
-  | ETacticConstructor (loc, name, exprs) ->
-     Ast.ETacticConstructor (loc, name, List.map (evaluate_goal_arg env) exprs)
+  | ETacticCtor (loc, name, exprs) ->
+     Ast.ETacticCtor (loc, name, List.map (evaluate_goal_arg env) exprs)
 
   | ECallGoal (loc, name, _) ->
      (* Goals don't return anything so they cannot be used in

diff --git a/src/parser.mly b/src/parser.mly
index 347c072..db70924 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.ETacticConstructor ($loc, $1, $2) }
+    | TACTIC params { Ast.ETacticCtor ($loc, $1, $2) }
     | STRING     { Ast.ESubsts ($loc, $1) }
     | LEFT_ARRAY barelist RIGHT_ARRAY { Ast.EList ($loc, $2) }
     ;

diff --git a/src/run.ml b/src/run.ml
index a0bb592..7d48a7e 100644 (file)
--- a/src/run.ml
+++ b/src/run.ml
@@ -33,7 +33,7 @@ and run_target env = function
      run_goal env loc name args goal
 
   (* Call a tactic. *)
-  | Ast.ETacticConstructor (loc, name, args) ->
+  | Ast.ETacticCtor (loc, name, args) ->
      (* All parameters of tactics must be simple constant expressions
       * (strings, in future booleans, numbers, etc).
       *)
@@ -108,7 +108,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.ETacticConstructor (loc, tactic, List.map expr_of_substs targs)
+             Ast.ETacticCtor (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
@@ -227,7 +227,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.ETacticConstructor (loc, tactic,
+       let t = Ast.ETacticCtor (loc, tactic,
                                 List.map (fun c -> Ast.EConstant (loc, c))
                                   cargs) in
        failwithf "%a: don't know how to build %a"