diff options
| -rw-r--r-- | pretyping/program.ml | 6 | ||||
| -rw-r--r-- | test-suite/bugs/closed/5066.v | 7 |
2 files changed, 11 insertions, 2 deletions
diff --git a/pretyping/program.ml b/pretyping/program.ml index b4333847b..62aedcfbf 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -15,10 +15,12 @@ open Term let make_dir l = DirPath.make (List.rev_map Id.of_string l) let find_reference locstr dir s = - let sp = Libnames.make_path (make_dir dir) (Id.of_string s) in + let dp = make_dir dir in + let sp = Libnames.make_path dp (Id.of_string s) in try Nametab.global_of_path sp with Not_found -> - anomaly ~label:locstr (Pp.str "cannot find" ++ spc () ++ Libnames.pr_path sp) + user_err_loc (Loc.ghost, "", str "Library " ++ Libnames.pr_dirpath dp ++ + str " has to be required first.") let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s let coq_constant locstr dir s = Universes.constr_of_global (coq_reference locstr dir s) diff --git a/test-suite/bugs/closed/5066.v b/test-suite/bugs/closed/5066.v new file mode 100644 index 000000000..eed7f0f3f --- /dev/null +++ b/test-suite/bugs/closed/5066.v @@ -0,0 +1,7 @@ +Require Import Vector. + +Fail Program Fixpoint vector_rev {A : Type} {n1 n2 : nat} (v1 : Vector.t A n1) (v2 : Vector.t A n2) : Vector.t A (n1+n2) := + match v1 with + | nil _ => v2 + | cons _ e n' sv => vector_rev sv (cons A e n2 v2) + end. |