diff options
| -rw-r--r-- | test-suite/bugs/closed/bug_10097.v | 14 | ||||
| -rw-r--r-- | user-contrib/Ltac2/tac2entries.ml | 9 |
2 files changed, 23 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_10097.v b/test-suite/bugs/closed/bug_10097.v new file mode 100644 index 0000000000..12f2d4cc58 --- /dev/null +++ b/test-suite/bugs/closed/bug_10097.v @@ -0,0 +1,14 @@ +From Ltac2 Require Import Ltac2. + +(* #10097 *) +Ltac2 Type s := [X(int)]. +Fail Ltac2 Type s. +Fail Ltac2 Type s := []. + +Ltac2 Type r := [..]. +Fail Ltac2 Type r := []. + +Module Other. + Ltac2 Type s. + Ltac2 Type r := []. +End Other. diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index 92bc49346f..b8853f3755 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -374,6 +374,15 @@ let register_typedef ?(local = false) isrec types = | ({loc;v=id}, _) :: _ -> user_err ?loc (str "Multiple definition of the type name " ++ Id.print id) in + let () = + let check_existing_type ({v=id},_) = + let qid = Libnames.make_qualid (Lib.current_dirpath false) id in + try let _ = Tac2env.locate_type qid in + user_err (str "Multiple definition of the type name " ++ pr_qualid qid) + with Not_found -> () + in + List.iter check_existing_type types + in let check ({loc;v=id}, (params, def)) = let same_name {v=id1} {v=id2} = Id.equal id1 id2 in let () = match List.duplicates same_name params with |