Branch V7_3_new_exportation merged.

[helm.git] / helm / meta_style / basic.xml

diff --git a/helm/meta_style/basic.xml b/helm/meta_style/basic.xml
index b0681468c95ba105ecc27d928648ef49434cb26e..e9da62a6281ceec8b6b24b8720f893dd09d93f78 100644 (file)
--- a/helm/meta_style/basic.xml
+++ b/helm/meta_style/basic.xml
@@ -7,16 +7,27 @@
 
 <Operator
  name  = "AND"
- uri   = "cic:/Coq/Init/Logic/Conjunction/and.ind"
+ uri   = "cic:/Coq/Init/Logic/and.ind"
  arity = "2"
  m-tag = "and"/>
 
 <Operator
  name  = "OR"
- uri   = "cic:/Coq/Init/Logic/Disjunction/or.ind"
+ uri   = "cic:/Coq/Init/Logic/or.ind"
  arity = "2"
  m-tag = "or"/>
 
+<Operator
+ name  = "IFF"
+ uri   = "cic:/Coq/Init/Logic/iff.con"
+ arity = "2">
+       <mapp>
+               <m:csymbol>iff</m:csymbol>
+               <param id="1"/>
+               <param id="2"/>
+       </mapp>
+</Operator>
+
 <Operator
  name  = "NOT" 
  uri   = "cic:/Coq/Init/Logic/not.con"
@@ -28,14 +39,14 @@
 
 <Operator
  name  = "EQUALITY and TYPE EQUALITY"
- uri   = "cic:/Coq/Init/Logic/Equality/eq.ind | cic:/Coq/Init/Logic_Type/eqT.ind"
+ uri   = "cic:/Coq/Init/Logic/eq.ind | cic:/Coq/Init/Logic_Type/eqT.ind"
  hide  = "1"
  arity = "2"
  m-tag = "eq"/>
 
 <NotOperator
  name  = "NOT-EQ and NOT-EQT"
- uri   = "cic:/Coq/Init/Logic/Equality/eq.ind | cic:/Coq/Init/Logic_Type/eqT.ind"
+ uri   = "cic:/Coq/Init/Logic/eq.ind | cic:/Coq/Init/Logic_Type/eqT.ind"
  hide  = "1"
  arity = "2">
        <mapp>
@@ -47,7 +58,7 @@
 
 <Operator
  name  = "EXIST"
- uri   = "cic:/Coq/Init/Logic/First_order_quantifiers/ex.ind | cic:/Coq/Init/Logic_Type/exT.ind"
+ uri   = "cic:/Coq/Init/Logic/ex.ind | cic:/Coq/Init/Logic_Type/exT.ind"
  arity = "2">
        <mapp>
                <mop tag="exists"/>
@@ -61,7 +72,7 @@
 
 <Operator
  name  = "EXIST"
- uri   = "cic:/Coq/Init/Logic/First_order_quantifiers/ex2.ind | cic:/Coq/Init/Logic_Type/exT2.ind"
+ uri   = "cic:/Coq/Init/Logic/ex2.ind | cic:/Coq/Init/Logic_Type/exT2.ind"
  hide  = "1"
  arity = "2">
        <mapp>