Skip to content

Instantly share code, notes, and snippets.

@johnbender johnbender/LibTactics.v
Last active Jan 10, 2017

Embed
What would you like to do?
Coq 8.6 and Software Foundations Fix
(*
The error while running `make` is:
File "./LibTactics.v", line 3238, characters 17-18:
Syntax error: ')' expected after [constr:lconstr] (in [tactic:tactic_arg]).
The fix to line 3238 is below.
*)
Ltac branch_tactic K N := (* Line 3237 *)
match constr:((K,N)) with (* (K, N) -> ((K, N)) *)
| (_,0) => fail 1
| (0,_) => fail 1
| (1,1) => idtac
| (1,_) => left
| (S ?K', S ?N') => right; branch_tactic K' N'
end.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.