diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/interface/depends.ml | 2 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 6 | ||||
| -rw-r--r-- | contrib/setoid_ring/Ring_theory.v | 2 |
3 files changed, 5 insertions, 5 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) -> diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v index 29feab5cab..531ab3ca5e 100644 --- a/contrib/setoid_ring/Ring_theory.v +++ b/contrib/setoid_ring/Ring_theory.v @@ -494,7 +494,7 @@ Qed. Proof. intros;mrewrite. Qed. Lemma ARdistr_r : forall x y z, z * (x + y) == z*x + z*y. - Proof. + Proof. intros;mrewrite. repeat rewrite (ARth.(ARmul_comm) z);sreflexivity. Qed. |