diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/coercion.ml | 6 | ||||
| -rw-r--r-- | pretyping/coercion.mli | 4 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 9 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 8 |
4 files changed, 20 insertions, 7 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index a8af39bc71..4ff60b41f2 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -43,6 +43,10 @@ module type S = sig val inh_coerce_to_base : loc -> env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment + (* [inh_coerce_to_prod env isevars t] coerces [t] to a product type *) + val inh_coerce_to_prod : loc -> + env -> evar_defs -> type_constraint_type -> evar_defs * type_constraint_type + (* [inh_conv_coerce_to loc env evd j t] coerces [j] to an object of type [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and [j.uj_type] are convertible; it fails if no coercion is applicable *) @@ -160,6 +164,8 @@ module Default = struct let inh_coerce_to_base loc env evd j = (evd, j) + let inh_coerce_to_prod loc env evd t = (evd, t) + let inh_coerce_to_fail env evd rigidonly v t c1 = if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t) then diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index 00735d8746..ff33d679df 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -39,6 +39,10 @@ module type S = sig type its base type (the notion depends on the coercion system) *) val inh_coerce_to_base : loc -> env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment + + (* [inh_coerce_to_prod env isevars t] coerces [t] to a product type *) + val inh_coerce_to_prod : loc -> + env -> evar_defs -> type_constraint_type -> evar_defs * type_constraint_type (* [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 12826851f2..778fb3f0ea 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1183,11 +1183,12 @@ let split_tycon loc env evd tycon = if cur = 0 then let evd', (x, dom, rng) = real_split c in evd, (Anonymous, - Some (Some (init, 0), dom), - Some (Some (init, 0), rng)) + Some (None, dom), + Some (None, rng)) else - evd, (Anonymous, None, Some (Some (init, pred cur), c))) - + evd, (Anonymous, None, + Some (if cur = 1 then None,c else Some (init, pred cur), c))) + let valcon_of_tycon x = match x with | Some (None, t) -> Some t diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 11d3b37104..17c7efb457 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -356,7 +356,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) ctxtv vdef in evar_type_fixpoint loc env evdref names ftys vdefj; - let fixj = match fixkind with + let ftys = Array.map (nf_evar (evars_of !evdref)) ftys in + let fdefs = Array.map (fun x -> nf_evar (evars_of !evdref) (j_val x)) vdefj in + let fixj = match fixkind with | RFix (vn,i) -> (* First, let's find the guard indexes. *) (* If recursive argument was not given by user, we try all args. @@ -370,11 +372,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct | None -> list_map_i (fun i _ -> i) 0 ctxtv.(i)) vn) in - let fixdecls = (names,ftys,Array.map j_val vdefj) in + let fixdecls = (names,ftys,fdefs) in let indexes = search_guard loc env possible_indexes fixdecls in make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | RCoFix i -> - let cofix = (i,(names,ftys,Array.map j_val vdefj)) in + let cofix = (i,(names,ftys,fdefs)) in (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e); make_judge (mkCoFix cofix) ftys.(i) in inh_conv_coerce_to_tycon loc env evdref fixj tycon |