Skip to content

LibHyps 2.0.2

Compare
Choose a tag to compare
@Matafou Matafou released this 30 Jun 14:33
· 27 commits to master since this release
  • bug fixes
  • Adding the following options to especialize:
especialize H at *. (* create a subgoal for each (dependent) premise of H. Cf "exploit" from CompCert. *)
especialize H at 2,3,4 (* up to 7 premise number *)
especialize H until 3 (* create goals for the n first (dependent) premises of H. *)

Many thanks to Sylvain Boulmé for the suggestions.