diff options
Diffstat (limited to 'vernac/comInductive.ml')
| -rw-r--r-- | vernac/comInductive.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index b93e8d9ac..6057c05f5 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -44,8 +44,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(make ?loc @@ Ident id,None))) params in - CAppExpl ((None,CAst.make ?loc @@ Ident name,None),List.rev args) + let args = List.map (fun id -> CAst.(make ?loc @@ CRef(qualid_of_ident ?loc id,None))) params in + CAppExpl ((None,qualid_of_ident ?loc name,None),List.rev args) | c -> c ) |