diff options
| author | Pierre-Marie Pédrot | 2019-05-05 18:31:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-05 18:31:19 +0200 |
| commit | 6ff10c569c1684927d4cb866a159fe6f54e55abe (patch) | |
| tree | 3fef486e92d07f900df79a2a465fe15c8afcb77c /tactics | |
| parent | 383991b5c1e9014229f2ca7124f10e6a2e995194 (diff) | |
| parent | a0cfcc318919b315b142abab7604f04e8dd6420f (diff) | |
Merge PR #10059: Fixing bugs introduced in change_no_check
Reviewed-by: ppedrot
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 4 |
1 files changed, 2 insertions, 2 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 = |