diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 41 | ||||
| -rw-r--r-- | pretyping/rawterm.ml | 2 | ||||
| -rw-r--r-- | pretyping/rawterm.mli | 2 |
4 files changed, 32 insertions, 15 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index a815e5d2f8..edbbbb3294 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -421,7 +421,7 @@ and detype_fix isgoal avoid env (vn,_ as nvn) (names,tys,bodies) = let v = array_map3 (fun c t i -> share_names isgoal (i+1) [] def_avoid def_env c (lift n t)) bodies tys vn in - RRec(dl,RFix (Array.map (fun i -> i, RStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi), + RRec(dl,RFix (Array.map (fun i -> Some i, RStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi), Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index f48ec74624..64ea0bbb88 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -329,18 +329,35 @@ module Pretyping_F (Coercion : Coercion.S) = struct { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt; uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) ctxtv vdef in - evar_type_fixpoint loc env isevars names ftys vdefj; - let fixj = - match fixkind with - | RFix (vn,i) -> - let fix = ((Array.map fst vn, i),(names,ftys,Array.map j_val vdefj)) in - (try check_fix env fix with e -> Stdpp.raise_with_loc loc e); - make_judge (mkFix fix) ftys.(i) - | RCoFix i -> - let cofix = (i,(names,ftys,Array.map j_val vdefj)) 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 isevars fixj tycon + evar_type_fixpoint loc env isevars names ftys vdefj; + let fixj = match fixkind with + | RFix (vn,i) -> + let guard_indexes = Array.mapi + (fun i (n,_) -> match n with + | Some n -> n + | None -> + (* Recursive argument was not given by the user : We + check that there is only one inductive argument *) + let ctx = ctxtv.(i) in + let isIndApp t = + isInd (fst (decompose_app (strip_head_cast t))) in + (* This could be more precise (e.g. do some delta) *) + let lb = List.rev_map (fun (_,_,t) -> isIndApp t) ctx in + try (list_unique_index true lb) - 1 + with Not_found -> + Util.user_err_loc + (loc,"pretype", + Pp.str "cannot guess decreasing argument of fix")) + vn + in + let fix = ((guard_indexes, i),(names,ftys,Array.map j_val vdefj)) in + (try check_fix env fix with e -> Stdpp.raise_with_loc loc e); + make_judge (mkFix fix) ftys.(i) + | RCoFix i -> + let cofix = (i,(names,ftys,Array.map j_val vdefj)) 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 isevars fixj tycon | RSort (loc,s) -> inh_conv_coerce_to_tycon loc env isevars (pretype_sort s) tycon diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index 1c59004175..36edf519bd 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -73,7 +73,7 @@ and rawdecl = name * rawconstr option * rawconstr and fix_recursion_order = RStructRec | RWfRec of rawconstr -and fix_kind = RFix of ((int * fix_recursion_order) array * int) | RCoFix of int +and fix_kind = RFix of ((int option * fix_recursion_order) array * int) | RCoFix of int let cases_predicate_names tml = List.flatten (List.map (function diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index cbd215d85e..8ef0cb9397 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -70,7 +70,7 @@ and rawdecl = name * rawconstr option * rawconstr and fix_recursion_order = RStructRec | RWfRec of rawconstr -and fix_kind = RFix of ((int * fix_recursion_order) array * int) | RCoFix of int +and fix_kind = RFix of ((int option * fix_recursion_order) array * int) | RCoFix of int val cases_predicate_names : (rawconstr * (name * (loc * inductive * name list) option)) list -> name list |