aboutsummaryrefslogtreecommitdiff
path: root/contrib/interface
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface')
-rw-r--r--contrib/interface/depends.ml2
-rw-r--r--contrib/interface/xlate.ml6
2 files changed, 4 insertions, 4 deletions
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index bf1cf5e7b2..203bc9e3dd 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -268,7 +268,7 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
igtal
acc)
| TacMatch (_, tac, tacexpr_mrl) -> failwith "depends_of_tacexpr of a Match not implemented yet"
- | TacMatchContext (_, _, tacexpr_mrl) -> failwith "depends_of_tacexpr of a Match Context not implemented yet"
+ | TacMatchGoal (_, _, tacexpr_mrl) -> failwith "depends_of_tacexpr of a Match Context not implemented yet"
| TacFun tacfa -> depends_of_tac_fun_ast tacfa acc
| TacArg tacarg -> depends_of_tac_arg tacarg acc
and depends_of_atomic_tacexpr atexpr acc = let depends_of_'constr_with_bindings = depends_of_'a_with_bindings depends_of_'constr in match atexpr with
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 716f6da3b7..e368ff637e 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -830,11 +830,11 @@ and xlate_tactic =
| [] -> assert false
| fst::others ->
CT_match_tac_rules(fst, others))
- | TacMatchContext (_,_,[]) | TacMatchContext (true,_,_) -> failwith ""
- | TacMatchContext (false,false,rule1::rules) ->
+ | TacMatchGoal (_,_,[]) | TacMatchGoal (true,_,_) -> failwith ""
+ | TacMatchGoal (false,false,rule1::rules) ->
CT_match_context(xlate_context_rule rule1,
List.map xlate_context_rule rules)
- | TacMatchContext (false,true,rule1::rules) ->
+ | TacMatchGoal (false,true,rule1::rules) ->
CT_match_context_reverse(xlate_context_rule rule1,
List.map xlate_context_rule rules)
| TacLetIn (false, l, t) ->