X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2FgTopLevel%2Fesempi%2Fring%2Fcaso3.3.cic;fp=helm%2FgTopLevel%2Fesempi%2Fring%2Fcaso3.3.cic;h=0000000000000000000000000000000000000000;hp=0ac953aa34d26a6bf689de61a67b5858382e9d9d;hb=3ef089a4c58fbe429dd539af6215991ecbe11ee2;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff

diff --git a/helm/gTopLevel/esempi/ring/caso3.3.cic b/helm/gTopLevel/esempi/ring/caso3.3.cic
deleted file mode 100644
index 0ac953aa3..000000000
--- a/helm/gTopLevel/esempi/ring/caso3.3.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
-  (Rmult (Rplus R1 R1) R1)
-  (Rmult R1 R1))