Commit f736bb46 authored by Michael Sammler's avatar Michael Sammler
Browse files

fix build

parent df893f20
Pipeline #57416 canceled with stage
in 1 minute and 33 seconds
......@@ -96,7 +96,7 @@ Ltac normalize_and_simpl_goal_step :=
| _ = _ =>
check_injection_tac;
let Hi := fresh "Hi" in move => Hi; injection Hi; clear Hi
| _ => check_hyp_not_exists P; intros ?; subst
| _ => assert_is_not_trivial P; intros ?; subst
| _ => move => _
end
end]
......
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