helm/gTopLevel/esempi/ring/aliases.cic

   1 alias false /Coq/Init/Datatypes/bool.ind#1/1/2
   2 alias apolynomial_normalize_ok /Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize_ok.con
   3 alias RTheory /Coq/Reals/Rbase/RTheory.con
   4 alias eq            /Coq/Init/Logic/Equality/eq.ind#1/1
   5 alias eqT           /Coq/Init/Logic_Type/eqT.ind#1/1
   6 alias R             /Coq/Reals/Rdefinitions/R.con
   7 alias Rplus         /Coq/Reals/Rdefinitions/Rplus.con
   8 alias Rmult         /Coq/Reals/Rdefinitions/Rmult.con
   9 alias R1            /Coq/Reals/Rdefinitions/R1.con
  10 alias R0            /Coq/Reals/Rdefinitions/R0.con
  11 alias Ropp          /Coq/Reals/Rdefinitions/Ropp.con
  12 alias interp_sacs   /Coq/ring/Ring_abstract/abstract_rings/interp_sacs.con
  13 alias apolynomial_normalize   /Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize.con
  14 alias Node_vm       /Coq/ring/Quote/variables_map/varmap.ind#1/1/2
  15 alias Empty_vm      /Coq/ring/Quote/variables_map/varmap.ind#1/1/1
  16 alias APvar         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/1
  17 alias AP0         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/2
  18 alias AP1         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/3
  19 alias APplus        /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/4
  20 alias APmult         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/5
  21 alias APopp         /Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind#1/1/6
  22 alias Left_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/1
  23 alias Right_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/2
  24 alias End_idx     /Coq/ring/Quote/variables_map/index.ind#1/1/3