diff options
| author | Maxime Dénès | 2018-03-10 10:03:50 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-10 10:03:50 +0100 |
| commit | 93a1c4786c9b17efdda025f754ad97376d61a9ba (patch) | |
| tree | 9ffa30a21f0d5b80aaeae66955e652f185929498 /pretyping/cases.ml | |
| parent | 5f989f48eaaf5e13568fce9849f40bc554ca0166 (diff) | |
| parent | 4af41a12a0e7e6b17d25a71568641bd03d5e1f94 (diff) | |
Merge PR #6831: [located] More work towards using CAst.t
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 10e2592094..a5b7a9e6f0 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -347,7 +347,7 @@ let unify_tomatch_with_patterns evdref env loc typ pats realnames = let find_tomatch_tycon evdref env loc = function (* Try if some 'in I ...' is present and can be used as a constraint *) - | Some (_,(ind,realnal)) -> + | Some {CAst.v=(ind,realnal)} -> mk_tycon (inductive_template evdref env loc ind),Some (List.rev realnal) | None -> empty_tycon,None @@ -1565,7 +1565,7 @@ substituer après par les initiaux *) * and linearizing the _ patterns. * Syntactic correctness has already been done in constrintern *) let matx_of_eqns env eqns = - let build_eqn (loc,(ids,initial_lpat,initial_rhs)) = + let build_eqn {CAst.loc;v=(ids,initial_lpat,initial_rhs)} = let avoid = ids_of_named_context_val (named_context_val env) in let avoid = List.fold_left (fun accu id -> Id.Set.add id accu) avoid ids in let rhs = @@ -1883,8 +1883,8 @@ let extract_arity_signature ?(dolift=true) env0 lvar tomatchl tmsign = | None -> let sign = match bo with | None -> [LocalAssum (na, lift n typ)] | Some b -> [LocalDef (na, lift n b, lift n typ)] in sign,sign - | Some (loc,_) -> - user_err ?loc + | Some {CAst.loc} -> + user_err ?loc (str"Unexpected type annotation for a term of non inductive type.")) | IsInd (term,IndType(indf,realargs),_) -> let indf' = if dolift then lift_inductive_family n indf else indf in @@ -1894,7 +1894,7 @@ let extract_arity_signature ?(dolift=true) env0 lvar tomatchl tmsign = let arsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) arsign in let realnal, realnal' = match t with - | Some (loc,(ind',realnal)) -> + | Some {CAst.loc;v=(ind',realnal)} -> if not (eq_ind ind ind') then user_err ?loc (str "Wrong inductive type."); if not (Int.equal nrealargs_ctxt (List.length realnal)) then |