diff options
34 files changed, 774 insertions, 96 deletions
diff --git a/.gitignore b/.gitignore index 71de7bb8d0..5ee2f3f77b 100644 --- a/.gitignore +++ b/.gitignore @@ -84,6 +84,8 @@ test-suite/coq-makefile/*/subdir/done test-suite/coq-makefile/merlin1/.merlin test-suite/coq-makefile/plugin-reach-outside-API-and-fail/_CoqProject test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/_CoqProject +test-suite/coqdoc/Coqdoc.* +test-suite/coqdoc/index.html # documentation diff --git a/API/API.mli b/API/API.mli index a0e77edd12..a99cd2a9ae 100644 --- a/API/API.mli +++ b/API/API.mli @@ -3782,6 +3782,12 @@ sig | DefaultInline | InlineAt of int + type cumulative_inductive_parsing_flag = + | GlobalCumulativity + | GlobalNonCumulativity + | LocalCumulativity + | LocalNonCumulativity + type vernac_expr = | VernacLoad of verbose_flag * string | VernacTime of vernac_expr Loc.located @@ -3806,7 +3812,7 @@ sig | VernacExactProof of Constrexpr.constr_expr | VernacAssumption of (Decl_kinds.locality option * Decl_kinds.assumption_object_kind) * inline * (plident list * Constrexpr.constr_expr) with_coercion list - | VernacInductive of Decl_kinds.cumulative_inductive_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list + | VernacInductive of cumulative_inductive_parsing_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of Decl_kinds.locality option * (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of diff --git a/README.ci.md b/README.ci.md index 9e25390d72..cf9da50941 100644 --- a/README.ci.md +++ b/README.ci.md @@ -1,30 +1,42 @@ **WARNING:** This document is a work in progress and intended as a RFC. -If you are not a Coq Developer, don't follow this instructions yet. +If you are not a Coq Developer, don't follow these instructions yet. Introduction ============ -The Coq Travis CI infrastructure is meant to provide lightweight -automatics testing of pull requests. -If you are on GitLab, their integrated CI is also set up. +As of 2017, Coq's Git repository includes a `.travis.yml` file, a +`.gitlab-ci.yml` file, and supporting scripts, that enable lightweight +Continuous Integration (CI) tests to be run on clones of that repository stored +at Github or on a GitLab instance, respectively. This affords two benefits. -More comprehensive testing is the responsability of Coq's [Jenkins CI -server](https://ci.inria.fr/coq/) see, [XXX: add document] for -instructions on how to add your development to Jenkins. +First, it allows developers working on Coq itself to perform CI on their own +Git remotes, thereby enabling them to catch and fix problems with their +proposed changes before submitting pull requests to Coq itself. This in turn +reduces the risk of a faulty PR being opened against the official Coq +repository. -How to submit your development for Coq CI -========================================= +Secondly, it allows developers working on a library dependent on Coq to have +that library included in the Travis CI tests invoked by the official Coq +repository on GitHub. + +(More comprehensive testing than is provided by the Travis CI and GitLab CI +integration is the responsibility of Coq's [Jenkins CI +server](https://ci.inria.fr/coq/) see, [XXX: add document] for instructions on +how to add your development to Jenkins.) + +How to submit your library for inclusion in Coq's Travis CI builds +================================================================== CI provides a convenient way to perform testing of Coq changes versus a set of curated libraries. Are you an author of a Coq library who would be interested in having -the latest Coq changes validated against your development? +the latest Coq changes validated against it? -If so, keep reading! Getting Coq changes tested against your library -is easy, all that you need to do is: +If so, all you need to do is: -1. Put you development in a public repository tracking coq trunk. +1. Put your library in a public repository tracking the `master` + branch of Coq's Git repository. 2. Make sure that your development builds in less than 35 minutes. 3. Submit a PR adding your development. 4. ? diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index 8cb049d50e..499239b6f3 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -381,6 +381,9 @@ some specific {\tt Extract Constant} when primitive counterparts exist. \Example Typical examples are the following: +\begin{coq_eval} +Require Extraction. +\end{coq_eval} \begin{coq_example} Extract Inductive unit => "unit" [ "()" ]. Extract Inductive bool => "bool" [ "true" "false" ]. diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 96fb1eb752..7a71d69086 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1425,6 +1425,9 @@ If there is an hypothesis $h:a=b$ in the local context, it can be used for rewriting not only in logical propositions but also in any type. % In that case, the term \verb!eq_rec! which was defined as an axiom, is % now a term of the calculus. +\begin{coq_eval} +Require Extraction. +\end{coq_eval} \begin{coq_example} Print eq_rec. Extraction eq_rec. diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index 71977d3e9d..ef12fe416a 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -37,7 +37,7 @@ Similarly, the notation ``\nelist{\entry}{}'' stands for a non empty sequence of expressions parsed by the ``{\entry}'' entry, without any separator between. -At the end, the notation ``\sequence{\entry}{\tt sep}'' stands for a +Finally, the notation ``\sequence{\entry}{\tt sep}'' stands for a possibly empty sequence of expressions parsed by the ``{\entry}'' entry, separated by the literal ``{\tt sep}''. diff --git a/doc/refman/RefMan-int.tex b/doc/refman/RefMan-int.tex index eca3efcdd6..2b9e4e6051 100644 --- a/doc/refman/RefMan-int.tex +++ b/doc/refman/RefMan-int.tex @@ -58,7 +58,7 @@ Chapter~\ref{Addoc-coqide}. \section*{How to read this book} -This is a Reference Manual, not a User Manual, then it is not made for a +This is a Reference Manual, not a User Manual, so it is not made for a continuous reading. However, it has some structure that is explained below. diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex index d3719bed46..23a1c9b029 100644 --- a/doc/refman/RefMan-sch.tex +++ b/doc/refman/RefMan-sch.tex @@ -227,6 +227,7 @@ We define the function \texttt{div2} as follows: \begin{coq_eval} Reset Initial. +Require Import FunInd. \end{coq_eval} \begin{coq_example*} diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex index 9f4ddc8044..cb8f916f13 100644 --- a/doc/refman/RefMan-tacex.tex +++ b/doc/refman/RefMan-tacex.tex @@ -849,7 +849,7 @@ Ltac DSimplif trm := Ltac Length trm := match trm with | (_ * ?B) => let succ := Length B in constr:(S succ) - | _ => constr:1 + | _ => constr:(1) end. Ltac assoc := repeat rewrite <- Ass. \end{coq_example} diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex index 2c9602a229..6c79284389 100644 --- a/doc/refman/Setoid.tex +++ b/doc/refman/Setoid.tex @@ -156,9 +156,9 @@ compatibility constraints. \begin{cscexample}[Rewriting] Continuing the previous examples, suppose that the user must prove \texttt{set\_eq int (union int (union int S1 S2) S2) (f S1 S2)} under the -hypothesis \texttt{H: set\_eq int S2 (nil int)}. It is possible to +hypothesis \texttt{H: set\_eq int S2 (@nil int)}. It is possible to use the \texttt{rewrite} tactic to replace the first two occurrences of -\texttt{S2} with \texttt{nil int} in the goal since the context +\texttt{S2} with \texttt{@nil int} in the goal since the context \texttt{set\_eq int (union int (union int S1 nil) nil) (f S1 S2)}, being a composition of morphisms instances, is a morphism. However the tactic will fail replacing the third occurrence of \texttt{S2} unless \texttt{f} diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex index 2bb1301c79..cd36d1d320 100644 --- a/doc/refman/Universes.tex +++ b/doc/refman/Universes.tex @@ -134,12 +134,14 @@ producing global universe constraints, one can use the \asection{{\tt Cumulative, NonCumulative}} \comindex{Cumulative} \comindex{NonCumulative} -\optindex{Inductive Cumulativity} +\optindex{Polymorphic Inductive Cumulativity} -Inductive types, coinductive types, variants and records can be +Polymorphic inductive types, coinductive types, variants and records can be declared cumulative using the \texttt{Cumulative}. Alternatively, -there is an option \texttt{Set Inductive Cumulativity} which when set, -makes all subsequent inductive definitions cumulative. Consider the examples below. +there is an option \texttt{Set Polymorphic Inductive Cumulativity} which when set, +makes all subsequent \emph{polymorphic} inductive definitions cumulative. When set, +inductive types and the like can be enforced to be +\emph{non-cumulative} using the \texttt{NonCumulative} prefix. Consider the examples below. \begin{coq_example*} Polymorphic Cumulative Inductive list {A : Type} := | nil : list @@ -158,24 +160,61 @@ This also means that any two instances of \texttt{list} are convertible: $\WTEGCONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ whenever $\WTEGCONV{A}{B}$ and furthermore their corresponding (when fully applied to convertible arguments) constructors. See Chapter~\ref{Cic} for more details on convertibility and subtyping. -Also notice the subtyping constraints for the \emph{non-cumulative} version of list: +The following is an example of a record with non-trivial subtyping relation: \begin{coq_example*} -Polymorphic NonCumulative Inductive list' {A : Type} := -| nil' : list' -| cons' : A -> list' -> list'. +Polymorphic Cumulative Record packType := {pk : Type}. \end{coq_example*} \begin{coq_example} -Print list'. +Print packType. +\end{coq_example} +Notice that as expected, \texttt{packType@\{i\}} and \texttt{packType@\{j\}} are +convertible if and only if \texttt{i $=$ j}. + +Cumulative inductive types, coninductive types, variants and records +only make sense when they are universe polymorphic. Therefore, an +error is issued whenever the user uses the \texttt{Cumulative} or +\texttt{NonCumulative} prefix in a monomorphic context. +Notice that this is not the case for the option \texttt{Set Polymorphic Inductive Cumulativity}. +That is, this option, when set, makes all subsequent \emph{polymorphic} +inductive declarations cumulative (unless, of course the \texttt{NonCumulative} prefix is used) +but has no effect on \emph{monomorphic} inductive declarations. +Consider the following examples. +\begin{coq_example} +Monomorphic Cumulative Inductive Unit := unit. +\end{coq_example} +\begin{coq_example} +Monomorphic NonCumulative Inductive Unit := unit. \end{coq_example} -The following is an example of a record with non-trivial subtyping relation: \begin{coq_example*} -Polymorphic Cumulative Record packType := {pk : Type}. +Set Polymorphic Inductive Cumulativity. +Inductive Unit := unit. \end{coq_example*} \begin{coq_example} -Print packType. +Print Unit. \end{coq_example} -Notice that as expected, \texttt{packType@\{i\}} and \texttt{packType@\{j\}} are convertible if and only if \texttt{i $=$ j}. +\subsection*{An example of a proof using cumulativity} + +\begin{coq_example} +Set Universe Polymorphism. +Set Polymorphic Inductive Cumulativity. + +Inductive eq@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := eq_refl : eq x x. + +Definition funext_type@{a b e} (A : Type@{a}) (B : A -> Type@{b}) + := forall f g : (forall a, B a), + (forall x, eq@{e} (f x) (g x)) + -> eq@{e} f g. + +Section down. + Universes a b e e'. + Constraint e' < e. + Lemma funext_down {A B} + (H : @funext_type@{a b e} A B) : @funext_type@{a b e'} A B. + Proof. + exact H. + Defined. +\end{coq_example} \asection{Global and local universes} diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex index 8337b1c48f..77ce8574f2 100644 --- a/doc/tutorial/Tutorial.tex +++ b/doc/tutorial/Tutorial.tex @@ -241,7 +241,7 @@ Variables A B C : Prop. \end{coq_example} We shall consider simple implications, such as $A\ra B$, read as -``$A$ implies $B$''. Remark that we overload the arrow symbol, which +``$A$ implies $B$''. Note that we overload the arrow symbol, which has been used above as the functionality type constructor, and which may be used as well as propositional connective: \begin{coq_example} @@ -289,7 +289,7 @@ apply H. We are now in the situation where we have two judgments as conjectures that remain to be proved. Only the first is listed in full, for the others the system displays only the corresponding subgoal, without its -local hypotheses list. Remark that \verb:apply: has kept the local +local hypotheses list. Note that \verb:apply: has kept the local hypotheses of its father judgment, which are still available for the judgments it generated. @@ -654,7 +654,7 @@ Hypothesis R_transitive : forall x y z : D, R x y -> R y z -> R x z. \end{coq_example} -Remark the syntax \verb+forall x : D,+ which stands for universal quantification +Note the syntax \verb+forall x : D,+ which stands for universal quantification $\forall x : D$. \subsection{Existential quantification} @@ -664,10 +664,10 @@ We now state our lemma, and enter proof mode. Lemma refl_if : forall x : D, (exists y, R x y) -> R x x. \end{coq_example} -Remark that the hypotheses which are local to the currently opened sections +The hypotheses that are local to the currently opened sections are listed as local hypotheses to the current goals. -The rationale is that these hypotheses are going to be discharged, as we -shall see, when we shall close the corresponding sections. +That is because these hypotheses are going to be discharged, as +we shall see, when we shall close the corresponding sections. Note the functional syntax for existential quantification. The existential quantifier is built from the operator \verb:ex:, which expects a @@ -687,7 +687,7 @@ verifies \verb:P:. Let us see how this works on this simple example. intros x x_Rlinked. \end{coq_example} -Remark that \verb:intros: treats universal quantification in the same way +Note that \verb:intros: treats universal quantification in the same way as the premises of implications. Renaming of bound variables occurs when it is needed; for instance, had we started with \verb:intro y:, we would have obtained the goal: @@ -859,7 +859,7 @@ Check weird. Check drinker. \end{coq_example} -Remark how the three theorems are completely generic in the most general +Note how the three theorems are completely generic in the most general fashion; the domain \verb:D: is discharged in all of them, \verb:R: is discharged in \verb:refl_if: only, \verb:P: is discharged only in \verb:weird: and @@ -867,7 +867,7 @@ the domain \verb:D: is discharged in all of them, \verb:R: is discharged in Finally, the excluded middle hypothesis is discharged only in \verb:drinker:. -Note that the name \verb:d: has vanished as well from +Note, too, that the name \verb:d: has vanished from the statements of \verb:weird: and \verb:drinker:, since \Coq's pretty-printer replaces systematically a quantification such as \texttt{forall d : D, E}, diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 6ef9532ad7..2adf522b74 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -305,6 +305,14 @@ type inline = type module_ast_inl = module_ast * inline type module_binder = bool option * lident list * module_ast_inl +(** Cumulativity can be set globally, locally or unset locally and it + can not enabled at all. *) +type cumulative_inductive_parsing_flag = + | GlobalCumulativity + | GlobalNonCumulativity + | LocalCumulativity + | LocalNonCumulativity + (** {6 The type of vernacular expressions} *) type vernac_expr = @@ -336,7 +344,7 @@ type vernac_expr = | VernacExactProof of constr_expr | VernacAssumption of (locality option * assumption_object_kind) * inline * (plident list * constr_expr) with_coercion list - | VernacInductive of cumulative_inductive_flag * private_flag * inductive_flag * (inductive_expr * decl_notation list) list + | VernacInductive of cumulative_inductive_parsing_flag * private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of locality option * (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of diff --git a/lib/flags.ml b/lib/flags.ml index 0bce22f584..027ba16f0e 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -167,9 +167,9 @@ let use_polymorphic_flag () = let make_polymorphic_flag b = local_polymorphic_flag := Some b -let inductive_cumulativity = ref false -let make_inductive_cumulativity b = inductive_cumulativity := b -let is_inductive_cumulativity () = !inductive_cumulativity +let polymorphic_inductive_cumulativity = ref false +let make_polymorphic_inductive_cumulativity b = polymorphic_inductive_cumulativity := b +let is_polymorphic_inductive_cumulativity () = !polymorphic_inductive_cumulativity (** [program_mode] tells that Program mode has been activated, either globally via [Set Program] or locally via the Program command prefix. *) diff --git a/lib/flags.mli b/lib/flags.mli index eb4c37a548..5af563b46e 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -119,9 +119,9 @@ val is_universe_polymorphism : unit -> bool val make_polymorphic_flag : bool -> unit val use_polymorphic_flag : unit -> bool -(** Global inductive cumulativity flag. *) -val make_inductive_cumulativity : bool -> unit -val is_inductive_cumulativity : unit -> bool +(** Global polymorphic inductive cumulativity flag. *) +val make_polymorphic_inductive_cumulativity : bool -> unit +val is_polymorphic_inductive_cumulativity : unit -> bool val warn : bool ref val make_warn : bool -> unit diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 3d29fca779..93a778274d 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -168,8 +168,13 @@ GEXTEND Gram let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in let cum = match cum with - Some b -> b - | None -> Flags.is_inductive_cumulativity () + Some true -> LocalCumulativity + | Some false -> LocalNonCumulativity + | None -> + if Flags.is_polymorphic_inductive_cumulativity () then + GlobalCumulativity + else + GlobalNonCumulativity in VernacInductive (cum, priv,f,indl) | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 8555a0b226..8cf5e8442d 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1492,7 +1492,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Vernacexpr.GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds)) ++ fnl () ++ msg in @@ -1507,7 +1507,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Vernacexpr.GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds)) ++ fnl () ++ CErrors.print reraise in diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4 index dd24aa3dbf..104977aef3 100644 --- a/plugins/ltac/g_class.ml4 +++ b/plugins/ltac/g_class.ml4 @@ -20,7 +20,7 @@ let set_transparency cl b = List.iter (fun r -> let gr = Smartlocate.global_with_alias r in let ev = Tacred.evaluable_of_global_reference (Global.env ()) gr in - Classes.set_typeclass_transparency ev false b) cl + Classes.set_typeclass_transparency ev (Locality.make_section_locality None) b) cl VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings CLASSIFIED AS SIDEFF | [ "Typeclasses" "Transparent" reference_list(cl) ] -> [ diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index d4fa266c02..375a8a983f 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -84,8 +84,8 @@ type instance = { is_class: global_reference; is_info: Vernacexpr.hint_info_expr; (* Sections where the instance should be redeclared, - -1 for discard, 0 for none. *) - is_global: int; + None for discard, Some 0 for none. *) + is_global: int option; is_poly: bool; is_impl: global_reference; } @@ -98,9 +98,11 @@ let hint_priority is = is.is_info.Vernacexpr.hint_priority let new_instance cl info glob poly impl = let global = - if glob then Lib.sections_depth () - else -1 + if glob then Some (Lib.sections_depth ()) + else None in + if match global with Some n -> n>0 && isVarRef impl | _ -> false then + CErrors.user_err (Pp.str "Cannot set Global an instance referring to a section variable."); { is_class = cl.cl_impl; is_info = info ; is_global = global ; @@ -350,22 +352,34 @@ let subst_instance (subst, (action, inst)) = action, is_impl = fst (subst_global subst inst.is_impl) } let discharge_instance (_, (action, inst)) = - if inst.is_global <= 0 then None - else Some (action, + match inst.is_global with + | None -> None + | Some n -> + assert (not (isVarRef inst.is_impl)); + Some (action, { inst with - is_global = pred inst.is_global; + is_global = Some (pred n); is_class = Lib.discharge_global inst.is_class; is_impl = Lib.discharge_global inst.is_impl }) -let is_local i = Int.equal i.is_global (-1) +let is_local i = (i.is_global == None) + +let is_local_for_hint i = + match i.is_global with + | None -> true (* i.e. either no Global keyword not in section, or in section *) + | Some n -> n <> 0 (* i.e. in a section, declare the hint as local + since discharge is managed by rebuild_instance which calls again + add_instance_hint; don't ask hints to take discharge into account + itself *) let add_instance check inst = let poly = Global.is_polymorphic inst.is_impl in - add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] (is_local inst) + let local = is_local_for_hint inst in + add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] local inst.is_info poly; List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path - (is_local inst) pri poly) + local pri poly) (build_subclasses ~check:(check && not (isVarRef inst.is_impl)) (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info) @@ -404,6 +418,7 @@ let declare_instance info local glob = let info = Option.default {hint_priority = None; hint_pattern = None} info in match class_of_constr Evd.empty (EConstr.of_constr ty) with | Some (rels, ((tc,_), args) as _cl) -> + assert (not (isVarRef glob) || local); add_instance (new_instance tc info (not local) (Flags.use_polymorphic_flag ()) glob) | None -> () diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index a68b569cbe..4c50c2f368 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -760,7 +760,11 @@ open Decl_kinds | Class _ -> "Class" | Variant -> "Variant" in if p then - let cm = if cum then "Cumulative" else "NonCumulative" in + let cm = + match cum with + | GlobalCumulativity | LocalCumulativity -> "Cumulative" + | GlobalNonCumulativity | LocalNonCumulativity -> "NonCumulative" + in cm ^ " " ^ kind else kind in diff --git a/test-suite/Makefile b/test-suite/Makefile index beb80a3dfd..1268ed14bc 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -33,6 +33,7 @@ BIN := $(shell cd ..; pwd)/bin/ coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite +coqdoc := $(BIN)coqdoc coqtopbyte := $(BIN)coqtop.byte coqtopload := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source @@ -85,7 +86,8 @@ COMPLEXITY := $(if $(bogomips),complexity) BUGS := bugs/opened bugs/closed VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ - output-modulo-time interactive micromega $(COMPLEXITY) modules stm + output-modulo-time interactive micromega $(COMPLEXITY) modules stm \ + coqdoc # All subsystems SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coq-makefile @@ -153,6 +155,7 @@ summary: $(call summary_dir, "VI tests", vio); \ $(call summary_dir, "Coqchk tests", coqchk); \ $(call summary_dir, "Coq makefile", coq-makefile); \ + $(call summary_dir, "Coqdoc tests", coqdoc); \ nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \ nb_failure=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_failure) | wc -l`; \ nb_tests=`expr $$nb_success + $$nb_failure`; \ @@ -456,6 +459,8 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake)) fi; \ } > "$@" +# vio compilation + vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v)) %.vio.log:%.v @@ -473,6 +478,8 @@ vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v)) fi; \ } > "$@" +# coqchk + coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v)) %.chk.log:%.v @@ -489,6 +496,8 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v)) fi; \ } > "$@" +# coq_makefile + coq-makefile: $(patsubst %/run.sh,%.log,$(wildcard coq-makefile/*/run.sh)) coq-makefile/%.log : coq-makefile/%/run.sh @@ -505,3 +514,27 @@ coq-makefile/%.log : coq-makefile/%/run.sh echo " $<...Error!"; \ fi; \ ) > "$@" + +# coqdoc + +coqdoc: $(patsubst %.sh,%.log,$(wildcard coqdoc/*.sh)) + +$(addsuffix .log,$(wildcard coqdoc/*.v)): %.v.log: %.v %.html.out %.tex.out $(PREREQUISITELOG) + @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" + $(HIDE){ \ + echo $(call log_intro,$<); \ + $(coqc) -R coqdoc Coqdoc $* 2>&1; \ + cd coqdoc; \ + f=`basename $*`; \ + $(coqdoc) -R . Coqdoc -coqlib http://coq.inria.fr/stdlib --html $$f.v; \ + $(coqdoc) -R . Coqdoc -coqlib http://coq.inria.fr/stdlib --latex $$f.v; \ + diff -u $$f.html.out Coqdoc.$$f.html 2>&1; R=$$?; times; \ + grep -v "^%%" Coqdoc.$$f.tex | diff -u $$f.tex.out - 2>&1; S=$$?; times; \ + if [ $$R = 0 -a $$S = 0 ]; then \ + echo $(log_success); \ + echo " $<...Ok"; \ + else \ + echo $(log_failure); \ + echo " $<...Error! (unexpected output)"; \ + fi; \ + } > "$@" diff --git a/test-suite/bugs/closed/5598.v b/test-suite/bugs/closed/5598.v new file mode 100644 index 0000000000..55fef1a575 --- /dev/null +++ b/test-suite/bugs/closed/5598.v @@ -0,0 +1,8 @@ +(* Checking when discharge of an existing class is possible *) +Section foo. + Context {T} (a : T) (b : T). + Let k := eq_refl a. + Existing Class eq. + Fail Global Existing Instance k. + Existing Instance k. +End foo. diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v index a978f6b901..7906a5b15e 100644 --- a/test-suite/coqchk/cumulativity.v +++ b/test-suite/coqchk/cumulativity.v @@ -1,5 +1,5 @@ Set Universe Polymorphism. -Set Inductive Cumulativity. +Set Polymorphic Inductive Cumulativity. Set Printing Universes. Inductive List (A: Type) := nil | cons : A -> List A -> List A. diff --git a/test-suite/coqdoc/bug5648.html.out b/test-suite/coqdoc/bug5648.html.out new file mode 100644 index 0000000000..06789c1c10 --- /dev/null +++ b/test-suite/coqdoc/bug5648.html.out @@ -0,0 +1,53 @@ +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" +"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> +<html xmlns="http://www.w3.org/1999/xhtml"> +<head> +<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1" /> +<link href="coqdoc.css" rel="stylesheet" type="text/css" /> +<title>Coqdoc.bug5648</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library Coqdoc.bug5648</h1> + +<div class="code"> +<span class="id" title="keyword">Lemma</span> <a name="a"><span class="id" title="lemma">a</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a>.<br/> +<span class="id" title="keyword">Proof</span>.<br/> +<span class="id" title="tactic">auto</span>.<br/> +<span class="id" title="keyword">Qed</span>.<br/> + +<br/> +<span class="id" title="keyword">Variant</span> <a name="t"><span class="id" title="inductive">t</span></a> :=<br/> +| <a name="A"><span class="id" title="constructor">A</span></a> | <a name="Add"><span class="id" title="constructor">Add</span></a> | <a name="G"><span class="id" title="constructor">G</span></a> | <a name="Goal"><span class="id" title="constructor">Goal</span></a> | <a name="L"><span class="id" title="constructor">L</span></a> | <a name="Lemma"><span class="id" title="constructor">Lemma</span></a> | <a name="P"><span class="id" title="constructor">P</span></a> | <a name="Proof"><span class="id" title="constructor">Proof</span></a> .<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="d"><span class="id" title="definition">d</span></a> <span class="id" title="var">x</span> :=<br/> + <span class="id" title="keyword">match</span> <a class="idref" href="Coqdoc.bug5648.html#x"><span class="id" title="variable">x</span></a> <span class="id" title="keyword">with</span><br/> + | <a class="idref" href="Coqdoc.bug5648.html#A"><span class="id" title="constructor">A</span></a> => 0<br/> + | <a class="idref" href="Coqdoc.bug5648.html#Add"><span class="id" title="constructor">Add</span></a> => 1<br/> + | <a class="idref" href="Coqdoc.bug5648.html#G"><span class="id" title="constructor">G</span></a> => 2<br/> + | <a class="idref" href="Coqdoc.bug5648.html#Goal"><span class="id" title="constructor">Goal</span></a> => 3<br/> + | <a class="idref" href="Coqdoc.bug5648.html#L"><span class="id" title="constructor">L</span></a> => 4<br/> + | <a class="idref" href="Coqdoc.bug5648.html#Lemma"><span class="id" title="constructor">Lemma</span></a> => 5<br/> + | <a class="idref" href="Coqdoc.bug5648.html#P"><span class="id" title="constructor">P</span></a> => 6<br/> + | <a class="idref" href="Coqdoc.bug5648.html#Proof"><span class="id" title="constructor">Proof</span></a> => 7<br/> + <span class="id" title="keyword">end</span>.<br/> +</div> +</div> + +<div id="footer"> +<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> +</div> + +</div> + +</body> +</html>
\ No newline at end of file diff --git a/test-suite/coqdoc/bug5648.tex.out b/test-suite/coqdoc/bug5648.tex.out new file mode 100644 index 0000000000..b0b732effa --- /dev/null +++ b/test-suite/coqdoc/bug5648.tex.out @@ -0,0 +1,49 @@ +\documentclass[12pt]{report} +\usepackage[]{inputenc} +\usepackage[T1]{fontenc} +\usepackage{fullpage} +\usepackage{coqdoc} +\usepackage{amsmath,amssymb} +\usepackage{url} +\begin{document} +\coqlibrary{Coqdoc.bug5648}{Library }{Coqdoc.bug5648} + +\begin{coqdoccode} +\coqdocnoindent +\coqdockw{Lemma} \coqdef{Coqdoc.bug5648.a}{a}{\coqdoclemma{a}} : \coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}.\coqdoceol +\coqdocnoindent +\coqdockw{Proof}.\coqdoceol +\coqdocnoindent +\coqdoctac{auto}.\coqdoceol +\coqdocnoindent +\coqdockw{Qed}.\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Variant} \coqdef{Coqdoc.bug5648.t}{t}{\coqdocinductive{t}} :=\coqdoceol +\coqdocnoindent +\ensuremath{|} \coqdef{Coqdoc.bug5648.A}{A}{\coqdocconstructor{A}} \ensuremath{|} \coqdef{Coqdoc.bug5648.Add}{Add}{\coqdocconstructor{Add}} \ensuremath{|} \coqdef{Coqdoc.bug5648.G}{G}{\coqdocconstructor{G}} \ensuremath{|} \coqdef{Coqdoc.bug5648.Goal}{Goal}{\coqdocconstructor{Goal}} \ensuremath{|} \coqdef{Coqdoc.bug5648.L}{L}{\coqdocconstructor{L}} \ensuremath{|} \coqdef{Coqdoc.bug5648.Lemma}{Lemma}{\coqdocconstructor{Lemma}} \ensuremath{|} \coqdef{Coqdoc.bug5648.P}{P}{\coqdocconstructor{P}} \ensuremath{|} \coqdef{Coqdoc.bug5648.Proof}{Proof}{\coqdocconstructor{Proof}} .\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.bug5648.d}{d}{\coqdocdefinition{d}} \coqdocvar{x} :=\coqdoceol +\coqdocindent{1.00em} +\coqdockw{match} \coqdocvariable{x} \coqdockw{with}\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqref{Coqdoc.bug5648.A}{\coqdocconstructor{A}} \ensuremath{\Rightarrow} 0\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqref{Coqdoc.bug5648.Add}{\coqdocconstructor{Add}} \ensuremath{\Rightarrow} 1\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqref{Coqdoc.bug5648.G}{\coqdocconstructor{G}} \ensuremath{\Rightarrow} 2\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqref{Coqdoc.bug5648.Goal}{\coqdocconstructor{Goal}} \ensuremath{\Rightarrow} 3\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqref{Coqdoc.bug5648.L}{\coqdocconstructor{L}} \ensuremath{\Rightarrow} 4\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqref{Coqdoc.bug5648.Lemma}{\coqdocconstructor{Lemma}} \ensuremath{\Rightarrow} 5\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqref{Coqdoc.bug5648.P}{\coqdocconstructor{P}} \ensuremath{\Rightarrow} 6\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqref{Coqdoc.bug5648.Proof}{\coqdocconstructor{Proof}} \ensuremath{\Rightarrow} 7\coqdoceol +\coqdocindent{1.00em} +\coqdockw{end}.\coqdoceol +\end{coqdoccode} +\end{document} diff --git a/test-suite/coqdoc/bug5648.v b/test-suite/coqdoc/bug5648.v new file mode 100644 index 0000000000..9b62dd1e1e --- /dev/null +++ b/test-suite/coqdoc/bug5648.v @@ -0,0 +1,19 @@ +Lemma a : True. +Proof. +auto. +Qed. + +Variant t := +| A | Add | G | Goal | L | Lemma | P | Proof . + +Definition d x := + match x with + | A => 0 + | Add => 1 + | G => 2 + | Goal => 3 + | L => 4 + | Lemma => 5 + | P => 6 + | Proof => 7 + end. diff --git a/test-suite/coqdoc/links.html.out b/test-suite/coqdoc/links.html.out new file mode 100644 index 0000000000..7d7d01c1b4 --- /dev/null +++ b/test-suite/coqdoc/links.html.out @@ -0,0 +1,206 @@ +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" +"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> +<html xmlns="http://www.w3.org/1999/xhtml"> +<head> +<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1" /> +<link href="coqdoc.css" rel="stylesheet" type="text/css" /> +<title>Coqdoc.links</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library Coqdoc.links</h1> + +<div class="code"> +</div> + +<div class="doc"> +Various checks for coqdoc + +<div class="paragraph"> </div> + +<ul class="doclist"> +<li> symbols should not be inlined in string g + +</li> +<li> links to both kinds of notations in a' should work to the right notation + +</li> +<li> with utf8 option, forall must be unicode + +</li> +<li> splitting between symbols and ident should be correct in a' and c + +</li> +<li> ".." should be rendered correctly + +</li> +</ul> + +</div> +<div class="code"> + +<br/> +<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Strings.String.html#"><span class="id" title="library">String</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="g"><span class="id" title="definition">g</span></a> := "dfjkh""sdfhj forall <> * ~"%<span class="id" title="var">string</span>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="a"><span class="id" title="definition">a</span></a> (<span class="id" title="var">b</span>: <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) := <a class="idref" href="Coqdoc.links.html#b"><span class="id" title="variable">b</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="f"><span class="id" title="definition">f</span></a> := <span class="id" title="keyword">forall</span> <span class="id" title="var">C</span>:<span class="id" title="keyword">Prop</span>, <a class="idref" href="Coqdoc.links.html#C"><span class="id" title="variable">C</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">"</span></a>n ++ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>).<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">"</span></a>n ++ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#mult"><span class="id" title="abbreviation">mult</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>). +<br/> +<span class="id" title="keyword">Notation</span> <a name="6b97e27793a3d22f5c0d1dd63170fd68"><span class="id" title="notation">"</span></a>n ** m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60).<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="3e01fbae4590c7b7699ff99ce61580e1"><span class="id" title="notation">"</span></a>n ▵ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60).<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">"</span></a>n '_' ++ 'x' m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 3).<br/> + +<br/> +<span class="id" title="keyword">Inductive</span> <a name="eq"><span class="id" title="inductive">eq</span></a> (<span class="id" title="var">A</span>:<span class="id" title="keyword">Type</span>) (<span class="id" title="var">x</span>:<a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a>) : <span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">-></span></a> <span class="id" title="keyword">Prop</span> := <a name="eq_refl"><span class="id" title="constructor">eq_refl</span></a> : <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:></span></a><a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a><br/> +<br/> +<span class="id" title="keyword">where</span> <a name="8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">"</span></a>x = y :> A" := (@<a class="idref" href="Coqdoc.links.html#eq"><span class="id" title="variable">eq</span></a> <span class="id" title="var">A</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) : <span class="id" title="var">type_scope</span>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="eq0"><span class="id" title="definition">eq0</span></a> := 0 <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:></span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="548d1059c499c9b2a9b95b07e68c2090"><span class="id" title="notation">"</span></a>( x # y ; .. ; z )" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#pair"><span class="id" title="constructor">pair</span></a> .. (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#pair"><span class="id" title="constructor">pair</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) .. <span class="id" title="var">z</span>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="9f5a1d89cbd4d38f5e289576db7123d1"><span class="id" title="definition">b_α</span></a> := <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="Coqdoc.links.html#548d1059c499c9b2a9b95b07e68c2090"><span class="id" title="notation">(</span></a>0<a class="idref" href="Coqdoc.links.html#548d1059c499c9b2a9b95b07e68c2090"><span class="id" title="notation">#</span></a>0<a class="idref" href="Coqdoc.links.html#548d1059c499c9b2a9b95b07e68c2090"><span class="id" title="notation">;</span></a>0<a class="idref" href="Coqdoc.links.html#548d1059c499c9b2a9b95b07e68c2090"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a>0 <a class="idref" href="Coqdoc.links.html#6b97e27793a3d22f5c0d1dd63170fd68"><span class="id" title="notation">**</span></a> 0<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">))</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="h"><span class="id" title="abbreviation">h</span></a> := <a class="idref" href="Coqdoc.links.html#a"><span class="id" title="definition">a</span></a>.<br/> + +<br/> + <span class="id" title="keyword">Section</span> <a name="test"><span class="id" title="section">test</span></a>.<br/> + +<br/> + <span class="id" title="keyword">Variables</span> <a name="test.b'"><span class="id" title="variable">b'</span></a> <a name="test.b2"><span class="id" title="variable">b2</span></a>: <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> + +<br/> + <span class="id" title="keyword">Notation</span> <a name="4ab0449b36c75cf94e08c5822ea83e3d"><span class="id" title="notation">"</span></a>n + m" := (<span class="id" title="var">n</span> <a class="idref" href="Coqdoc.links.html#3e01fbae4590c7b7699ff99ce61580e1"><span class="id" title="notation">▵</span></a> <span class="id" title="var">m</span>) : <span class="id" title="var">my_scope</span>.<br/> + +<br/> + <span class="id" title="keyword">Delimit</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">my_scope</span> <span class="id" title="keyword">with</span> <span class="id" title="var">my</span>.<br/> + +<br/> + <span class="id" title="keyword">Notation</span> <a name="l"><span class="id" title="abbreviation">l</span></a> := 0.<br/> + +<br/> + <span class="id" title="keyword">Definition</span> <a name="ab410a966ac148e9b78c65c6cdf301fd"><span class="id" title="definition">α</span></a> := (0 <a class="idref" href="Coqdoc.links.html#4ab0449b36c75cf94e08c5822ea83e3d"><span class="id" title="notation">+</span></a> <a class="idref" href="Coqdoc.links.html#l"><span class="id" title="abbreviation">l</span></a>)%<span class="id" title="var">my</span>.<br/> + +<br/> + <span class="id" title="keyword">Definition</span> <a name="a'"><span class="id" title="definition">a'</span></a> <span class="id" title="var">b</span> := <a class="idref" href="Coqdoc.links.html#test.b'"><span class="id" title="variable">b'</span></a><a class="idref" href="Coqdoc.links.html#1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">++</span></a>0<a class="idref" href="Coqdoc.links.html#1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">++</span></a><a class="idref" href="Coqdoc.links.html#test.b2"><span class="id" title="variable">b2</span></a> <a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">_</span></a> <a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">++</span></a><a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">x</span></a> <a class="idref" href="Coqdoc.links.html#b"><span class="id" title="variable">b</span></a>.<br/> + +<br/> + <span class="id" title="keyword">Definition</span> <a name="c"><span class="id" title="definition">c</span></a> := <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#5bf2050e90b21ebc82dc5463d1ba338e"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#5bf2050e90b21ebc82dc5463d1ba338e"><span class="id" title="notation">}+{</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#5bf2050e90b21ebc82dc5463d1ba338e"><span class="id" title="notation">}</span></a>.<br/> + +<br/> + <span class="id" title="keyword">Definition</span> <a name="d"><span class="id" title="definition">d</span></a> := (1<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#b3eea360671e1b32b18a26e15b3aace3"><span class="id" title="notation">+</span></a>2)%<span class="id" title="var">nat</span>.<br/> + +<br/> + <span class="id" title="keyword">Lemma</span> <a name="e"><span class="id" title="lemma">e</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#3dcaec3b772747610227247939f96b01"><span class="id" title="notation">+</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> + <span class="id" title="var">Admitted</span>.<br/> + +<br/> + <span class="id" title="keyword">End</span> <a class="idref" href="Coqdoc.links.html#test"><span class="id" title="section">test</span></a>.<br/> + +<br/> + <span class="id" title="keyword">Section</span> <a name="test2"><span class="id" title="section">test2</span></a>.<br/> + +<br/> + <span class="id" title="keyword">Variables</span> <a name="test2.b'"><span class="id" title="variable">b'</span></a>: <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> + +<br/> + <span class="id" title="keyword">Section</span> <a name="test2.test"><span class="id" title="section">test</span></a>.<br/> + +<br/> + <span class="id" title="keyword">Variables</span> <a name="test2.test.b2"><span class="id" title="variable">b2</span></a>: <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> + +<br/> + <span class="id" title="keyword">Definition</span> <a name="a''"><span class="id" title="definition">a''</span></a> <span class="id" title="var">b</span> := <a class="idref" href="Coqdoc.links.html#test2.b'"><span class="id" title="variable">b'</span></a> <a class="idref" href="Coqdoc.links.html#1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">++</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#O"><span class="id" title="constructor">O</span></a> <a class="idref" href="Coqdoc.links.html#1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">++</span></a> <a class="idref" href="Coqdoc.links.html#test2.test.b2"><span class="id" title="variable">b2</span></a> <a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">_</span></a> <a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">++</span></a> <a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">x</span></a> <a class="idref" href="Coqdoc.links.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#b3eea360671e1b32b18a26e15b3aace3"><span class="id" title="notation">+</span></a> <a class="idref" href="Coqdoc.links.html#h"><span class="id" title="abbreviation">h</span></a> 0.<br/> + +<br/> + <span class="id" title="keyword">End</span> <a class="idref" href="Coqdoc.links.html#test2.test"><span class="id" title="section">test</span></a>.<br/> + +<br/> + <span class="id" title="keyword">End</span> <a class="idref" href="Coqdoc.links.html#test2"><span class="id" title="section">test2</span></a>.<br/> + +<br/> +</div> + +<div class="doc"> +skip +<div class="paragraph"> </div> + + skip +<div class="paragraph"> </div> + + skip +<div class="paragraph"> </div> + + skip +<div class="paragraph"> </div> + + skip +<div class="paragraph"> </div> + + skip +<div class="paragraph"> </div> + + skip +<div class="paragraph"> </div> + + skip +<div class="paragraph"> </div> + + skip +<div class="paragraph"> </div> + + skip +<div class="paragraph"> </div> + + skip +<div class="paragraph"> </div> + + skip +<div class="paragraph"> </div> + + skip +<div class="paragraph"> </div> + + skip +</div> +<div class="code"> + +<br/> +</div> +</div> + +<div id="footer"> +<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> +</div> + +</div> + +</body> +</html>
\ No newline at end of file diff --git a/test-suite/coqdoc/links.tex.out b/test-suite/coqdoc/links.tex.out new file mode 100644 index 0000000000..844fb3031c --- /dev/null +++ b/test-suite/coqdoc/links.tex.out @@ -0,0 +1,162 @@ +\documentclass[12pt]{report} +\usepackage[]{inputenc} +\usepackage[T1]{fontenc} +\usepackage{fullpage} +\usepackage{coqdoc} +\usepackage{amsmath,amssymb} +\usepackage{url} +\begin{document} +\coqlibrary{Coqdoc.links}{Library }{Coqdoc.links} + +\begin{coqdoccode} +\end{coqdoccode} +Various checks for coqdoc + + + +\begin{itemize} +\item symbols should not be inlined in string g + +\item links to both kinds of notations in a' should work to the right notation + +\item with utf8 option, forall must be unicode + +\item splitting between symbols and ident should be correct in a' and c + +\item ``..'' should be rendered correctly + +\end{itemize} +\begin{coqdoccode} +\coqdocemptyline +\coqdocnoindent +\coqdockw{Require} \coqdockw{Import} \coqexternalref{}{http://coq.inria.fr/stdlib/Coq.Strings.String}{\coqdoclibrary{String}}.\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.links.g}{g}{\coqdocdefinition{g}} := "dfjkh""sdfhj forall <> * \~{}"\%\coqdocvar{string}.\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.links.a}{a}{\coqdocdefinition{a}} (\coqdocvar{b}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}) := \coqdocvariable{b}.\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.links.f}{f}{\coqdocdefinition{f}} := \coqdockw{\ensuremath{\forall}} \coqdocvar{C}:\coqdockw{Prop}, \coqdocvariable{C}.\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Notation} \coqdef{Coqdoc.links.::x '++' x}{"}{"}n ++ m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}).\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Notation} \coqdef{Coqdoc.links.::x '++' x}{"}{"}n ++ m" := (\coqexternalref{mult}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{mult}} \coqdocvar{n} \coqdocvar{m}). \coqdocemptyline +\coqdocnoindent +\coqdockw{Notation} \coqdef{Coqdoc.links.::x '**' x}{"}{"}n ** m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 60).\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Notation} \coqdef{Coqdoc.links.::x 'xE2x96xB5' x}{"}{"}n ▵ m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 60).\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Notation} \coqdef{Coqdoc.links.::x ''' ''' '++' 'x' x}{"}{"}n '\_' ++ 'x' m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 3).\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Inductive} \coqdef{Coqdoc.links.eq}{eq}{\coqdocinductive{eq}} (\coqdocvar{A}:\coqdockw{Type}) (\coqdocvar{x}:\coqdocvariable{A}) : \coqdocvar{A} \coqexternalref{:type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqdockw{Prop} := \coqdef{Coqdoc.links.eq refl}{eq\_refl}{\coqdocconstructor{eq\_refl}} : \coqdocvariable{x} \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{=}} \coqdocvariable{x} \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{:>}}\coqdocvariable{A}\coqdoceol +\coqdocnoindent +\coqdoceol +\coqdocnoindent +\coqdockw{where} \coqdef{Coqdoc.links.:type scope:x '=' x ':>' x}{"}{"}x = y :> A" := (@\coqdocvariable{eq} \coqdocvar{A} \coqdocvar{x} \coqdocvar{y}) : \coqdocvar{type\_scope}.\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.links.eq0}{eq0}{\coqdocdefinition{eq0}} := 0 \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{=}} 0 \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{:>}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Notation} \coqdef{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{"}{"}( x \# y ; .. ; z )" := (\coqexternalref{pair}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{pair}} .. (\coqexternalref{pair}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{pair}} \coqdocvar{x} \coqdocvar{y}) .. \coqdocvar{z}).\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.links.b xCExB1}{b\_α}{\coqdocdefinition{b\_α}} := \coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{(}}\coqref{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{(}}0\coqref{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{\#}}0\coqref{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{;}}0\coqref{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{)}} \coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{,}} \coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{(}}0 \coqref{Coqdoc.links.::x '**' x}{\coqdocnotation{**}} 0\coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{))}}.\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdockw{Notation} \coqdef{Coqdoc.links.h}{h}{\coqdocabbreviation{h}} := \coqref{Coqdoc.links.a}{\coqdocdefinition{a}}.\coqdoceol +\coqdocemptyline +\coqdocindent{1.00em} +\coqdockw{Section} \coqdef{Coqdoc.links.test}{test}{\coqdocsection{test}}.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Variables} \coqdef{Coqdoc.links.test.b'}{b'}{\coqdocvariable{b'}} \coqdef{Coqdoc.links.test.b2}{b2}{\coqdocvariable{b2}}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Notation} \coqdef{Coqdoc.links.test.:my scope:x '+' x}{"}{"}n + m" := (\coqdocvar{n} \coqref{Coqdoc.links.::x 'xE2x96xB5' x}{\coqdocnotation{▵}} \coqdocvar{m}) : \coqdocvar{my\_scope}.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Delimit} \coqdockw{Scope} \coqdocvar{my\_scope} \coqdockw{with} \coqdocvar{my}.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Notation} \coqdef{Coqdoc.links.l}{l}{\coqdocabbreviation{l}} := 0.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Definition} \coqdef{Coqdoc.links.xCExB1}{α}{\coqdocdefinition{α}} := (0 \coqref{Coqdoc.links.test.:my scope:x '+' x}{\coqdocnotation{+}} \coqref{Coqdoc.links.l}{\coqdocabbreviation{l}})\%\coqdocvar{my}.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Definition} \coqdef{Coqdoc.links.a'}{a'}{\coqdocdefinition{a'}} \coqdocvar{b} := \coqdocvariable{b'}\coqref{Coqdoc.links.::x '++' x}{\coqdocnotation{++}}0\coqref{Coqdoc.links.::x '++' x}{\coqdocnotation{++}}\coqdocvariable{b2} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{++}}\coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqdocvariable{b}.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Definition} \coqdef{Coqdoc.links.c}{c}{\coqdocdefinition{c}} := \coqexternalref{:type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\{}}\coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}\coqexternalref{:type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\}+\{}}\coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}\coqexternalref{:type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\}}}.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Definition} \coqdef{Coqdoc.links.d}{d}{\coqdocdefinition{d}} := (1\coqexternalref{:nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}}2)\%\coqdocvar{nat}.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Lemma} \coqdef{Coqdoc.links.e}{e}{\coqdoclemma{e}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} \coqexternalref{:type scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{+}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol +\coqdocindent{2.00em} +\coqdocvar{Admitted}.\coqdoceol +\coqdocemptyline +\coqdocindent{1.00em} +\coqdockw{End} \coqref{Coqdoc.links.test}{\coqdocsection{test}}.\coqdoceol +\coqdocemptyline +\coqdocindent{1.00em} +\coqdockw{Section} \coqdef{Coqdoc.links.test2}{test2}{\coqdocsection{test2}}.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Variables} \coqdef{Coqdoc.links.test2.b'}{b'}{\coqdocvariable{b'}}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{Section} \coqdef{Coqdoc.links.test2.test}{test}{\coqdocsection{test}}.\coqdoceol +\coqdocemptyline +\coqdocindent{3.00em} +\coqdockw{Variables} \coqdef{Coqdoc.links.test2.test.b2}{b2}{\coqdocvariable{b2}}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol +\coqdocemptyline +\coqdocindent{3.00em} +\coqdockw{Definition} \coqdef{Coqdoc.links.a''}{a'{}'}{\coqdocdefinition{a'{}'}} \coqdocvar{b} := \coqdocvariable{b'} \coqref{Coqdoc.links.::x '++' x}{\coqdocnotation{++}} \coqexternalref{O}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{O}} \coqref{Coqdoc.links.::x '++' x}{\coqdocnotation{++}} \coqdocvariable{b2} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{++}} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqdocvariable{b} \coqexternalref{:nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}} \coqref{Coqdoc.links.h}{\coqdocabbreviation{h}} 0.\coqdoceol +\coqdocemptyline +\coqdocindent{2.00em} +\coqdockw{End} \coqref{Coqdoc.links.test2.test}{\coqdocsection{test}}.\coqdoceol +\coqdocemptyline +\coqdocindent{1.00em} +\coqdockw{End} \coqref{Coqdoc.links.test2}{\coqdocsection{test2}}.\coqdoceol +\coqdocemptyline +\end{coqdoccode} +skip + + skip + + skip + + skip + + skip + + skip + + skip + + skip + + skip + + skip + + skip + + skip + + skip + + skip \begin{coqdoccode} +\coqdocemptyline +\end{coqdoccode} +\end{document} diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v index ebf817cfc5..0ee85712e2 100644 --- a/test-suite/success/cumulativity.v +++ b/test-suite/success/cumulativity.v @@ -1,5 +1,11 @@ +Polymorphic Cumulative Inductive T1 := t1 : T1. +Fail Monomorphic Cumulative Inductive T2 := t2 : T2. + +Polymorphic Cumulative Record R1 := { r1 : T1 }. +Fail Monomorphic Cumulative Inductive R2 := {r2 : T1}. + Set Universe Polymorphism. -Set Inductive Cumulativity. +Set Polymorphic Inductive Cumulativity. Set Printing Universes. Inductive List (A: Type) := nil | cons : A -> List A -> List A. @@ -62,4 +68,33 @@ End subtyping_test. Record A : Type := { a :> Type; }. -Record B (X : A) : Type := { b : X; }.
\ No newline at end of file +Record B (X : A) : Type := { b : X; }. + +NonCumulative Inductive NCList (A: Type) + := ncnil | nccons : A -> NCList A -> NCList A. + +Section NCListLift. + Universe i j. + + Constraint i < j. + + Fail Definition LiftNCL {A} : NCList@{i} A -> NCList@{j} A := fun x => x. + +End NCListLift. + +Inductive eq@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := eq_refl : eq x x. + +Definition funext_type@{a b e} (A : Type@{a}) (B : A -> Type@{b}) + := forall f g : (forall a, B a), + (forall x, eq@{e} (f x) (g x)) + -> eq@{e} f g. + +Section down. + Universes a b e e'. + Constraint e' < e. + Lemma funext_down {A B} + : @funext_type@{a b e} A B -> @funext_type@{a b e'} A B. + Proof. + intros H f g Hfg. exact (H f g Hfg). + Defined. +End down. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index e54ea45d41..3a8ca7b8d6 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -170,7 +170,7 @@ COQMAKEFILE_VERSION:=@COQ_VERSION@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") -CAMLFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) +CAMLFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) $(OCAML_API_FLAGS) CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 327f53520c..0f38d19386 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -203,8 +203,12 @@ let generate_conf_coq_config oc args bypass_API = section oc "Coq configuration."; let src_dirs = if bypass_API then Coq_config.all_src_dirs - else Coq_config.api_dirs @ Coq_config.plugins_dirs @ ["-open API"] in + else Coq_config.api_dirs @ Coq_config.plugins_dirs in Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs; + if bypass_API then + Printf.fprintf oc "OCAML_API_FLAGS=\n" + else + Printf.fprintf oc "OCAML_API_FLAGS=-open API\n"; fprintf oc "COQMF_WINDRIVE=%s\n" (windrive Coq_config.coqlib) ;; diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 5c0d2a39b0..d043c4a584 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -693,25 +693,21 @@ module Html = struct printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s) let ident s loc = - if is_keyword s then begin - printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s) - end else begin - try - match loc with - | None -> raise Not_found - | Some loc -> - reference (translate s) (Index.find (get_module false) loc) - with Not_found -> - if is_tactic s then - printf "<span class=\"id\" title=\"tactic\">%s</span>" (translate s) - else - if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) - then - try reference (translate s) (Index.find_string (get_module false) s) - with _ -> Tokens.output_tagged_ident_string s - else - Tokens.output_tagged_ident_string s - end + try + match loc with + | None -> raise Not_found + | Some loc -> + reference (translate s) (Index.find (get_module false) loc) + with Not_found -> + if is_tactic s then + printf "<span class=\"id\" title=\"tactic\">%s</span>" (translate s) + else if is_keyword s then + printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s) + else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) then + try reference (translate s) (Index.find_string (get_module false) s) + with Not_found -> Tokens.output_tagged_ident_string s + else + Tokens.output_tagged_ident_string s let proofbox () = printf "<font size=-2>☐</font>" diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 28aeaa725e..a4fe49020a 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -650,7 +650,7 @@ let declare_obligation prg obl body ty uctx = let constant = Declare.declare_constant obl.obl_name ~local:true (DefinitionEntry ce,IsProof Property) in - if not opaque then add_hint false prg constant; + if not opaque then add_hint (Locality.make_section_locality None) prg constant; definition_message obl.obl_name; true, { obl with obl_body = if poly then diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index adf24d23b1..4f63ed6f48 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -522,7 +522,21 @@ let vernac_assumption locality poly (local, kind) l nl = let status = do_assumptions kind nl l in if not status then Feedback.feedback Feedback.AddedAxiom +let should_treat_as_cumulative cum poly = + if poly then + match cum with + | GlobalCumulativity | LocalCumulativity -> true + | GlobalNonCumulativity | LocalNonCumulativity -> false + else + match cum with + | GlobalCumulativity | GlobalNonCumulativity -> false + | LocalCumulativity -> + user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.") + | LocalNonCumulativity -> + user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.") + let vernac_record cum k poly finite struc binders sort nameopt cfs = + let is_cumulative = should_treat_as_cumulative cum poly in let const = match nameopt with | None -> add_prefix "Build_" (snd (fst (snd struc))) | Some (_,id as lid) -> @@ -533,13 +547,14 @@ let vernac_record cum k poly finite struc binders sort nameopt cfs = match x with | Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj" | _ -> ()) cfs); - ignore(Record.definition_structure (k,cum,poly,finite,struc,binders,cfs,const,sort)) + ignore(Record.definition_structure (k,is_cumulative,poly,finite,struc,binders,cfs,const,sort)) (** When [poly] is true the type is declared polymorphic. When [lo] is true, then the type is declared private (as per the [Private] keyword). [finite] indicates whether the type is inductive, co-inductive or neither. *) let vernac_inductive cum poly lo finite indl = + let is_cumulative = should_treat_as_cumulative cum poly in if Dumpglob.dump () then List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) -> match cstrs with @@ -576,7 +591,7 @@ let vernac_inductive cum poly lo finite indl = | _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.") in let indl = List.map unpack indl in - do_mutual_inductive indl cum poly lo finite + do_mutual_inductive indl is_cumulative poly lo finite let vernac_fixpoint locality poly local l = let local = enforce_locality_exp locality local in @@ -1363,10 +1378,10 @@ let _ = let _ = declare_bool_option { optdepr = false; - optname = "inductive cumulativity"; - optkey = ["Inductive"; "Cumulativity"]; - optread = Flags.is_inductive_cumulativity; - optwrite = Flags.make_inductive_cumulativity } + optname = "Polymorphic inductive cumulativity"; + optkey = ["Polymorphic"; "Inductive"; "Cumulativity"]; + optread = Flags.is_polymorphic_inductive_cumulativity; + optwrite = Flags.make_polymorphic_inductive_cumulativity } let _ = declare_int_option |