X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Feval.ml;h=5e271a79f9bd9d9af4c1ebe978f32a783e2fcab8;hb=2d5b3813df7f7db3abf3bcbfe2c6a657f463c5ee;hp=8657b2cedc8abeb8ecae322dd9796e36de635c90;hpb=f36210fd16a8e4e4d6ecdd8825bf8b8307943472;p=goals.git

diff --git a/src/eval.ml b/src/eval.ml
index 8657b2c..5e271a7 100644
--- 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