diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-17 15:23:55 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-26 22:08:51 +0200 |
| commit | 2c7fb44684b26d9c9aea0794b9f0d52088337477 (patch) | |
| tree | 76996152c1fa2868a0e7644fc09fc0a691f88417 /pretyping/unification.ml | |
| parent | e128900aee63c972d7977fd47e3fd21649b63409 (diff) | |
Fixes #7011 (Fix/CoFix were not considered in tactic unification).
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index f2f922fd5..b9c877753 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -838,6 +838,26 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e with ex when precatchable_exception ex -> reduce curenvnb pb opt substn cM cN) + | Fix ((ln1,i1),(lna1,tl1,bl1)), Fix ((ln2,i2),(_,tl2,bl2)) when + Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 -> + (try + let opt' = {opt with at_top = true; with_types = false} in + let curenvnb' = Array.fold_right2 (fun na t -> push (na,t)) lna1 tl1 curenvnb in + Array.fold_left2 (unirec_rec curenvnb' CONV opt') + (Array.fold_left2 (unirec_rec curenvnb CONV opt') substn tl1 tl2) bl1 bl2 + with ex when precatchable_exception ex -> + reduce curenvnb pb opt substn cM cN) + + | CoFix (i1,(lna1,tl1,bl1)), CoFix (i2,(_,tl2,bl2)) when + Int.equal i1 i2 -> + (try + let opt' = {opt with at_top = true; with_types = false} in + let curenvnb' = Array.fold_right2 (fun na t -> push (na,t)) lna1 tl1 curenvnb in + Array.fold_left2 (unirec_rec curenvnb' CONV opt') + (Array.fold_left2 (unirec_rec curenvnb CONV opt') substn tl1 tl2) bl1 bl2 + with ex when precatchable_exception ex -> + reduce curenvnb pb opt substn cM cN) + | App (f1,l1), _ when (isMeta sigma f1 && use_metas_pattern_unification sigma flags nb l1 || use_evars_pattern_unification flags && isAllowedEvar sigma flags f1) -> |