]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: c41d664)
λδ site update
authorFerruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Mon, 7 Dec 2020 19:44:36 +0000 (20:44 +0100)
committerFerruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Mon, 7 Dec 2020 19:44:36 +0000 (20:44 +0100)
+ another Unicode character sponsored
+ Helena: minor updates
+ Ground: minor updates

helm/software/helena/src/common/layer.ml patch | blob | history
helm/software/helena/src/toplevel/helena.ml patch | blob | history
helm/www/lambdadelta/images/bronze-03C7.png [new file with mode: 0644] patch | blob
helm/www/lambdadelta/web/home/home.ldw.xml patch | blob | history
matita/matita/contribs/lambdadelta/ground/lib/exteq.ma patch | blob | history

diff --git a/helm/software/helena/src/common/layer.ml b/helm/software/helena/src/common/layer.ml
index 82300931bc5c0652d72a98f38f94fc6c5d258016..c0b6bcc19e47b8209838448f6e0a0a3b3642d602 100644 (file)
--- a/helm/software/helena/src/common/layer.ml
+++ b/helm/software/helena/src/common/layer.ml
@@ -39,7 +39,7 @@ let warn s = L.warn (pred level) s
 let zero = Fin 0
 
 let string_of_value k = function
-   | Inf        -> ""
+   | Inf        -> "-"
    | Fin i      -> string_of_int i
    | Ref (k, i) -> "-" ^ P.string_of_mark k ^ "-" ^ string_of_int i
    | Unk        -> "-" ^ P.string_of_mark k
diff --git a/helm/software/helena/src/toplevel/helena.ml b/helm/software/helena/src/toplevel/helena.ml
index 63a8c062116a2581c2cbf72402e172ab89be66c2..10c9f0f7f148d09c62f00fefc0cc1123f4b1454f 100644 (file)
--- a/helm/software/helena/src/toplevel/helena.ml
+++ b/helm/software/helena/src/toplevel/helena.ml
@@ -386,7 +386,7 @@ END
 
 IFDEF MANAGER THEN
 
-let set_manager s = match KS.lowercase s with
+let set_manager s = match KS.lowercase_ascii s with
    | "v8"  -> G.manager := G.Coq
    | "ma2" -> G.manager := G.Matita
    | "lp1" -> G.manager := G.LP1
diff --git a/helm/www/lambdadelta/images/bronze-03C7.png b/helm/www/lambdadelta/images/bronze-03C7.png
new file mode 100644 (file)
index 0000000..f33b0a8
Binary files /dev/null and b/helm/www/lambdadelta/images/bronze-03C7.png differ
diff --git a/helm/www/lambdadelta/web/home/home.ldw.xml b/helm/www/lambdadelta/web/home/home.ldw.xml
index fffcc806a802007222037e14953546ad5bd93592..11b564b997b11b8f21237895532f333f915a2763 100644 (file)
--- a/helm/www/lambdadelta/web/home/home.ldw.xml
+++ b/helm/www/lambdadelta/web/home/home.ldw.xml
@@ -41,6 +41,7 @@
    </body>
    <body>
       <ucs-bronze char="03BB"/>
+      <ucs-bronze char="03C7"/>
       <ucs-bronze char="03B4"/>
    </body>
 
diff --git a/matita/matita/contribs/lambdadelta/ground/lib/exteq.ma b/matita/matita/contribs/lambdadelta/ground/lib/exteq.ma
index 81d324bad7680885262a6f2c3ea5a6f9a63d9a43..d62edd8ede2d6c83f218507176b313f7f874fe64 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/exteq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/exteq.ma
@@ -36,4 +36,3 @@ lemma exteq_sym (A) (B): symmetric … (exteq A B).
 
 lemma exteq_trans (A) (B): Transitive … (exteq A B).
 /2 width=1 by exteq_repl/ qed-.
-
Unnamed repository; edit this file 'description' to name the repository.