diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-04-14 15:18:11 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:59:00 +0200 |
| commit | 3869ffab2021b076054280f5eb4226ecda8caf75 (patch) | |
| tree | af6cae718a2b6e4acf72794cbe6677d253ede62f /pretyping | |
| parent | d2f36624980cdc169d0ebcc4c0be66446b4a8936 (diff) | |
- Add back some compatibility functions to avoid rewriting plugins.
- Fix in canonical structure inferce, we have to check that the heads
are convertible and keep universe information around.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 7 | ||||
| -rw-r--r-- | pretyping/evarconv.mli | 3 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 1 |
3 files changed, 6 insertions, 5 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index e24c18ae2..a92698566 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -147,7 +147,8 @@ let check_conv_record (t1,sk1) (t2,sk2) = let c' = subst_univs_level_constr subst c in let t' = subst_univs_level_constr subst t' in let bs' = List.map (subst_univs_level_constr subst) bs in - ctx',t',c',bs',(Stack.append_app_list params Stack.empty,params1), + let f, _ = decompose_app_vect t' in + ctx',(t2,f),c',bs',(Stack.append_app_list params Stack.empty,params1), (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1, (n,Stack.zip(t2,sk2)) @@ -668,7 +669,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty end -and conv_record trs env evd (ctx,t,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) = +and conv_record trs env evd (ctx,(h,h'),c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) = let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in if Reductionops.Stack.compare_shape ts ts1 then let (evd',ks,_,test) = @@ -697,7 +698,7 @@ and conv_record trs env evd (ctx,t,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n us2 us); (fun i -> evar_conv_x trs env i CONV c1 app); (fun i -> exact_ise_stack2 env i (evar_conv_x trs) ts ts1); - (fun i -> evar_conv_x trs env i CONV (substl ks t) t2)] + (fun i -> evar_conv_x trs env i CONV h h')] else UnifFailure(evd,(*dummy*)NotSameHead) and eta_constructor ts env evd ((ind, i), u) l1 csts1 (c, csts2) = diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index aa45b5ef1..500bb5430 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -43,7 +43,8 @@ val check_problems_are_solved : env -> evar_map -> unit (** Check if a canonical structure is applicable *) val check_conv_record : constr * types Stack.t -> constr * types Stack.t -> - Univ.universe_context_set * constr * constr * constr list * (constr Stack.t * constr Stack.t) * + Univ.universe_context_set * (constr * constr) + * constr * constr list * (constr Stack.t * constr Stack.t) * (constr Stack.t * types Stack.t) * (constr Stack.t * types Stack.t) * constr * (int * constr) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 18b96e765..8e65cc480 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -507,7 +507,6 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t = if Int.equal npars 0 then [] else try - let ty = evd_comb1 (Coercion.inh_coerce_to_prod loc env) evdref ty in let IndType (indf, args) = find_rectype env !evdref ty in let ((ind',u'),pars) = dest_ind_family indf in if eq_ind ind ind' then pars |