- (match ty' with
- | None -> (* just we proved P done *)
- (
- try
- assert_tac ty None status goal (bydone wrappedjust status)
- with
- | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
- | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")
- )
- | Some ty' -> (* just we proved P that is equivalent to P' done *)
- (
- try
- assert_tac ty' None status goal (block_tac [change_tac ~where:("",0,(None,[],Some
- Ast.UserInput))
- ~with_what:ty; bydone wrappedjust]
- status )
- with
- | FirstTypeWrong -> fail (lazy "The second proposition is not the same as the conclusion")
- | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")
- )
- )
+ assert_tac ty None status goal (block_tac [clear_volatile_params_tac; add_parameter_tac
+ "volatile_context" "beta_rewrite"] status)