diff options
| author | Hugo Herbelin | 2020-04-27 14:39:56 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-10 22:13:59 +0200 |
| commit | 2cf0287c9c863d7969fb5d4e85b7ca538dd103c2 (patch) | |
| tree | 0dfa98a20514443017dcd81d165cdcb494e5743f /pretyping/detyping.ml | |
| parent | 03d55f990bb7a2c4f5c1fefa408b94a8a93e8d05 (diff) | |
Adding and using locations on identifiers in constr_expr where they were missing.
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 7fcb0795bd..503035c6c3 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -788,10 +788,10 @@ and detype_r d flags avoid env sigma t = let l = Evd.evar_instance_array bound_to_itself_or_letin (Evd.find sigma evk) cl in let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> match EConstr.kind sigma c with Rel n -> (fvs,Int.Set.add n rels) | Var id -> (Id.Set.add id fvs,rels) | _ -> (fvs,rels)) (Id.Set.empty,Int.Set.empty) l in let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel sigma c && Int.Set.mem (destRel sigma c) rels || isVar sigma c && (Id.Set.mem (destVar sigma c) fvs)))) (Evd.find sigma evk) cl in - id,l + id,List.map (fun (id,c) -> (CAst.make id,c)) l with Not_found -> Id.of_string ("X" ^ string_of_int (Evar.repr evk)), - (List.map (fun c -> (Id.of_string "__",c)) cl) + (List.map (fun c -> (CAst.make @@ Id.of_string "__",c)) cl) in GEvar (id, List.map (on_snd (detype d flags avoid env sigma)) l) |