transcript: we improved the parser/lexer to read the scripts of the standard

[helm.git] / helm / software / matita / contribs / procedural / Coq / Relations / Relation_Operators.mma

diff --git a/helm/software/matita/contribs/procedural/Coq/Relations/Relation_Operators.mma b/helm/software/matita/contribs/procedural/Coq/Relations/Relation_Operators.mma
new file mode 100644 (file)
index 0000000..6dde6e0
--- /dev/null
+++ b/helm/software/matita/contribs/procedural/Coq/Relations/Relation_Operators.mma
@@ -0,0 +1,286 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "Coq.ma".
+
+(*#**********************************************************************)
+
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+
+(*   \VV/  *************************************************************)
+
+(*    //   *      This file is distributed under the terms of the      *)
+
+(*         *       GNU Lesser General Public License Version 2.1       *)
+
+(*#**********************************************************************)
+
+(*i $Id: Relation_Operators.v,v 1.8 2003/11/29 17:28:41 herbelin Exp $ i*)
+
+(*#***************************************************************************)
+
+(*                      Bruno Barras, Cristina Cornes                       *)
+
+(*                                                                          *)
+
+(*  Some of these definitons were taken from :                              *)
+
+(*     Constructing Recursion Operators in Type Theory                      *)
+
+(*     L. Paulson  JSC (1986) 2, 325-355                                    *)
+
+(*#***************************************************************************)
+
+include "Relations/Relation_Definitions.ma".
+
+include "Lists/List.ma".
+
+(*#* Some operators to build relations *)
+
+(* UNEXPORTED
+Section Transitive_Closure
+*)
+
+(* UNEXPORTED
+cic:/Coq/Relations/Relation_Operators/Transitive_Closure/A.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Relations/Relation_Operators/Transitive_Closure/R.var
+*)
+
+inline procedural "cic:/Coq/Relations/Relation_Operators/clos_trans.ind".
+
+(* UNEXPORTED
+End Transitive_Closure
+*)
+
+(* UNEXPORTED
+Section Reflexive_Transitive_Closure
+*)
+
+(* UNEXPORTED
+cic:/Coq/Relations/Relation_Operators/Reflexive_Transitive_Closure/A.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Relations/Relation_Operators/Reflexive_Transitive_Closure/R.var
+*)
+
+inline procedural "cic:/Coq/Relations/Relation_Operators/clos_refl_trans.ind".
+
+(* UNEXPORTED
+End Reflexive_Transitive_Closure
+*)
+
+(* UNEXPORTED
+Section Reflexive_Symetric_Transitive_Closure
+*)
+
+(* UNEXPORTED
+cic:/Coq/Relations/Relation_Operators/Reflexive_Symetric_Transitive_Closure/A.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Relations/Relation_Operators/Reflexive_Symetric_Transitive_Closure/R.var
+*)
+
+inline procedural "cic:/Coq/Relations/Relation_Operators/clos_refl_sym_trans.ind".
+
+(* UNEXPORTED
+End Reflexive_Symetric_Transitive_Closure
+*)
+
+(* UNEXPORTED
+Section Transposee
+*)
+
+(* UNEXPORTED
+cic:/Coq/Relations/Relation_Operators/Transposee/A.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Relations/Relation_Operators/Transposee/R.var
+*)
+
+inline procedural "cic:/Coq/Relations/Relation_Operators/transp.con" as definition.
+
+(* UNEXPORTED
+End Transposee
+*)
+
+(* UNEXPORTED
+Section Union
+*)
+
+(* UNEXPORTED
+cic:/Coq/Relations/Relation_Operators/Union/A.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Relations/Relation_Operators/Union/R1.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Relations/Relation_Operators/Union/R2.var
+*)
+
+inline procedural "cic:/Coq/Relations/Relation_Operators/union.con" as definition.
+
+(* UNEXPORTED
+End Union
+*)
+
+(* UNEXPORTED
+Section Disjoint_Union
+*)
+
+(* UNEXPORTED
+cic:/Coq/Relations/Relation_Operators/Disjoint_Union/A.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Relations/Relation_Operators/Disjoint_Union/B.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Relations/Relation_Operators/Disjoint_Union/leA.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Relations/Relation_Operators/Disjoint_Union/leB.var
+*)
+
+inline procedural "cic:/Coq/Relations/Relation_Operators/le_AsB.ind".
+
+(* UNEXPORTED
+End Disjoint_Union
+*)
+
+(* UNEXPORTED
+Section Lexicographic_Product
+*)
+
+(* Lexicographic order on dependent pairs *)
+
+(* UNEXPORTED
+cic:/Coq/Relations/Relation_Operators/Lexicographic_Product/A.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Relations/Relation_Operators/Lexicographic_Product/B.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Relations/Relation_Operators/Lexicographic_Product/leA.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Relations/Relation_Operators/Lexicographic_Product/leB.var
+*)
+
+inline procedural "cic:/Coq/Relations/Relation_Operators/lexprod.ind".
+
+(* UNEXPORTED
+End Lexicographic_Product
+*)
+
+(* UNEXPORTED
+Section Symmetric_Product
+*)
+
+(* UNEXPORTED
+cic:/Coq/Relations/Relation_Operators/Symmetric_Product/A.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Relations/Relation_Operators/Symmetric_Product/B.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Relations/Relation_Operators/Symmetric_Product/leA.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Relations/Relation_Operators/Symmetric_Product/leB.var
+*)
+
+inline procedural "cic:/Coq/Relations/Relation_Operators/symprod.ind".
+
+(* UNEXPORTED
+End Symmetric_Product
+*)
+
+(* UNEXPORTED
+Section Swap
+*)
+
+(* UNEXPORTED
+cic:/Coq/Relations/Relation_Operators/Swap/A.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Relations/Relation_Operators/Swap/R.var
+*)
+
+inline procedural "cic:/Coq/Relations/Relation_Operators/swapprod.ind".
+
+(* UNEXPORTED
+End Swap
+*)
+
+(* UNEXPORTED
+Section Lexicographic_Exponentiation
+*)
+
+(* UNEXPORTED
+cic:/Coq/Relations/Relation_Operators/Lexicographic_Exponentiation/A.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Relations/Relation_Operators/Lexicographic_Exponentiation/leA.var
+*)
+
+inline procedural "cic:/Coq/Relations/Relation_Operators/Lexicographic_Exponentiation/Nil.con" "Lexicographic_Exponentiation__" as definition.
+
+inline procedural "cic:/Coq/Relations/Relation_Operators/Lexicographic_Exponentiation/List.con" "Lexicographic_Exponentiation__" as definition.
+
+inline procedural "cic:/Coq/Relations/Relation_Operators/Ltl.ind".
+
+inline procedural "cic:/Coq/Relations/Relation_Operators/Desc.ind".
+
+inline procedural "cic:/Coq/Relations/Relation_Operators/Pow.con" as definition.
+
+inline procedural "cic:/Coq/Relations/Relation_Operators/lex_exp.con" as definition.
+
+(* UNEXPORTED
+End Lexicographic_Exponentiation
+*)
+
+(* UNEXPORTED
+Hint Unfold transp union: sets v62.
+*)
+
+(* UNEXPORTED
+Hint Resolve t_step rt_step rt_refl rst_step rst_refl: sets v62.
+*)
+
+(* UNEXPORTED
+Hint Immediate rst_sym: sets v62.
+*)
+