Coercions are now hidden by default (in termAcicContent.ml)

diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml
index fddd777f7e13959fac65a76ff202f40ae23f4738..a25730e4d1fa0aed8e2279694d2d60d3a7d7deb7 100644 (file)
--- a/helm/software/components/acic_content/termAcicContent.ml
+++ b/helm/software/components/acic_content/termAcicContent.ml
@@ -66,6 +66,8 @@ let constructor_of_inductive_type uri i j =
     fst (List.nth (constructors_of_inductive_type uri i) (j-1))
   with Not_found -> assert false)
 
+let hide_coercions = ref true;;
+
 let ast_of_acic0 term_info acic k =
   let k = k term_info in
   let id_to_uris = term_info.uri in
@@ -117,7 +119,23 @@ let ast_of_acic0 term_info acic k =
     | Cic.ALetIn (id,n,s,t) ->
         idref id (Ast.LetIn ((CicNotationUtil.name_of_cic_name n, None),
           k s, k t))
-    | Cic.AAppl (aid,args) -> idref aid (Ast.Appl (List.map k args))
+    | Cic.AAppl (aid,(Cic.AConst _ as he::tl as args))
+    | Cic.AAppl (aid,(Cic.AMutInd _ as he::tl as args))
+    | Cic.AAppl (aid,(Cic.AMutConstruct _ as he::tl as args)) ->
+       if CoercGraph.is_a_coercion (Deannotate.deannotate_term he) &&
+          !hide_coercions
+       then
+        let rec last =
+         function
+            [] -> assert false
+          | [t] -> t
+          | _::tl -> last tl
+        in
+         idref aid (k (last tl))
+       else
+        idref aid (Ast.Appl (List.map k args))
+    | Cic.AAppl (aid,args) ->
+        idref aid (Ast.Appl (List.map k args))
     | Cic.AConst (id,uri,substs) ->
         register_uri id uri;
         idref id (Ast.Ident (UriManager.name_of_uri uri, aux_substs substs))

diff --git a/helm/software/components/acic_content/termAcicContent.mli b/helm/software/components/acic_content/termAcicContent.mli
index 1fd57e0d00cdcec44e1fb2c7059cc42ea2b32bbf..214d7f5d2e9f228dc677c50100ca6a3b8aa0fb78 100644 (file)
--- a/helm/software/components/acic_content/termAcicContent.mli
+++ b/helm/software/components/acic_content/termAcicContent.mli
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+val hide_coercions: bool ref
+
   (** {2 Persistant state handling} *)
 
 type interpretation_id

diff --git a/helm/software/matita/library/algebra/finite_groups.ma b/helm/software/matita/library/algebra/finite_groups.ma
index 2b731d3026a7edb544b084d39c5329554373560e..2078cf1d75cccc151280cc54877f25d1e41156e9 100644 (file)
--- a/helm/software/matita/library/algebra/finite_groups.ma
+++ b/helm/software/matita/library/algebra/finite_groups.ma
@@ -44,30 +44,6 @@ record finite_enumerable_SemiGroup : Type ≝
    is_finite_enumerable:> finite_enumerable semigroup
  }.
 
-notation < "S"
-for @{ 'semigroup_of_finite_enumerable_semigroup $S }.
-
-interpretation "Semigroup_of_finite_enumerable_semigroup"
- 'semigroup_of_finite_enumerable_semigroup S
-=
- (cic:/matita/algebra/finite_groups/semigroup.con S).
-
-notation < "S"
-for @{ 'magma_of_finite_enumerable_semigroup $S }.
-
-interpretation "Magma_of_finite_enumerable_semigroup"
- 'magma_of_finite_enumerable_semigroup S
-=
- (cic:/matita/algebra/finite_groups/Magma_of_finite_enumerable_SemiGroup.con S).
- 
-notation < "S"
-for @{ 'type_of_finite_enumerable_semigroup $S }.
-
-interpretation "Type_of_finite_enumerable_semigroup"
- 'type_of_finite_enumerable_semigroup S
-=
- (cic:/matita/algebra/finite_groups/Type_of_finite_enumerable_SemiGroup.con S).
-
 interpretation "Finite_enumerable representation" 'repr S i =
  (cic:/matita/algebra/finite_groups/repr.con S
   (cic:/matita/algebra/finite_groups/is_finite_enumerable.con S) i).

diff --git a/helm/software/matita/library/algebra/groups.ma b/helm/software/matita/library/algebra/groups.ma
index 57c43d4ae07472c64349296035a59a3e28eb1efd..5d3be8cb14180a09d7154871a7be831a5d7863a4 100644 (file)
--- a/helm/software/matita/library/algebra/groups.ma
+++ b/helm/software/matita/library/algebra/groups.ma
@@ -35,24 +35,6 @@ record Group : Type ≝
    group_properties:> isGroup pregroup
  }.
 
-(*notation < "G"
-for @{ 'monoid $G }.
-
-interpretation "Monoid coercion" 'monoid G =
- (cic:/matita/algebra/groups/monoid.con G).*)
-
-notation < "G"
-for @{ 'type_of_group $G }.
-
-interpretation "Type_of_group coercion" 'type_of_group G =
- (cic:/matita/algebra/groups/Type_of_Group.con G).
-
-notation < "G"
-for @{ 'magma_of_group $G }.
-
-interpretation "magma_of_group coercion" 'magma_of_group G =
- (cic:/matita/algebra/groups/Magma_of_Group.con G).
-
 notation "hvbox(x \sup (-1))" with precedence 89
 for @{ 'ginv $x }.
 
@@ -203,12 +185,6 @@ record subgroup (G:Group) : Type ≝
    embed:> monomorphism group G
  }.
 
-notation < "G"
-for @{ 'type_of_subgroup $G }.
-
-interpretation "Type_of_subgroup coercion" 'type_of_subgroup G =
- (cic:/matita/algebra/groups/Type_of_subgroup.con _ G).
- 
 notation "hvbox(x \sub H)" with precedence 79
 for @{ 'subgroupimage $H $x }.
 

diff --git a/helm/software/matita/library/algebra/monoids.ma b/helm/software/matita/library/algebra/monoids.ma
index 63b6430ec90facf077bfbd3b4b346a9e124d7cc9..a80ee5fb06e40723f2f9e6051c255b9a3fa2a36d 100644 (file)
--- a/helm/software/matita/library/algebra/monoids.ma
+++ b/helm/software/matita/library/algebra/monoids.ma
@@ -21,10 +21,6 @@ record PreMonoid : Type ≝
    e: magma
  }.
 
-notation < "M" for @{ 'pmmagma $M }.
-interpretation "premonoid magma coercion" 'pmmagma M =
- (cic:/matita/algebra/monoids/magma.con M).
-
 record isMonoid (M:PreMonoid) : Prop ≝
  { is_semi_group:> isSemiGroup M;
    e_is_left_unit:
@@ -38,18 +34,6 @@ record Monoid : Type ≝
    monoid_properties:> isMonoid premonoid 
  }.
 
-notation < "M" for @{ 'semigroup $M }.
-interpretation "premonoid coercion" 'premonoid M =
- (cic:/matita/algebra/monoids/premonoid.con M).
- 
-notation < "M" for @{ 'typeofmonoid $M }.
-interpretation "premonoid coercion" 'typeofmonoid M =
- (cic:/matita/algebra/monoids/Type_of_Monoid.con M).
- 
-notation < "M" for @{ 'magmaofmonoid $M }.
-interpretation "premonoid coercion" 'magmaofmonoid M =
- (cic:/matita/algebra/monoids/Magma_of_Monoid.con M).
- 
 notation "1" with precedence 89
 for @{ 'munit }.
 

diff --git a/helm/software/matita/library/algebra/semigroups.ma b/helm/software/matita/library/algebra/semigroups.ma
index 73099286ba7350a1148d6f46afa692c84c9e871c..12ff9531155cc31d19e9aecb8b2a44bb8ba4885f 100644 (file)
--- a/helm/software/matita/library/algebra/semigroups.ma
+++ b/helm/software/matita/library/algebra/semigroups.ma
@@ -23,10 +23,6 @@ record Magma : Type ≝
    op: carrier → carrier → carrier
  }.
 
-notation < "M" for @{ 'carrier $M }.
-interpretation "carrier coercion" 'carrier S =
- (cic:/matita/algebra/semigroups/carrier.con S).
-
 notation "hvbox(a break \middot b)" 
   left associative with precedence 55
 for @{ 'magma_op $a $b }.
@@ -44,10 +40,6 @@ record SemiGroup : Type ≝
    semigroup_properties:> isSemiGroup magma
  }.
  
-notation < "S" for @{ 'magma $S }.
-interpretation "magma coercion" 'magma S =
- (cic:/matita/algebra/semigroups/magma.con S).
- 
 definition is_left_unit ≝
  λS:SemiGroup. λe:S. ∀x:S. e·x = x.
  

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index 2cbb9a9a1350cd2303712637c3705d42c22e21e3..a8a031273b309a05f7316449d4ed57e46c8d1f24 100644 (file)
--- a/helm/software/matita/matita.ml
+++ b/helm/software/matita/matita.ml
@@ -191,6 +191,10 @@ let _ =
       (fun _ ->
         CicNotation.set_active_notations
           (List.map fst (CicNotation.get_all_notations ())));
+    addDebugItem "enable coercions hiding"
+      (fun _ -> TermAcicContent.hide_coercions := true);
+    addDebugItem "disable coercions hiding"
+      (fun _ -> TermAcicContent.hide_coercions := false);
   end
   (** Debugging }}} *)