| 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
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
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"
| 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