diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/unification.ml | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 24e06007e9..123f9b8cd3 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -554,6 +554,19 @@ let isAllowedEvar flags c = match kind_of_term c with | Evar (evk,_) -> not (Evar.Set.mem evk flags.frozen_evars) | _ -> false + +let subst_defined_metas_evars (bl,el) c = + let rec substrec c = match kind_of_term c with + | Meta i -> + let select (j,_,_) = Int.equal i j in + substrec (pi2 (List.find select bl)) + | Evar (evk,args) -> + let select (_,(evk',args'),_) = Evar.equal evk evk' && Array.equal Constr.equal args args' in + (try substrec (pi3 (List.find select el)) + with Not_found -> map_constr substrec c) + | _ -> map_constr substrec c + in try Some (substrec c) with Not_found -> None + let check_compatibility env pbty flags (sigma,metasubst,evarsubst) tyM tyN = match subst_defined_metas_evars (metasubst,[]) tyM with | None -> sigma |