Merge PR #6837: [located] Push inner locations in reference to a CAst.t node.

1 files changed, 2 insertions, 2 deletions

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index c59286d1a3..db2f16525b 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -46,8 +46,8 @@ let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function
         user_err ?loc
          (strbrk"Cannot infer the non constant arguments of the conclusion of "
           ++ Id.print cs ++ str ".");
-      let args = List.map (fun id -> CAst.make ?loc @@ CRef(Ident(loc,id),None)) params in
-      CAppExpl ((None,Ident(loc,name),None),List.rev args)
+      let args = List.map (fun id -> CAst.(make ?loc @@ CRef(make ?loc @@ Ident id,None))) params in
+      CAppExpl ((None,CAst.make ?loc @@ Ident name,None),List.rev args)
   | c -> c
   )