Commit c031da7d by Robbert Krebbers

### Tactic iSimplifyEq that substitutes Leibniz equalities that are in the proof mode context.

parent 7c4416b6
Pipeline #1591 passed with stage
 ... @@ -34,6 +34,11 @@ Tactic Notation "iTypeOf" constr(H) tactic(tac):= ... @@ -34,6 +34,11 @@ Tactic Notation "iTypeOf" constr(H) tactic(tac):= | Some (?p,?P) => tac p P | Some (?p,?P) => tac p P end. end. Ltac iMatchGoal tac := match goal with | |- context[ environments.Esnoc _ ?x ?P ] => tac x P end. (** * Start a proof *) (** * Start a proof *) Tactic Notation "iProof" := Tactic Notation "iProof" := lazymatch goal with lazymatch goal with ... @@ -789,6 +794,10 @@ Tactic Notation "iRewrite" open_constr(t) "in" constr(H) := ... @@ -789,6 +794,10 @@ Tactic Notation "iRewrite" open_constr(t) "in" constr(H) := Tactic Notation "iRewrite" "-" open_constr(t) "in" constr(H) := Tactic Notation "iRewrite" "-" open_constr(t) "in" constr(H) := iRewriteCore true t in H. iRewriteCore true t in H. Ltac iSimplifyEq := repeat ( iMatchGoal ltac:(fun H P => match P with (_ = _)%I => iDestruct H as %? end) || simplify_eq/=). (* Make sure that by and done solve trivial things in proof mode *) (* Make sure that by and done solve trivial things in proof mode *) Hint Extern 0 (of_envs _ ⊢ _) => by iPureIntro. Hint Extern 0 (of_envs _ ⊢ _) => by iPureIntro. Hint Extern 0 (of_envs _ ⊢ _) => iAssumption. Hint Extern 0 (of_envs _ ⊢ _) => iAssumption. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!