X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Fast.ml;h=c3b3969f6c3eb69c4ab96e70aec063941baf2d51;hb=2d5b3813df7f7db3abf3bcbfe2c6a657f463c5ee;hp=c3e530e64e5e483b4a18a986d35fb2896781db52;hpb=f36210fd16a8e4e4d6ecdd8825bf8b8307943472;p=goals.git

diff --git a/src/ast.ml b/src/ast.ml
index c3e530e..c3b3969 100644
--- 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