diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-18 10:18:00 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-18 10:26:21 +0100 |
commit | 2e3ae20fe1ed3d7238286720c302bc892505caae (patch) | |
tree | 74fbaa4ee461bb19b1a349c43c3d2d82dc9005a4 /pretyping/find_subterm.ml | |
parent | 8d26a1d9a3846c6cbe92a9b2f17ffac6fd7d48f5 (diff) |
Fixing a little bug with nested but convertible occurrences in "destruct at".
Diffstat (limited to 'pretyping/find_subterm.ml')
-rw-r--r-- | pretyping/find_subterm.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index 30233cdf9..28e52856c 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -110,7 +110,13 @@ let replace_term_occ_gen_modulo occs like_first test bywhat cl occ t = try let subst = test.match_fun test.testing_state t in if Locusops.is_selected !pos occs then - (add_subst t subst; incr pos; + (if !nested then begin + (* in case it is nested but not later detected as unconvertible, + as when matching "id _" in "id (id 0)" *) + let lastpos = Option.get test.last_found in + raise (SubtermUnificationError (!nested,((cl,!pos),t),lastpos,None)) + end; + add_subst t subst; incr pos; (* Check nested matching subterms *) nested := true; ignore (subst_below k t); nested := false; (* Do the effective substitution *) |