aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--coqpp/coqpp_main.ml6
-rwxr-xr-xdev/ci/ci-hott.sh2
-rw-r--r--dev/ci/user-overlays/07859-printers.sh6
-rw-r--r--interp/constrintern.ml6
-rw-r--r--printing/prettyp.ml6
-rw-r--r--printing/printer.ml16
-rw-r--r--printing/printer.mli8
-rw-r--r--printing/printmod.ml4
-rw-r--r--test-suite/bugs/closed/8126.v13
-rw-r--r--test-suite/output/Notations3.out6
-rw-r--r--test-suite/output/Notations3.v11
-rw-r--r--vernac/himsg.ml8
12 files changed, 61 insertions, 31 deletions
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index e76a1e9ed8..fd425ef4ff 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -326,10 +326,14 @@ let print_ast fmt ext =
end
+let declare_plugin fmt name =
+ fprintf fmt "let %s = \"%s\"@\n" plugin_name name;
+ fprintf fmt "let _ = Mltop.add_known_module %s@\n" plugin_name
+
let pr_ast fmt = function
| Code s -> fprintf fmt "%s@\n" s.code
| Comment s -> fprintf fmt "%s@\n" s
-| DeclarePlugin name -> fprintf fmt "let %s = \"%s\"@\n" plugin_name name
+| DeclarePlugin name -> declare_plugin fmt name
| GramExt gram -> fprintf fmt "%a@\n" GramExt.print_ast gram
| VernacExt -> fprintf fmt "VERNACEXT@\n"
| TacticExt tac -> fprintf fmt "%a@\n" TacticExt.print_ast tac
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index 6ded97984e..184b90a50b 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -7,4 +7,4 @@ HoTT_CI_DIR="${CI_BUILD_DIR}"/HoTT
git_checkout "${HoTT_CI_BRANCH}" "${HoTT_CI_GITURL}" "${HoTT_CI_DIR}"
-( cd "${HoTT_CI_DIR}" && ./autogen.sh && ./configure && make )
+( cd "${HoTT_CI_DIR}" && ./autogen.sh && ./configure && make && make validate )
diff --git a/dev/ci/user-overlays/07859-printers.sh b/dev/ci/user-overlays/07859-printers.sh
new file mode 100644
index 0000000000..27f588e214
--- /dev/null
+++ b/dev/ci/user-overlays/07859-printers.sh
@@ -0,0 +1,6 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "7859" ] || [ "$CI_BRANCH" = "rm-univ-broken-printing" ]; then
+ Equations_CI_BRANCH=fix-printers
+ Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+fi
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c87768b190..715823e5d0 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1891,9 +1891,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
intern_applied_reference intern env (Environ.named_context globalenv)
lvar us args ref
in
- (* Rem: GApp(_,f,[]) stands for @f *)
- DAst.make ?loc @@
- GApp (f, intern_args env args_scopes (List.map fst args))
+ (* Rem: GApp(_,f,[]) stands for @f *)
+ if args = [] then DAst.make ?loc @@ GApp (f,[]) else
+ smart_gapp f loc (intern_args env args_scopes (List.map fst args))
| CApp ((isproj,f), args) ->
let f,args = match f.CAst.v with
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index fd7135b6a6..7258bb9b72 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -98,7 +98,8 @@ let print_ref reduce ref udecl =
(Array.to_list (Univ.Instance.to_array inst)) udecl in
let sigma = Evd.from_ctx (UState.of_binders bl) in
let inst =
- if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs
+ if Global.is_polymorphic ref
+ then Printer.pr_universe_instance sigma (Univ.UContext.instance univs)
else mt ()
in
hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++
@@ -552,8 +553,7 @@ let print_instance sigma cb =
if Declareops.constant_is_polymorphic cb then
let univs = Declareops.constant_polymorphic_context cb in
let inst = Univ.AUContext.instance univs in
- let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
- pr_universe_instance sigma univs
+ pr_universe_instance sigma inst
else mt()
let print_constant with_values sep sp udecl =
diff --git a/printing/printer.ml b/printing/printer.ml
index ba094596ff..a77c1ced56 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -290,11 +290,13 @@ let pr_cumulativity_info sigma cumi =
let pr_global_env = pr_global_env
let pr_global = pr_global_env Id.Set.empty
-let pr_puniverses f env (c,u) =
- f env c ++
- (if !Constrextern.print_universes then
- str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)"
- else mt ())
+let pr_universe_instance evd inst =
+ str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}"
+
+let pr_puniverses f env sigma (c,u) =
+ if !Constrextern.print_universes
+ then f env c ++ pr_universe_instance sigma u
+ else f env c
let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst)
let pr_existential_key = Termops.pr_existential_key
@@ -1016,10 +1018,6 @@ let pr_polymorphic b =
if b then str"Polymorphic " else str"Monomorphic "
else mt ()
-let pr_universe_instance evd ctx =
- let inst = Univ.UContext.instance ctx in
- str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}"
-
(* print the proof step, possibly with diffs highlighted, *)
let print_and_diff oldp newp =
match newp with
diff --git a/printing/printer.mli b/printing/printer.mli
index 948b06f3f6..971241d5f9 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -120,7 +120,7 @@ val pr_sort : evar_map -> Sorts.t -> Pp.t
val pr_polymorphic : bool -> Pp.t
val pr_cumulative : bool -> bool -> Pp.t
-val pr_universe_instance : evar_map -> Univ.UContext.t -> Pp.t
+val pr_universe_instance : evar_map -> Univ.Instance.t -> Pp.t
val pr_universe_ctx : evar_map -> ?variance:Univ.Variance.t array ->
Univ.UContext.t -> Pp.t
val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t
@@ -139,9 +139,9 @@ val pr_constructor : env -> constructor -> Pp.t
val pr_inductive : env -> inductive -> Pp.t
val pr_evaluable_reference : evaluable_global_reference -> Pp.t
-val pr_pconstant : env -> pconstant -> Pp.t
-val pr_pinductive : env -> pinductive -> Pp.t
-val pr_pconstructor : env -> pconstructor -> Pp.t
+val pr_pconstant : env -> evar_map -> pconstant -> Pp.t
+val pr_pinductive : env -> evar_map -> pinductive -> Pp.t
+val pr_pconstructor : env -> evar_map -> pconstructor -> Pp.t
(** Contexts *)
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 3f95dcfb6d..e2d9850bf8 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -103,9 +103,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
let envpar = push_rel_context params env in
let inst =
if Declareops.inductive_is_polymorphic mib then
- let ctx = Declareops.inductive_polymorphic_context mib in
- let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
- Printer.pr_universe_instance sigma ctx
+ Printer.pr_universe_instance sigma u
else mt ()
in
hov 0 (
diff --git a/test-suite/bugs/closed/8126.v b/test-suite/bugs/closed/8126.v
new file mode 100644
index 0000000000..f52dfc6b47
--- /dev/null
+++ b/test-suite/bugs/closed/8126.v
@@ -0,0 +1,13 @@
+(* See also output test Notations4.v *)
+
+Inductive foo := tt.
+Bind Scope foo_scope with foo.
+Delimit Scope foo_scope with foo.
+Notation "'HI'" := tt : foo_scope.
+Definition myfoo (x : nat) (y : nat) (z : foo) := y.
+Notation myfoo0 := (@myfoo 0).
+Notation myfoo01 := (@myfoo0 1).
+Check myfoo 0 1 HI. (* prints [myfoo0 1 HI], but should print [myfoo01 HI] *)
+Check myfoo0 1 HI. (* prints [myfoo0 1 HI], but should print [myfoo01 HI] *)
+Check myfoo01 tt. (* prints [myfoo0 1 HI], but should print [myfoo01 HI] *)
+Check myfoo01 HI. (* was failing *)
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 5ab616160a..d32cf67e28 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -246,3 +246,9 @@ Notation
============================
##@%
^^^
+myfoo01 tt
+ : nat
+myfoo01 tt
+ : nat
+myfoo01 tt
+ : nat
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 876aaa3944..180e8d337e 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -399,3 +399,14 @@ Show.
Abort.
End Issue7731.
+
+Module Issue8126.
+
+Definition myfoo (x : nat) (y : nat) (z : unit) := y.
+Notation myfoo0 := (@myfoo 0).
+Notation myfoo01 := (@myfoo0 1).
+Check myfoo 0 1 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] *)
+Check myfoo0 1 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] *)
+Check myfoo01 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] *)
+
+End Issue8126.
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index c49ffe2679..e208d176bb 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -194,12 +194,6 @@ let rec pr_disjunction pr = function
| a::l -> pr a ++ str "," ++ spc () ++ pr_disjunction pr l
| [] -> assert false
-let pr_puniverses f env (c,u) =
- f env c ++
- (if Flags.is_universe_polymorphism () && not (Univ.Instance.is_empty u) then
- str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)"
- else mt())
-
let explain_elim_arity env sigma ind sorts c pj okinds =
let open EConstr in
let env = make_all_name_different env sigma in
@@ -262,7 +256,7 @@ let explain_ill_formed_branch env sigma c ci actty expty =
let pa, pe = pr_explicit env sigma (simp actty) (simp expty) in
strbrk "In pattern-matching on term" ++ brk(1,1) ++ pc ++
spc () ++ strbrk "the branch for constructor" ++ spc () ++
- quote (pr_puniverses pr_constructor env ci) ++
+ quote (pr_pconstructor env sigma ci) ++
spc () ++ str "has type" ++ brk(1,1) ++ pa ++ spc () ++
str "which should be" ++ brk(1,1) ++ pe ++ str "."
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 08:11:18 +0000