From ee1e3685100a98925a272de31ea1c6147e24512f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 30 Apr 2019 12:15:44 +0200
Subject: Updating CHANGES.

---
 CHANGES.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/CHANGES.md b/CHANGES.md
index 5ca16ae1fe..f6806de9d0 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**
 
-- 
cgit v1.2.3


From a0cfcc318919b315b142abab7604f04e8dd6420f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 3 May 2019 21:27:19 +0200
Subject: Tactics: fixing "change_no_check in".

(Merge of the initial version with #9983 was broken)
---
 tactics/tactics.ml          |  4 ++--
 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.
-- 
cgit v1.2.3