Tactics: fixing "change_no_check in".

(Merge of the initial version with #9983 was broken)
coq · May 3, 2019 · a0cfcc3 · a0cfcc3
1 parent ee1e368
commit a0cfcc3
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 5 deletions.
diff --git 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
@@ -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.