X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2FgTopLevel%2Fesempi%2Fring%2Fcaso3.1bis.cic;fp=helm%2FgTopLevel%2Fesempi%2Fring%2Fcaso3.1bis.cic;h=0000000000000000000000000000000000000000;hp=ec85c071aa0decb9a837009516edaca6565fae0c;hb=1696761e4b8576e8ed81caa905fd108717019226;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1

diff --git a/helm/gTopLevel/esempi/ring/caso3.1bis.cic b/helm/gTopLevel/esempi/ring/caso3.1bis.cic
deleted file mode 100644
index ec85c071a..000000000
--- a/helm/gTopLevel/esempi/ring/caso3.1bis.cic
+++ /dev/null
@@ -1,25 +0,0 @@
-(* ok *)
-alias eq            /Coq/Init/Logic/Equality/eq.ind#1/1
-alias eqT           /Coq/Init/Logic_Type/eqT.ind#1/1
-alias R             /Coq/Reals/Rdefinitions/R.con
-alias Rplus         /Coq/Reals/Rdefinitions/Rplus.con
-alias Rmult         /Coq/Reals/Rdefinitions/Rmult.con
-alias R1            /Coq/Reals/Rdefinitions/R1.con
-alias R0            /Coq/Reals/Rdefinitions/R0.con
-alias Ropp          /Coq/Reals/Rdefinitions/Ropp.con
-alias interp_sacs   /Coq/ring/Ring_abstract/abstract_rings/interp_sacs.con
-alias apolynomial_normalize   /Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize.con
-alias Node_vm       /Coq/ring/Quote/variables_map/varmap.ind#1/1/2
-alias Empty_vm      /Coq/ring/Quote/variables_map/varmap.ind#1/1/1
-alias APvar         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/1
-alias AP0         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/2
-alias AP1         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/3
-alias APplus        /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/4
-alias APmult         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/5
-alias APopp         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/6
-alias Left_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/1
-alias Right_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/2
-alias End_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/3
-(eqT R
-  (Rplus R1 R1)
-  (Rmult R1 R1))