Skip to content

Instantly share code, notes, and snippets.

@johnbender

johnbender/LibTactics.v

Last active January 10, 2017 07:04
Show Gist options
  • Save johnbender/97295ae72d52a10756286c6c748b2cdc to your computer and use it in GitHub Desktop.
Save johnbender/97295ae72d52a10756286c6c748b2cdc to your computer and use it in GitHub Desktop.
Download ZIP
Coq 8.6 and Software Foundations Fix
Raw
LibTactics.v
(*
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