diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-12-19 01:30:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:44 +0100 |
| commit | aaf75678a13d9c26341e762ab8e56b957cf4c771 (patch) | |
| tree | 8e7042f6630053f7c130957fde011929d45fde13 /pretyping/unification.ml | |
| parent | 594ac9654164e377e8598894019cc4445509d570 (diff) | |
Dedicated datatype for aliases in Evarsolve.
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 318a0b2cd..336b3348c 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -206,7 +206,9 @@ let solve_pattern_eqn_array (env,nb) f l c (sigma,metasubst,evarsubst : subst0) let pb = (Conv,TypeNotProcessed) in if noccur_between sigma 1 nb c then sigma,(k,lift (-nb) c,pb)::metasubst,evarsubst - else error_cannot_unify_local env sigma (applist (f, l),c,c) + else + let l = List.map of_alias l in + error_cannot_unify_local env sigma (applist (f, l),c,c) | Evar ev -> let env' = pop_rel_context nb env in let sigma,c = pose_all_metas_as_evars env' sigma c in |