Commit f01228f2 authored by Ralf Jung's avatar Ralf Jung
Browse files

make solve_ne slightly more robust

parent 35520fdf
......@@ -21,7 +21,7 @@ Tactic Notation "cofe_subst" :=
| H:@dist ?A ?d ?n _ ?x |- _ => symmetry in H;setoid_subst_aux (@dist A d n) x
Tactic Notation "solve_ne" := move=>n; solve_proper.
Tactic Notation "solve_ne" := intros; solve_proper.
Record chain (A : Type) `{Dist A} := {
chain_car :> nat A;
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment