diff options
Diffstat (limited to 'tactics/rewrite.ml')
| -rw-r--r-- | tactics/rewrite.ml | 42 |
1 files changed, 25 insertions, 17 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index e8a7c0f6..74bb6d59 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -403,7 +403,7 @@ module TypeGlobal = struct let inverse env (evd,cstrs) car rel = - let evd, (sort,_) = Evarutil.new_type_evar env evd Evd.univ_flexible in + let evd, sort = Evarutil.new_Type ~rigid:Evd.univ_flexible env evd in app_poly_check env (evd,cstrs) coq_inverse [| car ; car; sort; rel |] end @@ -1505,7 +1505,7 @@ let assert_replacing id newt tac = let after, before = List.split_when (fun (n, b, t) -> Id.equal n id) ctx in let nc = match before with | [] -> assert false - | (id, b, _) :: rem -> insert_dependent env (id, b, newt) [] after @ rem + | (id, b, _) :: rem -> insert_dependent env (id, None, newt) [] after @ rem in let env' = Environ.reset_with_named_context (val_of_named_context nc) env in Proofview.Refine.refine ~unsafe:false begin fun sigma -> @@ -1521,12 +1521,13 @@ let assert_replacing id newt tac = let newfail n s = Proofview.tclZERO (Refiner.FailError (n, lazy s)) -let cl_rewrite_clause_newtac ?abs ?origsigma strat clause = +let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let open Proofview.Notations in let treat sigma res = match res with | None -> newfail 0 (str "Nothing to rewrite") - | Some None -> Proofview.tclUNIT () + | Some None -> if progress then newfail 0 (str"Failed to progress") + else Proofview.tclUNIT () | Some (Some res) -> let (undef, prf, newt) = res in let fold ev _ accu = if Evd.mem sigma ev then accu else ev :: accu in @@ -1593,21 +1594,25 @@ let tactic_init_setoid () = try init_setoid (); tclIDTAC with e when Errors.noncritical e -> tclFAIL 0 (str"Setoid library not loaded") -(** Setoid rewriting when called with "rewrite_strat" *) -let cl_rewrite_clause_strat strat clause = +let cl_rewrite_clause_strat progress strat clause = tclTHEN (tactic_init_setoid ()) - (fun gl -> - try Proofview.V82.of_tactic (cl_rewrite_clause_newtac strat clause) gl - with RewriteFailure e -> - errorlabstrm "" (str"setoid rewrite failed: " ++ e) - | Refiner.FailError (n, pp) -> - tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp) gl) + ((if progress then tclWEAK_PROGRESS else fun x -> x) + (fun gl -> + try Proofview.V82.of_tactic (cl_rewrite_clause_newtac ~progress strat clause) gl + with RewriteFailure e -> + errorlabstrm "" (str"setoid rewrite failed: " ++ e) + | Refiner.FailError (n, pp) -> + tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp) gl)) (** Setoid rewriting when called with "setoid_rewrite" *) let cl_rewrite_clause l left2right occs clause gl = let strat = rewrite_with left2right (general_rewrite_unif_flags ()) l occs in - cl_rewrite_clause_strat strat clause gl + cl_rewrite_clause_strat true strat clause gl +(** Setoid rewriting when called with "rewrite_strat" *) +let cl_rewrite_clause_strat strat clause = + cl_rewrite_clause_strat false strat clause + let apply_glob_constr c l2r occs = (); fun ({ state = () ; env = env } as input) -> let c sigma = let (sigma, c) = Pretyping.understand_tcc env sigma c in @@ -2013,7 +2018,8 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals gl = tclWEAK_PROGRESS (tclTHEN (Refiner.tclEVARS evd) - (Proofview.V82.of_tactic (cl_rewrite_clause_newtac ~abs:(Some abs) ~origsigma strat cl))) gl + (Proofview.V82.of_tactic + (cl_rewrite_clause_newtac ~progress:true ~abs:(Some abs) ~origsigma strat cl))) gl with RewriteFailure e -> tclFAIL 0 (str"setoid rewrite failed: " ++ e) gl @@ -2077,8 +2083,10 @@ let poly_proof getp gett env evm car rel = let setoid_reflexivity = setoid_proof "reflexive" (fun env evm car rel -> - tac_open (poly_proof PropGlobal.get_reflexive_proof TypeGlobal.get_reflexive_proof - env evm car rel) (fun c -> Proofview.V82.of_tactic (apply c))) + tac_open (poly_proof PropGlobal.get_reflexive_proof + TypeGlobal.get_reflexive_proof + env evm car rel) + (fun c -> tclCOMPLETE (Proofview.V82.of_tactic (apply c)))) (reflexivity_red true) let setoid_symmetry = |