aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Uniformisation in the documentation: remove the use of 'coinductive' inGravatar aspiwack2012-04-13
| | | | | | favour of 'co-inductive'. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15162 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation of records defined with the keywords Inductive andGravatar aspiwack2012-04-13
| | | | | | CoInductive. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15161 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restores pdf bookmarks in the reference manual.Gravatar aspiwack2012-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15160 85f007b7-540e-0410-9357-904b9bb8a0f7
* Better error message when defining recursive records with Record orGravatar aspiwack2012-04-13
| | | | | | Structure. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15159 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed syntax BeginSubproof/EndSubproof. It has been replaced byGravatar aspiwack2012-04-13
| | | | | | | | braces ( { / } ). BeginSuproof n (where n is a goal number) can be replaced by Focus n. { . git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15158 85f007b7-540e-0410-9357-904b9bb8a0f7
* Browser documentation & CharSet under WindowsGravatar pboutill2012-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15157 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove print call that do not use the pp mechanismGravatar pboutill2012-04-12
| | | | | | Signed-off-by: Edward Z. Yang <ezyang@mit.edu> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15148 85f007b7-540e-0410-9357-904b9bb8a0f7
* make otags only relies on otagsGravatar pboutill2012-04-12
| | | | | | but it requires otags-3.12.2 and and ./configure -usecamlp4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15147 85f007b7-540e-0410-9357-904b9bb8a0f7
* "A -> B" is a notation for "forall _ : A, B".Gravatar pboutill2012-04-12
| | | | | | | No good reason for that except uniformity so revert this commit if you find a reason against it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15146 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide minor enhancementsGravatar pboutill2012-04-12
| | | | | | | | | | | | Bug 2736: Syntax highlighting 600 transitions left before ocamllex limit. A preference pane large enough to change fonts. Erase extra empty line in Coqide goal display. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15145 85f007b7-540e-0410-9357-904b9bb8a0f7
* lib directory is cut in 2 cma.Gravatar pboutill2012-04-12
| | | | | | | | | | | | | | | - Clib that does not depend on camlpX and is made to be shared by all coq tools/scripts/... - Lib that is Coqtop specific As a side effect for the build system : - Coq_config is in Clib and does not appears in makefiles - only the BEST version of coqc and coqmktop is made - ocamlbuild build system fails latter but is still broken (ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15144 85f007b7-540e-0410-9357-904b9bb8a0f7
* Repair two testsGravatar letouzey2012-04-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15131 85f007b7-540e-0410-9357-904b9bb8a0f7
* CHANGES: adapt after backport of some features to 8.4Gravatar letouzey2012-04-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15130 85f007b7-540e-0410-9357-904b9bb8a0f7
* remove plugins/subtac/subtac.ml reintroduced by mistaked in a previous commitGravatar letouzey2012-04-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15129 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a reset button for CoqIDE colorsGravatar ppedrot2012-04-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15128 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a background color configuration option in CoqIDE.Gravatar ppedrot2012-04-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15127 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing the "capture" check newly introduced in r15122 whenGravatar herbelin2012-04-07
| | | | | | | | | | internalizing declaration of contexts of the form "(x y : P x)": - don't forget to catch the error in intern_context; - check capture on glob_constr rather than constr_expr so that binders possibly introduced by notations are recognized as such; - give a more expressive error message. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15123 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unifying the different procedures for interning binders.Gravatar herbelin2012-04-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15122 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing a few bugs (see #2571) related to interpretation of multiple bindersGravatar herbelin2012-04-06
| | | | | | | | | | | | | | | | | | | | | | | | - fixing missing spaces in the format of the exists' notations (Logic.v); - fixing wrong variable name in check_is_hole error message (topconstr.ml); - interpret expressions with open binders such as "forall x y, t" as "forall (x:_) (y:_),t" instead of "forall (x y:_),t" to avoid the "implicit type" of a variable being propagated to the type of another variable of different base name. An open question remains: when writing explicitly "forall (x y:_),t", should the types of x and y be the same or not. To avoid the "bug" that x and y have implicit types but the one of x takes precedences, I enforced the interpretation (in constrintern, not in parsing) that "forall (x y:_),t" means the same as "forall (x:_) (y:_),t". However, another choice could have been made. Then one would have to check that if x and y have implicit types, they are the same; also, glob_constr should ideally be changed to support a GProd and GLam with multiple names in the same type, especially if this type is an evar. On the contrary, one might also want e.g. "forall x y : list _, t" to mean "forall (x:list _) (y:list _), t" with distinct instanciations of "_" ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15121 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing Dhyp from debugger.Gravatar herbelin2012-04-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15120 85f007b7-540e-0410-9357-904b9bb8a0f7
* Shortcuts and optimizations of comparisonsGravatar xclerc2012-04-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15118 85f007b7-540e-0410-9357-904b9bb8a0f7
* Relax uniform inheritance conditionGravatar gareuselesinge2012-04-05
| | | | | | | Uniform inheritance is not always needed for the coercion mechanism to work. We turn it into a warning. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15117 85f007b7-540e-0410-9357-904b9bb8a0f7
* Speedup free_vars_and_rels_up_alias_expansion (evarconv)Gravatar gareuselesinge2012-04-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Small cache to avoid checking the same Rel or Var twice. Consider an unification problem like the following one: a := huge b := F1 a + F2 a c := G1 b + G2 b =============== ?i[c,b,a] == ?g[c,c,c] The old code, as the "not optimal" comment was suggesting, did process every item in the explicit substitution, even duplicated ones, unfolding the letins over and over. This was the cause of the huge slowdown in the definition of cormen_lup in Ssreflect/theories/matrix.v, that follows: Fixpoint cormen_lup {n} := match n return let M := 'M[F]_n.+1 in M -> M * M * M with | 0 => fun A => (1, 1, A) | _.+1 => fun A => let k := odflt 0 [pick k | A k 0 != 0] in let A1 : 'M_(1 + _) := xrow 0 k A in let P1 : 'M_(1 + _) := tperm_mx 0 k in let Schur := ((A k 0)^-1 *: dlsubmx A1) *m ursubmx A1 in let: (P2, L2, U2) := cormen_lup (drsubmx A1 - Schur) in let P := block_mx 1 0 0 P2 *m P1 in let L := block_mx 1 0 ((A k 0)^-1 *: (P2 *m dlsubmx A1)) L2 in let U := block_mx (ulsubmx A1) (ursubmx A1) 0 U2 in (P, L, U) end. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15116 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reversed colour highlight in CoqIDEGravatar ppedrot2012-04-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15113 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo in a message.Gravatar aspiwack2012-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15105 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a command "Unfocused" which returns an error when the proof isGravatar aspiwack2012-03-30
| | | | | | not fully unfocused (in the style of the Guarded command). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15104 85f007b7-540e-0410-9357-904b9bb8a0f7
* info_trivial, info_auto, info_eauto, and debug (trivial|auto)Gravatar letouzey2012-03-30
| | | | | | | | | | | | | | | | | | | | | | | To mitigate the lack of a general "info" tactical, let's introduce some specialized tactics info_trivial, info_auto and info_eauto that display the basic tactics used when solving a goal. We also add tactics "debug trivial" and "debug auto" which display every basic tactics attempted by trivial or auto. Triggering the "info" or "debug" mode for auto, eauto, trivial can also be done now via global options, such as Set Debug Auto or Set Info Eauto. In case both debug and info modes are activated, the debug mode takes precedence. NB: it would be nice to name these tactics "info xxx" instead of "info_xxx", but I don't see how to implement a "info eauto" in eauto.ml4 (hence by TACTIC EXTEND) while keeping a generic "info foo" tactic in g_ltac.ml4 (useful to display a nice message about the unavailability of the general info). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15103 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove code of obsolete tactics : superauto, autotdb, cdhyp, dhyp, dconclGravatar letouzey2012-03-30
| | | | | | No grammar entries for these tactics since coq 8.0 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15102 85f007b7-540e-0410-9357-904b9bb8a0f7
* A revolution has come: CoqIDE, now in color. Fixes bug #2704 btw.Gravatar ppedrot2012-03-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15101 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adapt the checker after commit 15080Gravatar letouzey2012-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15100 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unification: Fixing bug in materialize_evar (spotted by MathClasses).Gravatar herbelin2012-03-26
| | | | | | Also fixed apparent other bug in the presence of let-ins. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15099 85f007b7-540e-0410-9357-904b9bb8a0f7
* Slight change in the semantics of arguments scopes: scopes can noGravatar herbelin2012-03-26
| | | | | | | | | | | longer be bound to Funclass or Sortclass (this does not seem to be useful). [An exception is when using modules, if a constant foo is expanded into a type, a "Bind Scope sc with foo" starts binding Sortclass]. Also reworked reference manual for Arguments Scopes and Bind Scopes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15098 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing printing level of Utf8 equivalent for ->.Gravatar herbelin2012-03-26
| | | | | | | Parsing with rhs at level 200 was already working thanks to I don't which unexpected magic from camlp4/5. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15096 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing deactivation of scope at printing time in the body of aGravatar herbelin2012-03-26
| | | | | | | lam or prod to be consistent with what is done at parsing time (see coq-club on 25/3/2012). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15093 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unification: Added a heuristic to solve problems of the formGravatar herbelin2012-03-26
| | | | | | | | | | | | | | | | | | ?x[t1..tm] = ?y[u1..un] when ?x occurs in u1..un with no (easy) way to know if it occurs in rigid position or not. Such equations typically come from matching problems such as "match a return ?T[a] with pair a1 a2 => a1 end" where, a is in type "?A * ?B", and, in the branch, the return clause, of the form "?T[pair ?A ?B a1 a2]", has to be unified with ?A. This possible dependency is kept since commits r15060-15062. The heuristic is to restrict ?T so that the dependency is removed, leading to a behavior similar to the one existing before these commits. This allows BGsection15.v, from contrib Ssreflect, to compile as it did before these commits. Also, removed one function exported without true need in r15061. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15092 85f007b7-540e-0410-9357-904b9bb8a0f7
* Module names and constant/inductive names are now in two separate namespacesGravatar letouzey2012-03-26
| | | | | | | | | | | | | | We now accept the following code: Definition E := 0. Module E. End E. Techically, we simply allow the same label to occur at most twice in a structure_body, which is a (label * structure_field_body) list). These two label occurences should not be at the same level of fields (e.g. a SFBmodule and a SFBmind are ok, but not two SFBmodule's or a SFBmodule and a SFBmodtype). Gain : a minimal amount of code change. Drawback : no more simple List.assoc or equivalent should be performed on a structure_body ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15088 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix the test-suite by removing any Reset in the scriptsGravatar letouzey2012-03-23
| | | | | | | | Reset and the other backtracking commands (Back, BackTo, Backtrack) are now allowed only during interactive session, not in compiled or loaded scripts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15087 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation of last commit concerning BacktrackingGravatar letouzey2012-03-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15086 85f007b7-540e-0410-9357-904b9bb8a0f7
* A unified backtrack mechanism, with a basic "Show Script" as side-effectGravatar letouzey2012-03-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Migrate the backtracking code from ide_slave.ml into a new backtrack.ml. In particular the history stack of commands that used to be there is now non-coqide-specific. ** Adapted commands ** - "Show Script": a basic functional version is restored (and the printing of scripts at Qed in coqtop). No indentation, one Coq command per line, based on the vernac_expr asts recorded in the history stack, printed via Ppvernac. - "Back n" : now mimics the backtrack of coqide: it goes n steps back (both commands and proofs), and maybe more if needed to avoid re-entering a proof (it outputs a warning in this case). - "BackTo n" : still try to go back to state n, but it also handles the proof state, and it may end on some state n' <= n if needed to avoid re-entering a proof. Ideally, it could someday be used by ProofGeneral instead of the complex Backtrack command. ** Compatible commands ** - "Backtrack" is left intact from compatibility with current ProofGeneral. We simply re-synchronize the command history stack after each Backtrack. - "Undo" is kept as a standard command, not a backtracking one, a bit like "Focus". Same for "Restart" and "Abort". All of these are now accepted in coqide (Undo simply triggers a warning). - Undocumented command "Undo To n" (counting from start of proof instead of from end) also keep its semantics, it is simply made compatible with the new stack mechanism. ** New restrictions ** We now forbid backtracking commands (Reset* / Back*) inside files when Load'ing or compiling, or inside VernacList/VernacTime/VernacFail. Too much work dealing with these situation that nobody uses. ** Internal details ** Internally, the command stack differs a bit from what was in Ide_slave earlier (which was inspired by lisp code in ProofGeneral). We now tag commands that are unreachable by a backtrack, due to some proof being finished, aborted, restarted, or partly Undo'ed. This induce a bit of bookkeeping during Qed/Abort/Restart/Undo, but then the backtracking code is straightforward: we simply search backward the first reachable state starting from the desired place. We don't depend anymore on the proof names (apart in the last proof block), It's more robust this way (think of re-entering a M.foo from an outside proof foo). Many internal clarifications in Lib, Vernac, etc. For instance "Reset Initial" is now just a BackTo 1, while "Reset foo" now calls (Lib.label_before_name "foo"), and performs a BackTo to the corresponding label. Concerning Coqide, we directly suppress the regular printing of goals via a flag in Vernacentries. This avoid relying on a classification of commands in Ide_slave as earlier. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15085 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove undocumented command "Delete foo"Gravatar letouzey2012-03-23
| | | | | | | | | This command isn't trivial to port to the forthcoming evolution of backtracking in coqtop. Moreover, it isn't clear whether this "Delete" works well in advanced situation (was not updating frozen states). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15084 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove old proof-managment commands Suspend/ResumeGravatar letouzey2012-03-23
| | | | | | | There're not compatible with the current Backtrack mecanism used both by ProofGeneral and CoqIDE. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15083 85f007b7-540e-0410-9357-904b9bb8a0f7
* Little bug in r15061 leading to unusable debug mode.Gravatar herbelin2012-03-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15082 85f007b7-540e-0410-9357-904b9bb8a0f7
* Univ: enforce_leq instead of enforce_geq for more uniformityGravatar letouzey2012-03-22
| | | | | | Same for check_leq instead of check_geq git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15081 85f007b7-540e-0410-9357-904b9bb8a0f7
* Univ: switch the order of int and dir_path in UniverseLevel.LevelGravatar letouzey2012-03-22
| | | | | | | | Our specialized comparison already handles the int and dir_path in this order. But there may remain some Pervasives.(=) elsewhere in the code, which should benefit from this reordering git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15080 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update of .gitignore (via a regexp g_*.ml)Gravatar letouzey2012-03-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15079 85f007b7-540e-0410-9357-904b9bb8a0f7
* evarconv: MaybeFlex/MaybeFlex case infers more Canonical StructuresGravatar gareuselesinge2012-03-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Canonical Structure inference works on named terms only: i.e. the projection and the value must be named (with few exceptions). The set of named (head) terms is: (Var _|Construct _|Ind _|Const _|Prod _|Sort _) The set of unnamed is thus: (Case _|Fix _|CoFix _|Evar _|Meta _|Rel _) The MaybeFlex/MaybeFlex case, when no CS inference takes place, unfolds the rhs only if it exposes a named term. If it exposes an unnamed term, it tries to unfold on the lhs first. Note that unnamed terms are whd normal terms, since iota and zeta are performed by evar_apprec. So the algorithm behaves as before, but stops unfolding the rhs 1 delta step before it exposes an unnamed term. Then it starts unfolding the lhs. If the lhs exposes a rigid term the rhs is naturally unfolded, going back to same situation in which the algorithm was ending before. But while it unfolds on the left, the rhs is still named, and canonical structure inference can succeed. Ex failing before, the "canon_" prefix marks projections/values declared as canonical. Record test := K { canon_proj : nat } (* canon_proj x := math x with K y => y end *) canon_val x := match x with 0 => 0 | S m => m end Canonical Structure canon_struct x := K (canon_val x) (* aliases *) proj := canon_proj val := canon_val Old alg: proj ? ===?=== val x proj ? ===?=== canon_val x proj ? ===?=== match x with ... end canon_proj ? ===?=== match x with ... end (* no inference *) match ? with K x...end ===?=== match x with 0 ...end (* FAIL *) New alg: proj ? ===?=== val x proj ? ===?=== canon_val x canon_proj ? ===?=== canon_val x (* inference works: ? := canon_struct *) In case canon_struct is not declared for canon_proj and canon_val it continues like that: canon_proj ? ===?=== canon_val x match ? with K x...end ===?=== canon_val x match ? with K x...end ===?=== match x with 0 ...end (* FAIL *) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15077 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ppvernac: nicer printing of proof delimiters { ... }Gravatar letouzey2012-03-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15076 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pfedit: avoid Undoing too muchGravatar letouzey2012-03-21
| | | | | | | | | | | | | | | | | | It seems that we can currently do a successful Undo (but not two!) on a freshly started Lemma. Let's add a depth check on Pfedit.undo to avoid that. This way, we cannot Undo to depth < 1 (with 1 being the initial depth of a lemma). Simplier implementation of Pfedit.restart : it is Pfedit.undo_todepth 1. This extra initial step in the Undo Stack has probably something to see with the Lemma argument introduction. For instance, before this patch we had: Lemma test n : n+0=n. Restart. (* now the goal is universally quantified ! *) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15075 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix interface of resolve_typeclasses: onlyargs -> with_goals:Gravatar msozeau2012-03-20
| | | | | | by default typeclass resolution is not launched on goal evars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15074 85f007b7-540e-0410-9357-904b9bb8a0f7
* Arranged for the desirable behaviour that bullets do not see beyond braces.Gravatar aspiwack2012-03-20
| | | | | | | | | | | i.e.: after a brace is open, one can use the bullets again without clashing with bullets outside the brace. In particular, one can nest bullets with arbitrary depth (by interleaving them with occasional braces). Also fixed a typo introduced in my previous commit which caused bullets and braces to behave just like regular focuses. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15073 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 15:49:01 +0000