diff options
| -rw-r--r-- | tactics/rewrite.ml | 3 | ||||
| -rw-r--r-- | tactics/rewrite.mli | 30 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3291.v (renamed from test-suite/bugs/opened/3291.v) | 3 |
3 files changed, 33 insertions, 3 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index aa0152d35a..7309e22759 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -295,7 +295,8 @@ end) = struct let ap = is_Prop ta and bp = is_Prop tb in if ap && bp then app_poly env evd impl [| a; b |], unfold_impl else if ap then (* Domain in Prop, CoDomain in Type *) - (evd, mkProd (Anonymous, a, b)), (fun x -> x) + (app_poly env evd arrow [| a; b |]), unfold_impl + (* (evd, mkProd (Anonymous, a, b)), (fun x -> x) *) else if bp then (* Dummy forall *) (app_poly env evd coq_all [| a; mkLambda (Anonymous, a, b) |]), unfold_forall else (* None in Prop, use arrow *) diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli index 0f155c8bb8..81f1175c4c 100644 --- a/tactics/rewrite.mli +++ b/tactics/rewrite.mli @@ -28,7 +28,24 @@ type ('constr,'redexpr) strategy_ast = | StratEval of 'redexpr | StratFold of 'constr -type strategy +type rewrite_proof = + | RewPrf of constr * constr + | RewCast of cast_kind + +type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *) + +type rewrite_result_info = { + rew_car : constr; + rew_from : constr; + rew_to : constr; + rew_prf : rewrite_proof; + rew_evars : evars; +} + +type rewrite_result = rewrite_result_info option + +type strategy = Environ.env -> Id.t list -> constr -> types -> + (bool (* prop *) * constr option) -> evars -> rewrite_result option val strategy_of_ast : (glob_constr_and_expr, raw_red_expr) strategy_ast -> strategy @@ -78,3 +95,14 @@ val setoid_symmetry_in : Id.t -> unit Proofview.tactic val setoid_reflexivity : unit Proofview.tactic val setoid_transitivity : constr option -> unit Proofview.tactic + + +val apply_strategy : + strategy -> + Environ.env -> + Names.Id.t list -> + Term.constr -> + bool * Term.constr -> + evars -> + (rewrite_proof * evars * Term.constr * Term.constr * Term.constr) + option option diff --git a/test-suite/bugs/opened/3291.v b/test-suite/bugs/closed/3291.v index 4e1c2630e3..4ea748c0fb 100644 --- a/test-suite/bugs/opened/3291.v +++ b/test-suite/bugs/closed/3291.v @@ -4,5 +4,6 @@ Definition segv : forall x, (x = 0%nat) -> (forall (y : nat), (y < x)%nat -> nat intros x eq. assert (H : forall y, (y < x)%nat = (y < 0)%nat). rewrite -> eq. auto. -Fail Timeout 1 setoid_rewrite <- H. (* The command has indeed failed with message: +Set Typeclasses Debug. +Fail setoid_rewrite <- H. (* The command has indeed failed with message: => Stack overflow. *) |