From a14157957532b731330492388ab32909b4147758 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 11 Jun 2009 22:02:51 +0000 Subject: [PATCH] - applyTransformation: bugfix in the rendering of records now algebra/monoids.ma is fully reconstructed :) --- helm/software/matita/applyTransformation.ml | 5 +++-- helm/software/matita/library/algebra/monoids.ma | 5 +++-- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index f5f279e73..5ee48f3da 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -235,7 +235,8 @@ let txt_of_cic_object ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp in let aux = function - | G.Executable (_, G.Command (_, G.Obj (_, N.Inductive _))) as stm + | G.Executable (_, G.Command (_, G.Obj (_, N.Inductive _))) + | G.Executable (_, G.Command (_, G.Obj (_, N.Record _))) as stm -> let hc = !Acic2content.hide_coercions in if List.mem G.IPCoercions params then @@ -245,7 +246,7 @@ let txt_of_cic_object enable_notations true; Acic2content.hide_coercions := hc; str -(* FG: we disable notation for Inductive to avoid recursive notation *) +(* FG: we disable notation for inductive types to avoid recursive notation *) | G.Executable (_, G.Tactic _) as stm -> let hc = !Acic2content.hide_coercions in Acic2content.hide_coercions := false; diff --git a/helm/software/matita/library/algebra/monoids.ma b/helm/software/matita/library/algebra/monoids.ma index 9fc13f91e..36de5a369 100644 --- a/helm/software/matita/library/algebra/monoids.ma +++ b/helm/software/matita/library/algebra/monoids.ma @@ -19,6 +19,9 @@ record PreMonoid : Type ≝ e: magma }. +(* FG: the interpretation goes just after its definition *) +interpretation "Monoid unit" 'neutral = (e ?). + record isMonoid (M:PreMonoid) : Prop ≝ { is_semi_group:> isSemiGroup M; e_is_left_unit: @@ -31,8 +34,6 @@ record Monoid : Type ≝ { premonoid:> PreMonoid; monoid_properties:> isMonoid premonoid }. - -interpretation "Monoid unit" 'neutral = (e ?). definition is_left_inverse ≝ λM:Monoid. -- 2.39.2