diff options
| author | Enrico Tassi | 2019-03-12 12:20:28 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-03-12 12:20:28 +0100 |
| commit | 3c0e9465029d7dcddff2c9a813cfd727a3ed4444 (patch) | |
| tree | b6e474f2b3051f196a4c6803f43b5bd4154f3fef /plugins/ltac | |
| parent | 591af507e606aef4bd97dc226567289b1a959cc1 (diff) | |
| parent | d9f86f9920efda1057b09d10d64764babe1dec44 (diff) | |
Merge PR #7819: Ho matching occ sel
Ack-by: gares
Ack-by: herbelin
Ack-by: mattam82
Ack-by: ppedrot
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacintern.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 2d833a2cde..e78d0f93a4 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -449,7 +449,7 @@ let evd_convertible env evd x y = unsolvable constraints remain, so we check that this unification does not introduce any new problem. *) let _, pbs = Evd.extract_all_conv_pbs evd in - let evd' = Evarconv.the_conv_x env x y evd in + let evd' = Evarconv.unify_delay env evd x y in let _, pbs' = Evd.extract_all_conv_pbs evd' in if evd' == evd || problem_inclusion pbs' pbs then Some evd' else None diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index a1e21aab04..543d4de0fe 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -557,7 +557,7 @@ let rec intern_atomic lf ist x = | _ -> false in let is_onconcl = match cl.concl_occs with - | AllOccurrences | NoOccurrences -> true + | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true | _ -> false in TacChange (None, diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 30f716d764..eac84f0543 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1766,7 +1766,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | _ -> false in let is_onconcl = match cl.concl_occs with - | AllOccurrences | NoOccurrences -> true + | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true | _ -> false in let c_interp patvars env sigma = |