Merge PR #10059: Fixing bugs introduced in change_no_check

Reviewed-by: ppedrot

3 files changed, 12 insertions, 5 deletions

diff --git a/CHANGES.md b/CHANGES.md
index bcb73f8fd0..28ea84e4e3 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -15,6 +15,8 @@ Unreleased changes
 
 **Tactics**
 
+- New variant change_no_check of change (usable as a documented
+  replacement of convert_concl_no_check).
 
 **Tactic language**
 
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.