(**************************************************************************)
(*       ___                                                              *)
(*      ||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___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)

(*   \VV/  **************************************************************)

(*    //   *      This file is distributed under the terms of the       *)

(*         *       GNU Lesser General Public License Version 2.1        *)

(*#***********************************************************************)

(*i $Id: Notations.v,v 1.24.2.2 2004/08/01 09:36:44 herbelin Exp $ i*)

(*#* These are the notations whose level and associativity are imposed by Coq *)

(*#* Notations for propositional connectives *)

(* NOTATION
Reserved Notation "x <-> y" (at level 95, no associativity).
*)

(* NOTATION
Reserved Notation "x /\ y" (at level 80, right associativity).
*)

(* NOTATION
Reserved Notation "x \/ y" (at level 85, right associativity).
*)

(* NOTATION
Reserved Notation "~ x" (at level 75, right associativity).
*)

(*#* Notations for equality and inequalities *)

(* NOTATION
Reserved Notation "x = y  :> T"
(at level 70, y at next level, no associativity).
*)

(* NOTATION
Reserved Notation "x = y" (at level 70, no associativity).
*)

(* NOTATION
Reserved Notation "x = y = z"
(at level 70, no associativity, y at next level).
*)

(* NOTATION
Reserved Notation "x <> y  :> T"
(at level 70, y at next level, no associativity).
*)

(* NOTATION
Reserved Notation "x <> y" (at level 70, no associativity).
*)

(* NOTATION
Reserved Notation "x <= y" (at level 70, no associativity).
*)

(* NOTATION
Reserved Notation "x < y" (at level 70, no associativity).
*)

(* NOTATION
Reserved Notation "x >= y" (at level 70, no associativity).
*)

(* NOTATION
Reserved Notation "x > y" (at level 70, no associativity).
*)

(* NOTATION
Reserved Notation "x <= y <= z" (at level 70, y at next level).
*)

(* NOTATION
Reserved Notation "x <= y < z" (at level 70, y at next level).
*)

(* NOTATION
Reserved Notation "x < y < z" (at level 70, y at next level).
*)

(* NOTATION
Reserved Notation "x < y <= z" (at level 70, y at next level).
*)

(*#* Arithmetical notations (also used for type constructors) *)

(* NOTATION
Reserved Notation "x + y" (at level 50, left associativity).
*)

(* NOTATION
Reserved Notation "x - y" (at level 50, left associativity).
*)

(* NOTATION
Reserved Notation "x * y" (at level 40, left associativity).
*)

(* NOTATION
Reserved Notation "x / y" (at level 40, left associativity).
*)

(* NOTATION
Reserved Notation "- x" (at level 35, right associativity).
*)

(* NOTATION
Reserved Notation "/ x" (at level 35, right associativity).
*)

(* NOTATION
Reserved Notation "x ^ y" (at level 30, right associativity).
*)

(*#* Notations for pairs *)

(* NOTATION
Reserved Notation "( x , y , .. , z )" (at level 0).
*)

(*#* Notation "{ x }" is reserved and has a special status as component
    of other notations; it is at level 0 to factor with {x:A|P} etc *)

(* NOTATION
Reserved Notation "{ x }" (at level 0, x at level 99).
*)

(*#* Notations for sum-types *)

(* NOTATION
Reserved Notation "{ A } + { B }" (at level 50, left associativity).
*)

(* NOTATION
Reserved Notation "A + { B }" (at level 50, left associativity).
*)

(*#* Notations for sigma-types or subsets *)

(* NOTATION
Reserved Notation "{ x : A  |  P }" (at level 0, x at level 99).
*)

(* NOTATION
Reserved Notation "{ x : A  |  P  &  Q }" (at level 0, x at level 99).
*)

(* NOTATION
Reserved Notation "{ x : A  &  P }" (at level 0, x at level 99).
*)

(* NOTATION
Reserved Notation "{ x : A  &  P  &  Q }" (at level 0, x at level 99).
*)

(* UNEXPORTED
Delimit Scope type_scope with type.
*)

(* UNEXPORTED
Delimit Scope core_scope with core.
*)

(* UNEXPORTED
Open Scope core_scope.
*)

(* UNEXPORTED
Open Scope type_scope.
*)