diff options
| author | Emilio Jesus Gallego Arias | 2017-01-16 13:22:42 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-04-24 23:58:23 +0200 |
| commit | be83b52cf50ed4c596e40cfd52da03258a7a4a18 (patch) | |
| tree | 92e1e62378d2274751ab46673e2ee56fe4f65999 /pretyping/detyping.ml | |
| parent | ad3aab9415b98a247a6cbce05752632c3c42391c (diff) | |
[location] Move Glob_term.predicate_pattern to located.
We continue the uniformization pass. No big news here, trying to be
minimally invasive.
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index eef6d34acb..f3018ac64b 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -380,7 +380,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = | _ -> Anonymous, typ in let aliastyp = if List.for_all (Name.equal Anonymous) nl then None - else Some (dl,indsp,nl) in + else Some (dl,(indsp,nl)) in n, aliastyp, Some typ in let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in @@ -844,9 +844,9 @@ let rec subst_glob_constr subst raw = let a' = subst_glob_constr subst a in let (n,topt) = x in let topt' = Option.smartmap - (fun (loc,(sp,i),y as t) -> + (fun ((loc,((sp,i),y) as t)) -> let sp' = subst_mind subst sp in - if sp == sp' then t else (loc,(sp',i),y)) topt in + if sp == sp' then t else (loc,((sp',i),y))) topt in if a == a' && topt == topt' then y else (a',(n,topt'))) rl and branches' = List.smartmap (fun (loc,idl,cpl,r as branch) -> @@ -919,4 +919,4 @@ let simple_cases_matrix_of_branches ind brs = let return_type_of_predicate ind nrealargs_tags pred = let nal,p = it_destRLambda_or_LetIn_names (nrealargs_tags@[false]) pred in - (List.hd nal, Some (Loc.ghost, ind, List.tl nal)), Some p + (List.hd nal, Some (Loc.tag (ind, List.tl nal))), Some p |