diff options
| author | Hugo Herbelin | 2019-05-03 21:27:19 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-05-03 21:33:41 +0200 |
| commit | a0cfcc318919b315b142abab7604f04e8dd6420f (patch) | |
| tree | e877cb18648e465c0e7eebb92f5d8345c03facd0 | |
| parent | ee1e3685100a98925a272de31ea1c6147e24512f (diff) | |
Tactics: fixing "change_no_check in".
(Merge of the initial version with #9983 was broken)
| -rw-r--r-- | tactics/tactics.ml | 4 | ||||
| -rw-r--r-- | test-suite/success/change.v | 11 |
2 files changed, 10 insertions, 5 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 35b3b38298..5e8869f9b0 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -833,7 +833,7 @@ let change_in_hyp ?(check=true) occl t id = (* FIXME: we set the [check] flag only to reorder hypotheses in case of introduction of dependencies in new variables. We should separate this check from the conversion function. *) - e_change_in_hyp ~check:true (fun x -> change_on_subterm check Reduction.CONV x t occl) id + e_change_in_hyp ~check (fun x -> change_on_subterm check Reduction.CONV x t occl) id let concrete_clause_of enum_hyps cl = match cl.onhyps with | None -> @@ -855,7 +855,7 @@ let change ?(check=true) chg c cls = let redfun deep env sigma t = change_on_subterm check Reduction.CONV deep c occl env sigma t in (redfun, id, where) in - e_change_in_hyps ~check:true f hyps + e_change_in_hyps ~check f hyps end let change_concl t = diff --git a/test-suite/success/change.v b/test-suite/success/change.v index 5a8f735151..2f676cf9ad 100644 --- a/test-suite/success/change.v +++ b/test-suite/success/change.v @@ -71,8 +71,13 @@ Qed. (* Mini-check that no_check does not check *) -Goal False. -change_no_check True. -exact I. +Goal True -> False. +intro H. +change_no_check nat. +apply S. +change_no_check nat with bool. +change_no_check nat in H. +change_no_check nat with (bool->bool) in H. +exact (H true). Fail Qed. Abort. |