v8Lexer.cmx: v8Parser.cmx options.cmx
grafite.cmo: types.cmx options.cmx grafite.cmi
grafite.cmx: types.cmx options.cmx grafite.cmi
-engine.cmo: v8Parser.cmi v8Lexer.cmx types.cmx grafite.cmi engine.cmi
-engine.cmx: v8Parser.cmx v8Lexer.cmx types.cmx grafite.cmx engine.cmi
+engine.cmo: v8Parser.cmi v8Lexer.cmx types.cmx options.cmx grafite.cmi \
+ engine.cmi
+engine.cmx: v8Parser.cmx v8Lexer.cmx types.cmx options.cmx grafite.cmx \
+ engine.cmi
top.cmo: options.cmx engine.cmi
top.cmx: options.cmx engine.cmx
* http://cs.unibo.it/helm/.
*)
-module R = Helm_registry
-module X = HExtlib
-module T = Types
-module G = Grafite
+module R = Helm_registry
+module X = HExtlib
+module T = Types
+module G = Grafite
+module HP = Http_getter
+
+module O = Options
type script = {
name : string;
let init () =
let transcript_dir = Filename.dirname Sys.argv.(0) in
let default_registry = Filename.concat transcript_dir "transcript" in
- load_registry default_registry
+ let matita_registry = Filename.concat !O.cwd "matita" in
+ load_registry default_registry;
+ load_registry matita_registry;
+ HP.init ()
-let make cwd registry =
+let make registry =
let id x = x in
let get_coercions = R.get_list (R.pair id id) in
let get_output_type key =
scripts = Array.make default_scripts default_script
} in
let st = {st with
- heading_path = Filename.concat cwd st.heading_path;
- output_path = Filename.concat cwd st.output_path;
+ heading_path = Filename.concat !O.cwd st.heading_path;
+ output_path = Filename.concat !O.cwd st.output_path;
} in
prerr_endline "reading file names ...";
let st = set_files st in
val init: unit -> unit
-val make: string -> string -> status
+val make: string -> status
val produce: status -> unit
module UM = UriManager
module NP = CicNotationPp
module GP = GrafiteAstPp
-module G = GrafiteAst
-module H = HExtlib
+module G = GrafiteAst
+module H = HExtlib
+module HG = Http_getter
let floc = H.dummy_floc
let out_line_comment och s =
let l = 70 - String.length s in
+ let l = if l < 0 then 0 else l in
let s = Printf.sprintf " %s %s" s (String.make l '*') in
out_comment och s
let coercion value =
command_of_obj (G.Coercion (floc, UM.uri_of_string value, true, 0, 0))
-let inline (kind, uri, prefix, flavour) =
+let inline kind uri prefix flavour =
let kind = match kind with
| T.Declarative -> G.Declarative
| T.Procedural -> G.Procedural None
let out_alias och name uri =
Printf.fprintf och "alias id \"%s\" = \"%s\".\n\n" name uri
+let check och src =
+ if HG.exists ~local:false src then () else
+ let msg = "UNAVAILABLE OBJECT: " ^ src in
+ out_line_comment och msg;
+ prerr_endline msg
+
let commit kind och items =
let trd (_, _, x) = x in
- let trd_rth kind (_, _, x, y, z) = kind, x, y, z in
let commit = function
| T.Heading heading -> out_preamble och heading
| T.Line line ->
if !O.comments then out_unexported och "NOTATION" (snd specs) (**)
| T.Inline (_, T.Var, src, _, _) ->
if !O.comments then out_unexported och "UNEXPORTED" src
-(* FG: we do not export variables because we cook the other object
+(* FG: we do not export variables because we cook the other objects
* let name = UriManager.name_of_uri (UriManager.uri_of_string src) in
* out_alias och name src
*)
- | T.Inline specs -> out_command och (inline (trd_rth kind specs))
+ | T.Inline (_, _, src, pre, fl) ->
+ if !O.getter then check och src;
+ out_command och (inline kind src pre fl)
| T.Section specs ->
if !O.comments then out_unexported och "UNEXPORTED" (trd specs)
| T.Comment comment ->
* http://cs.unibo.it/helm/.
*)
+let cwd = ref Filename.current_dir_name
+
let verbose_parser = ref false
let verbose_lexer = ref false
let verbose_escape = ref false
let comments = ref true
+
+let getter = ref false
*)
let main =
- let cwd = ref Filename.current_dir_name in
- let help = "Usage: transcript [ -C <dir> ] [ <package> | <conf_file> ]*" in
+ let help = "Usage: transcript [ -glmpx | -C <dir> ] [ <package> | <conf_file> ]*" in
let help_C = " set working directory to <dir>" in
- let help_vp = " verbose parsing" in
- let help_vl = " verbose lexing" in
- let help_vx = " verbose character escaping" in
- let set_cwd dir = cwd := dir in
- let process_package package = Engine.produce (Engine.make !cwd package) in
- Engine.init ();
+ let help_g = " check for non existing objects" in
+ let help_l = " verbose lexing" in
+ let help_m = " minimal output generation" in
+ let help_p = " verbose parsing" in
+ let help_x = " verbose character escaping" in
+ let set_cwd dir = Options.cwd := dir; Engine.init () in
+ let process_package package = Engine.produce (Engine.make package) in
Arg.parse [
("-C", Arg.String set_cwd, help_C);
- ("-vp", Arg.Set Options.verbose_parser, help_vp);
- ("-vl", Arg.Set Options.verbose_lexer, help_vl);
- ("-vx", Arg.Set Options.verbose_escape, help_vx);
+ ("-g", Arg.Set Options.getter, help_g);
+ ("-l", Arg.Set Options.verbose_lexer, help_l);
+ ("-m", Arg.Clear Options.comments, help_m);
+ ("-p", Arg.Set Options.verbose_parser, help_p);
+ ("-x", Arg.Set Options.verbose_escape, help_x);
] process_package help
| "Theorem" -> Some `Theorem
| "Definition" -> Some `Definition
| "Fixpoint" -> Some `Definition
+ | "CoFixpoint" -> Some `Definition
| "Let" -> Some `Definition
| "Scheme" -> Some `Theorem
| _ -> assert false
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Arith.v,v 1.11 2003/11/29 17:28:28 herbelin Exp $ i*)
+(*i $Id: Arith.v,v 1.11.2.2 2004/08/03 17:42:42 herbelin Exp $ i*)
include "Arith/Le.ma".
include "Arith/Between.ma".
-include "Arith/Minus.ma".
-
include "Arith/Peano_dec.ma".
include "Arith/Compare_dec.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Between.v,v 1.12 2003/12/15 19:48:17 barras Exp $ i*)
+(*i $Id: Between.v,v 1.12.2.1 2004/07/16 19:30:59 herbelin Exp $ i*)
include "Arith/Le.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* $Id: Bool_nat.v,v 1.5 2003/11/29 17:28:28 herbelin Exp $ *)
+(* $Id: Bool_nat.v,v 1.5.2.1 2004/07/16 19:30:59 herbelin Exp $ *)
include "Arith/Compare_dec.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Compare.v,v 1.12 2004/03/03 15:53:40 marche Exp $ i*)
+(*i $Id: Compare.v,v 1.12.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
(*#* Equality is decidable on [nat] *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Compare_dec.v,v 1.13 2003/11/29 17:28:28 herbelin Exp $ i*)
+(*i $Id: Compare_dec.v,v 1.13.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
include "Arith/Le.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Div.v,v 1.8 2003/04/09 10:55:03 herbelin Exp $ i*)
+(*i $Id: Div.v,v 1.8.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
(*#* Euclidean division *)
Implicit Variables Type n,a,b,q,r:nat.
*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Arith/Div/inf_dec.con *********************)
+
inline procedural "cic:/Coq/Arith/Div/inf_dec.con" as definition.
+(* UNAVAILABLE OBJECT: cic:/Coq/Arith/Div/div1.con ************************)
+
inline procedural "cic:/Coq/Arith/Div/div1.con" as theorem.
+(* UNAVAILABLE OBJECT: cic:/Coq/Arith/Div/div2.con ************************)
+
inline procedural "cic:/Coq/Arith/Div/div2.con" as theorem.
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Div2.v,v 1.15 2003/11/29 17:28:28 herbelin Exp $ i*)
+(*i $Id: Div2.v,v 1.15.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
include "Arith/Lt.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: EqNat.v,v 1.14 2003/11/29 17:28:28 herbelin Exp $ i*)
+(*i $Id: EqNat.v,v 1.14.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
(*#* Equality on natural numbers *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Euclid.v,v 1.7 2003/12/15 19:48:17 barras Exp $ i*)
+(*i $Id: Euclid.v,v 1.7.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
include "Arith/Mult.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Even.v,v 1.14 2003/11/29 17:28:28 herbelin Exp $ i*)
+(*i $Id: Even.v,v 1.14.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
(*#* Here we define the predicates [even] and [odd] by mutual induction
and we prove the decidability and the exclusion of those predicates.
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Factorial.v,v 1.5 2003/11/29 17:28:28 herbelin Exp $ i*)
+(*i $Id: Factorial.v,v 1.5.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
include "Arith/Plus.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Gt.v,v 1.8 2003/11/29 17:28:28 herbelin Exp $ i*)
+(*i $Id: Gt.v,v 1.8.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
include "Arith/Le.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Le.v,v 1.14 2003/11/29 17:28:28 herbelin Exp $ i*)
+(*i $Id: Le.v,v 1.14.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
(*#* Order on natural numbers *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Lt.v,v 1.11 2003/11/29 17:28:28 herbelin Exp $ i*)
+(*i $Id: Lt.v,v 1.11.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
include "Arith/Le.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Max.v,v 1.7 2003/11/29 17:28:28 herbelin Exp $ i*)
+(*i $Id: Max.v,v 1.7.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
include "Arith/Arith.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Min.v,v 1.10 2003/11/29 17:28:29 herbelin Exp $ i*)
+(*i $Id: Min.v,v 1.10.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
include "Arith/Arith.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Minus.v,v 1.14 2003/11/29 17:28:29 herbelin Exp $ i*)
+(*i $Id: Minus.v,v 1.14.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
(*#* Subtraction (difference between two natural numbers) *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Mult.v,v 1.21 2003/11/29 17:28:29 herbelin Exp $ i*)
+(*i $Id: Mult.v,v 1.21.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
include "Arith/Plus.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Peano_dec.v,v 1.10 2003/11/29 17:28:29 herbelin Exp $ i*)
+(*i $Id: Peano_dec.v,v 1.10.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
include "Logic/Decidable.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Plus.v,v 1.18 2003/11/29 17:28:29 herbelin Exp $ i*)
+(*i $Id: Plus.v,v 1.18.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
(*#* Properties of addition *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Wf_nat.v,v 1.16 2003/12/15 19:48:17 barras Exp $ i*)
+(*i $Id: Wf_nat.v,v 1.16.2.1 2004/07/16 19:31:01 herbelin Exp $ i*)
(*#* Well-founded relations and natural numbers *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Bool.v,v 1.29 2004/02/12 16:03:01 herbelin Exp $ i*)
+(*i $Id: Bool.v,v 1.29.2.1 2004/07/16 19:31:01 herbelin Exp $ i*)
(*#* Booleans *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: BoolEq.v,v 1.4 2003/12/15 19:48:17 barras Exp $ i*)
+(*i $Id: BoolEq.v,v 1.4.2.1 2004/07/16 19:31:02 herbelin Exp $ i*)
(* Cuihtlauac Alvarado - octobre 2000 *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Bvector.v,v 1.6 2004/02/10 15:38:01 marche Exp $ i*)
+(*i $Id: Bvector.v,v 1.6.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
(*#* Bit vectors. Contribution by Jean Duprat (ENS Lyon). *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: DecBool.v,v 1.6 2004/03/28 14:41:45 herbelin Exp $ i*)
+(*i $Id: DecBool.v,v 1.6.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
(* UNEXPORTED
Set Implicit Arguments.
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: IfProp.v,v 1.7 2003/11/29 17:28:29 herbelin Exp $ i*)
+(*i $Id: IfProp.v,v 1.7.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
include "Bool/Bool.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Sumbool.v,v 1.12 2003/11/29 17:28:30 herbelin Exp $ i*)
+(*i $Id: Sumbool.v,v 1.12.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
(*#* Here are collected some results about the type sumbool (see INIT/Specif.v)
[sumbool A B], which is written [{A}+{B}], is the informative
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Zerob.v,v 1.8 2003/11/29 17:28:30 herbelin Exp $ i*)
+(*i $Id: Zerob.v,v 1.8.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
include "Arith/Arith.ma".
<key name="output_name">Coq</key>
<key name="input_base_uri">cic:/Coq</key>
<key name="output_base_uri">cic:/matita/procedural/Coq</key>
- <key name="input_path">/projects/helm/exportation/V8.0_mowgli_bugfix_branch/theories</key>
+ <key name="input_path">/home/fguidi/coq_ufficial_theories/8.0pl2</key>
<key name="output_path">contribs/procedural/Coq</key>
<key name="input_type">.v</key>
<key name="output_type">procedural</key>
Infix "++" := app (right associativity, at level 60) : list_scope.
*)
-(* From Num/Leibniz/EqAxioms **********************************************)
-
-(* NOTATION
-Grammar constr constr1 :=
-eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ].
-*)
-
-(* NOTATION
-Syntax constr
- level 1:
- equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "=" $t2:E ] ].
-*)
-
-(* From Num/Leibniz/NSyntax ***********************************************)
-
-(* NOTATION
-Infix 6 "<" lt.
-*)
-
-(* NOTATION
-Infix 6 "<=" le.
-*)
-
-(* NOTATION
-Infix 6 ">" gt.
-*)
-
-(* NOTATION
-Infix 6 ">=" ge.
-*)
-
-(* NOTATION
-Grammar constr lassoc_constr4 :=
- squash_sum
- [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
- case [$c2] of
- (SQUASH $T2) ->
- case [$c1] of
- (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
- | $_ -> [ (sumor $c1 $T2) ] (* c1+{T2} *)
- esac
- | $_ -> [ (add $c1 $c2) ] (* c1+c2 *)
- esac.
-*)
-
-(* NOTATION
-Syntax constr
- level 1:
- equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "=" $t2:E ] ]
- ;
-
- level 4:
- sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
-.
-*)
-
-(* From Num/Nat/NSyntax ***************************************************)
-
-(* NOTATION
-Infix 6 "<" lt.
-*)
-
-(* NOTATION
-Infix 6 "<=" le.
-*)
-
-(* NOTATION
-Infix 6 ">" gt.
-*)
-
-(* NOTATION
-Infix 6 ">=" ge.
-*)
-
-(* NOTATION
-Grammar constr lassoc_constr4 :=
- squash_sum
- [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
- case [$c2] of
- (SQUASH $T2) ->
- case [$c1] of
- (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
- | $_ -> [ (sumor $c1 $T2) ] (* c1+{T2} *)
- esac
- | $_ -> [ (add $c1 $c2) ] (* c1+c2 *)
- esac.
-*)
-
-(* NOTATION
-Syntax constr
- level 4:
- sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
-.
-*)
-
-(* From Num/EqParams ******************************************************)
+(* From NArith/BinNat *****************************************************)
(* NOTATION
-Grammar constr constr1 :=
-eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ].
+Infix "+" := Nplus : N_scope.
*)
(* NOTATION
-Syntax constr
- level 1:
- equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "=" $t2:E ] ]
-.
-*)
-
-(* From Num/NSyntax *******************************************************)
-
-(* NOTATION
-Infix 6 "<" lt V8only 70.
+Infix "*" := Nmult : N_scope.
*)
(* NOTATION
-Infix 6 "<=" le V8only 70.
+Infix "?=" := Ncompare (at level 70, no associativity) : N_scope.
*)
-(* NOTATION
-Infix 6 ">" gt V8only 70.
-*)
+(* From NArith/BinPos *****************************************************)
(* NOTATION
-Infix 6 ">=" ge V8only 70.
+Infix "+" := Pplus : positive_scope.
*)
(* NOTATION
-Grammar constr lassoc_constr4 :=
- squash_sum
- [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
- case [$c2] of
- (SQUASH $T2) ->
- case [$c1] of
- (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
- | $_ -> [ (sumor $c1 $T2) ] (* c1+{T2} *)
- esac
- | $_ -> [ (add $c1 $c2) ] (* c1+c2 *)
- esac.
+Infix "-" := Pminus : positive_scope.
*)
(* NOTATION
-Syntax constr
- level 4:
- sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
-.
+Infix "*" := Pmult : positive_scope.
*)
-(* From Num/NeqDef ********************************************************)
-
(* NOTATION
-Infix 6 "<>" neq V8only 70.
+Infix "/" := Pdiv2 : positive_scope.
*)
-(* From Num/NeqParams *****************************************************)
-
(* NOTATION
-Infix 6 "<>" neq V8only 70.
+Infix "?=" := Pcompare (at level 70, no associativity) : positive_scope.
*)
(* From Reals/RIneq *******************************************************)
Notation Le_AsB := (le_AsB A B leA leB).
*)
-(* From Wellfounded/Lexicographic_Product *********************************)
-
-(* NOTATION
-Notation LexProd := (lexprod A B leA leB).
-*)
-
-(* NOTATION
-Notation Symprod := (symprod A B leA leB).
-*)
-
-(* NOTATION
-Notation SwapProd := (swapprod A R).
-*)
-
-(* From Wellfounded/Union *************************************************)
-
-(* NOTATION
-Notation Union := (union A R1 R2).
-*)
-
(* From Wellfounded/Lexicographic_Exponentiation **************************)
(* NOTATION
Notation "<< x , y >>" := (exist Descl x y) (at level 0, x, y at level 100).
*)
-(* From Wellfounded/Transitive_Closure ************************************)
+(* From Wellfounded/Lexicographic_Product *********************************)
(* NOTATION
-Notation trans_clos := (clos_trans A R).
+Notation LexProd := (lexprod A B leA leB).
*)
-(* From ZArith/Zdiv *******************************************************)
-
(* NOTATION
-Infix "/" := Zdiv : Z_scope.
+Notation Symprod := (symprod A B leA leB).
*)
(* NOTATION
-Infix "mod" := Zmod (at level 40, no associativity) : Z_scope.
+Notation SwapProd := (swapprod A R).
*)
-(* From ZArith/Zpower *****************************************************)
+(* From Wellfounded/Transitive_Closure ************************************)
(* NOTATION
-Infix "^" := Zpower : Z_scope.
+Notation trans_clos := (clos_trans A R).
*)
+(* From Wellfounded/Union *************************************************)
+
(* NOTATION
-Infix "^" := Zpower : Z_scope.
+Notation Union := (union A R1 R2).
*)
(* From ZArith/BinInt *****************************************************)
Notation "x < y <= z" := (x < y /\ y <= z) : Z_scope.
*)
-(* From ZArith/Znumtheory *************************************************)
-
-(* NOTATION
-Notation "( a | b )" := (Zdivide a b) (at level 0) : Z_scope.
-*)
-
-(* From NArith/BinNat *****************************************************)
-
-(* NOTATION
-Infix "+" := Nplus : N_scope.
-*)
+(* From ZArith/Zdiv *******************************************************)
(* NOTATION
-Infix "*" := Nmult : N_scope.
+Infix "/" := Zdiv : Z_scope.
*)
(* NOTATION
-Infix "?=" := Ncompare (at level 70, no associativity) : N_scope.
+Infix "mod" := Zmod (at level 40, no associativity) : Z_scope.
*)
-(* From NArith/BinPos *****************************************************)
-
-(* NOTATION
-Infix "+" := Pplus : positive_scope.
-*)
+(* From ZArith/Znumtheory *************************************************)
(* NOTATION
-Infix "-" := Pminus : positive_scope.
+Notation "( a | b )" := (Zdivide a b) (at level 0) : Z_scope.
*)
-(* NOTATION
-Infix "*" := Pmult : positive_scope.
-*)
+(* From ZArith/Zpower *****************************************************)
(* NOTATION
-Infix "/" := Pdiv2 : positive_scope.
+Infix "^" := Zpower : Z_scope.
*)
(* NOTATION
-Infix "?=" := Pcompare (at level 70, no associativity) : positive_scope.
+Infix "^" := Zpower : Z_scope.
*)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Datatypes.v,v 1.26 2004/03/17 10:54:49 herbelin Exp $ i*)
+(*i $Id: Datatypes.v,v 1.26.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
include "Init/Notations.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Logic.v,v 1.29 2004/03/29 09:40:49 herbelin Exp $ i*)
+(*i $Id: Logic.v,v 1.29.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
(* UNEXPORTED
Set Implicit Arguments.
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Logic_Type.v,v 1.19 2003/11/29 17:28:30 herbelin Exp $ i*)
+(*i $Id: Logic_Type.v,v 1.19.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
(* UNEXPORTED
Set Implicit Arguments.
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Notations.v,v 1.24 2004/03/17 10:54:50 herbelin Exp $ i*)
+(*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 is imposed by Coq *)
+(*#* These are the notations whose level and associativity are imposed by Coq *)
-(*#* Notations for logical connectives *)
+(*#* Notations for propositional connectives *)
(* NOTATION
Reserved Notation "x <-> y" (at level 95, no associativity).
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Peano.v,v 1.23 2003/11/29 17:28:30 herbelin Exp $ i*)
+(*i $Id: Peano.v,v 1.23.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
(*#* Natural numbers [nat] built from [O] and [S] are defined in Datatypes.v *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Prelude.v,v 1.11 2003/11/29 17:28:30 herbelin Exp $ i*)
+(*i $Id: Prelude.v,v 1.11.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
include "Init/Notations.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Specif.v,v 1.25 2004/04/06 17:30:47 herbelin Exp $ i*)
+(*i $Id: Specif.v,v 1.25.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
(* UNEXPORTED
Set Implicit Arguments.
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
(* UNEXPORTED
Set Implicit Arguments.
*)
-(*i $Id: Wf.v,v 1.17 2003/11/29 17:28:30 herbelin Exp $ i*)
+(*i $Id: Wf.v,v 1.17.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
(*#* This module proves the validity of
- well-founded recursion (also called course of values)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Adalloc.v,v 1.10 2003/11/29 17:28:30 herbelin Exp $ i*)
+(*i $Id: Adalloc.v,v 1.10.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
include "Bool/Bool.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Addec.v,v 1.7 2003/11/29 17:28:31 herbelin Exp $ i*)
+(*i $Id: Addec.v,v 1.7.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
(*#* Equality on adresses *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Addr.v,v 1.8 2003/11/29 17:28:31 herbelin Exp $ i*)
+(*i $Id: Addr.v,v 1.8.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
(*#* Representation of adresses by the [positive] type of binary numbers *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Adist.v,v 1.9 2003/11/29 17:28:31 herbelin Exp $ i*)
+(*i $Id: Adist.v,v 1.9.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
include "Bool/Bool.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Allmaps.v,v 1.3 2003/11/29 17:28:31 herbelin Exp $ i*)
+(*i $Id: Allmaps.v,v 1.3.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
include "IntMap/Addr.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Fset.v,v 1.5 2003/11/29 17:28:31 herbelin Exp $ i*)
+(*i $Id: Fset.v,v 1.5.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
(*s Sets operations on maps *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Lsort.v,v 1.4 2003/11/29 17:28:31 herbelin Exp $ i*)
+(*i $Id: Lsort.v,v 1.4.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
include "Bool/Bool.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Map.v,v 1.7 2003/11/29 17:28:31 herbelin Exp $ i*)
+(*i $Id: Map.v,v 1.7.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
(*#* Definition of finite sets as trees indexed by adresses *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Mapaxioms.v,v 1.4 2003/11/29 17:28:31 herbelin Exp $ i*)
+(*i $Id: Mapaxioms.v,v 1.4.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
include "Bool/Bool.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Mapc.v,v 1.4 2003/11/29 17:28:31 herbelin Exp $ i*)
+(*i $Id: Mapc.v,v 1.4.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
include "Bool/Bool.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Mapcanon.v,v 1.4 2003/11/29 17:28:31 herbelin Exp $ i*)
+(*i $Id: Mapcanon.v,v 1.4.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
include "Bool/Bool.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Mapcard.v,v 1.5 2003/11/29 17:28:31 herbelin Exp $ i*)
+(*i $Id: Mapcard.v,v 1.5.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
include "Bool/Bool.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Mapfold.v,v 1.4 2003/11/29 17:28:31 herbelin Exp $ i*)
+(*i $Id: Mapfold.v,v 1.4.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
include "Bool/Bool.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Mapiter.v,v 1.4 2003/11/29 17:28:31 herbelin Exp $ i*)
+(*i $Id: Mapiter.v,v 1.4.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
include "Bool/Bool.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Maplists.v,v 1.4 2003/11/29 17:28:31 herbelin Exp $ i*)
+(*i $Id: Maplists.v,v 1.4.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
include "IntMap/Addr.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Mapsubset.v,v 1.4 2003/11/29 17:28:32 herbelin Exp $ i*)
+(*i $Id: Mapsubset.v,v 1.4.2.1 2004/07/16 19:31:05 herbelin Exp $ i*)
include "Bool/Bool.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: List.v,v 1.9 2003/12/24 17:10:31 herbelin Exp $ i*)
+(*i $Id: List.v,v 1.9.2.1 2004/07/16 19:31:05 herbelin Exp $ i*)
include "Arith/Le.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: ListSet.v,v 1.13 2003/11/29 17:28:32 herbelin Exp $ i*)
+(*i $Id: ListSet.v,v 1.13.2.1 2004/07/16 19:31:05 herbelin Exp $ i*)
(*#* A Library for finite sets, implemented as lists
A Library with similar interface will soon be available under
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: MonoList.v,v 1.2 2003/11/29 17:28:32 herbelin Exp $ i*)
+(*i $Id: MonoList.v,v 1.2.2.1 2004/07/16 19:31:05 herbelin Exp $ i*)
(*#* THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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: Streams.v,v 1.15.2.1 2004/07/16 19:31:05 herbelin Exp $ i*)
+
+(* UNEXPORTED
+Set Implicit Arguments.
+*)
+
+(*#* Streams *)
+
+(* UNEXPORTED
+Section Streams
+*)
+
+(* UNEXPORTED
+cic:/Coq/Lists/Streams/Streams/A.var
+*)
+
+inline procedural "cic:/Coq/Lists/Streams/Stream.ind".
+
+inline procedural "cic:/Coq/Lists/Streams/hd.con" as definition.
+
+inline procedural "cic:/Coq/Lists/Streams/tl.con" as definition.
+
+inline procedural "cic:/Coq/Lists/Streams/Str_nth_tl.con" as definition.
+
+inline procedural "cic:/Coq/Lists/Streams/Str_nth.con" as definition.
+
+inline procedural "cic:/Coq/Lists/Streams/unfold_Stream.con" as lemma.
+
+inline procedural "cic:/Coq/Lists/Streams/tl_nth_tl.con" as lemma.
+
+(* UNEXPORTED
+Hint Resolve tl_nth_tl: datatypes v62.
+*)
+
+inline procedural "cic:/Coq/Lists/Streams/Str_nth_tl_plus.con" as lemma.
+
+inline procedural "cic:/Coq/Lists/Streams/Str_nth_plus.con" as lemma.
+
+(*#* Extensional Equality between two streams *)
+
+inline procedural "cic:/Coq/Lists/Streams/EqSt.ind".
+
+(*#* A coinduction principle *)
+
+(* UNEXPORTED
+Ltac coinduction proof :=
+ cofix proof; intros; constructor;
+ [ clear proof | try (apply proof; clear proof) ].
+*)
+
+(*#* Extensional equality is an equivalence relation *)
+
+inline procedural "cic:/Coq/Lists/Streams/EqSt_reflex.con" as theorem.
+
+inline procedural "cic:/Coq/Lists/Streams/sym_EqSt.con" as theorem.
+
+inline procedural "cic:/Coq/Lists/Streams/trans_EqSt.con" as theorem.
+
+(*#* The definition given is equivalent to require the elements at each
+ position to be equal *)
+
+inline procedural "cic:/Coq/Lists/Streams/eqst_ntheq.con" as theorem.
+
+inline procedural "cic:/Coq/Lists/Streams/ntheq_eqst.con" as theorem.
+
+(* UNEXPORTED
+Section Stream_Properties
+*)
+
+(* UNEXPORTED
+cic:/Coq/Lists/Streams/Streams/Stream_Properties/P.var
+*)
+
+(*i
+Inductive Exists : Stream -> Prop :=
+ | Here : forall x:Stream, P x -> Exists x
+ | Further : forall x:Stream, ~ P x -> Exists (tl x) -> Exists x.
+i*)
+
+inline procedural "cic:/Coq/Lists/Streams/Exists.ind".
+
+inline procedural "cic:/Coq/Lists/Streams/ForAll.ind".
+
+(* UNEXPORTED
+Section Co_Induction_ForAll
+*)
+
+(* UNEXPORTED
+cic:/Coq/Lists/Streams/Streams/Stream_Properties/Co_Induction_ForAll/Inv.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Lists/Streams/Streams/Stream_Properties/Co_Induction_ForAll/InvThenP.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Lists/Streams/Streams/Stream_Properties/Co_Induction_ForAll/InvIsStable.var
+*)
+
+inline procedural "cic:/Coq/Lists/Streams/ForAll_coind.con" as theorem.
+
+(* UNEXPORTED
+End Co_Induction_ForAll
+*)
+
+(* UNEXPORTED
+End Stream_Properties
+*)
+
+(* UNEXPORTED
+End Streams
+*)
+
+(* UNEXPORTED
+Section Map
+*)
+
+(* UNEXPORTED
+cic:/Coq/Lists/Streams/Map/A.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Lists/Streams/Map/B.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Lists/Streams/Map/f.var
+*)
+
+inline procedural "cic:/Coq/Lists/Streams/map.con" as definition.
+
+(* UNEXPORTED
+End Map
+*)
+
+(* UNEXPORTED
+Section Constant_Stream
+*)
+
+(* UNEXPORTED
+cic:/Coq/Lists/Streams/Constant_Stream/A.var
+*)
+
+(* UNEXPORTED
+cic:/Coq/Lists/Streams/Constant_Stream/a.var
+*)
+
+inline procedural "cic:/Coq/Lists/Streams/const.con" as definition.
+
+(* UNEXPORTED
+End Constant_Stream
+*)
+
+(* UNEXPORTED
+Unset Implicit Arguments.
+*)
+
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: TheoryList.v,v 1.15 2004/03/28 14:41:45 herbelin Exp $ i*)
+(*i $Id: TheoryList.v,v 1.15.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
(*#* Some programs and results about lists following CAML Manual *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Berardi.v,v 1.5 2003/11/29 17:28:33 herbelin Exp $ i*)
+(*i $Id: Berardi.v,v 1.5.2.2 2004/08/03 17:42:43 herbelin Exp $ i*)
(*#* This file formalizes Berardi's paradox which says that in
the calculus of constructions, excluded middle (EM) and axiom of
- choice (AC) implie proof irrelevenace (PI).
+ choice (AC) imply proof irrelevance (PI).
Here, the axiom of choice is not necessary because of the use
of inductive types.
<<
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: ChoiceFacts.v,v 1.7 2003/12/24 10:27:05 barras Exp $ i*)
+(*i $Id: ChoiceFacts.v,v 1.7.2.2 2004/08/01 09:29:59 herbelin Exp $ i*)
-(* We show that the functional formulation of the axiom of Choice
+(*#* We show that the functional formulation of the axiom of Choice
(usual formulation in type theory) is equivalent to its relational
formulation (only formulation of set theory) + the axiom of
(parametric) definite description (aka axiom of unique choice) *)
-(* This shows that the axiom of choice can be assumed (under its
+(*#* This shows that the axiom of choice can be assumed (under its
relational formulation) without known inconsistency with classical logic,
though definite description conflicts with classical logic *)
inline procedural "cic:/Coq/Logic/ChoiceFacts/FunChoice_Equiv_RelChoice_and_ParamDefinDescr.con" as theorem.
-(* We show that the guarded relational formulation of the axiom of Choice
+(*#* We show that the guarded relational formulation of the axiom of Choice
comes from the non guarded formulation in presence either of the
independance of premises or proof-irrelevance *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Classical.v,v 1.6 2003/11/29 17:28:33 herbelin Exp $ i*)
+(*i $Id: Classical.v,v 1.6.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
(*#* Classical Logic *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: ClassicalChoice.v,v 1.4 2003/12/15 19:48:19 barras Exp $ i*)
+(*i $Id: ClassicalChoice.v,v 1.4.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
(*#* This file provides classical logic and functional choice *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: ClassicalDescription.v,v 1.7 2004/03/17 00:11:13 herbelin Exp $ i*)
+(*i $Id: ClassicalDescription.v,v 1.7.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
(*#* This file provides classical logic and definite description *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: ClassicalFacts.v,v 1.6 2004/03/17 00:11:13 herbelin Exp $ i*)
+(*i $Id: ClassicalFacts.v,v 1.6.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
(*#* Some facts and definitions about classical logic *)
cic:/Coq/Logic/ClassicalFacts/Proof_irrelevance_gen/bool_elim_redr.var
*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Logic/ClassicalFacts/Proof_irrelevance_gen/bool_dep_induction.con *)
+
inline procedural "cic:/Coq/Logic/ClassicalFacts/Proof_irrelevance_gen/bool_dep_induction.con" "Proof_irrelevance_gen__" as definition.
inline procedural "cic:/Coq/Logic/ClassicalFacts/aux.con" as lemma.
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Classical_Pred_Set.v,v 1.6 2003/12/15 19:48:19 barras Exp $ i*)
+(*i $Id: Classical_Pred_Set.v,v 1.6.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
(*#* Classical Predicate Logic on Set*)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Classical_Pred_Type.v,v 1.6 2003/12/15 19:48:19 barras Exp $ i*)
+(*i $Id: Classical_Pred_Type.v,v 1.6.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
(*#* Classical Predicate Logic on Type *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Classical_Prop.v,v 1.6 2003/11/29 17:28:33 herbelin Exp $ i*)
+(*i $Id: Classical_Prop.v,v 1.6.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
(*#* Classical Propositional Logic *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Classical_Type.v,v 1.5 2003/11/29 17:28:33 herbelin Exp $ i*)
+(*i $Id: Classical_Type.v,v 1.5.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
(*#* Classical Logic for Type *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Decidable.v,v 1.5 2003/11/29 17:28:33 herbelin Exp $ i*)
+(*i $Id: Decidable.v,v 1.5.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
(*#* Properties of decidable propositions *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Diaconescu.v,v 1.5 2003/12/24 10:27:05 barras Exp $ i*)
+(*i $Id: Diaconescu.v,v 1.5.2.3 2004/08/01 09:36:44 herbelin Exp $ i*)
-(* R. Diaconescu [Diaconescu] showed that the Axiom of Choice in Set Theory
+(*#* R. Diaconescu [Diaconescu] showed that the Axiom of Choice in Set Theory
entails Excluded-Middle; S. Lacas and B. Werner [LacasWerner]
adapted the proof to show that the axiom of choice in equivalence
classes entails Excluded-Middle in Type Theory.
Section PredExt_GuardRelChoice_imp_EM
*)
-(* The axiom of extensionality for predicates *)
+(*#* The axiom of extensionality for predicates *)
inline procedural "cic:/Coq/Logic/Diaconescu/PredicateExtensionality.con" as definition.
-(* From predicate extensionality we get propositional extensionality
+(*#* From predicate extensionality we get propositional extensionality
hence proof-irrelevance *)
include "Logic/ClassicalFacts.ma".
inline procedural "cic:/Coq/Logic/Diaconescu/proof_irrel.con" as lemma.
-(* From proof-irrelevance and relational choice, we get guarded
+(*#* From proof-irrelevance and relational choice, we get guarded
relational choice *)
include "Logic/ChoiceFacts.ma".
inline procedural "cic:/Coq/Logic/Diaconescu/guarded_rel_choice.con" as lemma.
-(* The form of choice we need: there is a functional relation which chooses
- an element in any non empty subset of bool *)
+(*#* The form of choice we need: there is a functional relation which chooses
+ an element in any non empty subset of bool *)
include "Bool/Bool.ma".
inline procedural "cic:/Coq/Logic/Diaconescu/AC.con" as lemma.
-(* The proof of the excluded middle *)
+(*#* The proof of the excluded middle *)
-(* Remark: P could have been in Set or Type *)
+(*#* Remark: P could have been in Set or Type *)
inline procedural "cic:/Coq/Logic/Diaconescu/pred_ext_and_rel_choice_imp_EM.con" as theorem.
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Eqdep.v,v 1.10 2004/01/27 14:37:30 herbelin Exp $ i*)
+(*i $Id: Eqdep.v,v 1.10.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
(*#* This file defines dependent equality and shows its equivalence with
equality on dependent pairs (inhabiting sigma-types). It axiomatizes
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Eqdep_dec.v,v 1.14 2003/11/29 17:28:33 herbelin Exp $ i*)
+(*i $Id: Eqdep_dec.v,v 1.14.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
(*#* We prove that there is only one proof of [x=x], i.e [(refl_equal ? x)].
This holds if the equality upon the set of [x] is decidable.
cic:/Coq/Logic/Eqdep_dec/DecidableEqDep/A.var
*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Logic/Eqdep_dec/DecidableEqDep/comp.con ***)
+
inline procedural "cic:/Coq/Logic/Eqdep_dec/DecidableEqDep/comp.con" "DecidableEqDep__" as definition.
inline procedural "cic:/Coq/Logic/Eqdep_dec/trans_sym_eqT.con" as remark.
cic:/Coq/Logic/Eqdep_dec/DecidableEqDep/x.var
*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Logic/Eqdep_dec/DecidableEqDep/nu.con *****)
+
inline procedural "cic:/Coq/Logic/Eqdep_dec/DecidableEqDep/nu.con" "DecidableEqDep__" as definition.
+(* UNAVAILABLE OBJECT: cic:/Coq/Logic/Eqdep_dec/DecidableEqDep/nu_constant.con *)
+
inline procedural "cic:/Coq/Logic/Eqdep_dec/DecidableEqDep/nu_constant.con" "DecidableEqDep__" as definition.
+(* UNAVAILABLE OBJECT: cic:/Coq/Logic/Eqdep_dec/DecidableEqDep/nu_inv.con *)
+
inline procedural "cic:/Coq/Logic/Eqdep_dec/DecidableEqDep/nu_inv.con" "DecidableEqDep__" as definition.
inline procedural "cic:/Coq/Logic/Eqdep_dec/nu_left_inv.con" as remark.
(*#* The corollary *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Logic/Eqdep_dec/DecidableEqDep/proj.con ***)
+
inline procedural "cic:/Coq/Logic/Eqdep_dec/DecidableEqDep/proj.con" "DecidableEqDep__" as definition.
inline procedural "cic:/Coq/Logic/Eqdep_dec/inj_right_pair.con" as theorem.
include "Coq.ma".
-(*#***************************************************************************)
+(*#***********************************************************************)
-(* The Calculus of Inductive Constructions *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* Projet LogiCal *)
+(* \VV/ **************************************************************)
-(* *)
+(* // * This file is distributed under the terms of the *)
-(* INRIA LRI-CNRS *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(* Rocquencourt Orsay *)
+(*#***********************************************************************)
-(* *)
+(* Hurkens.v *)
-(* May 29th 2002 *)
-
-(* *)
-
-(*#***************************************************************************)
-
-(* Hurkens.v *)
-
-(*#***************************************************************************)
+(*#***********************************************************************)
(*#* This is Hurkens paradox [Hurkens] in system U-, adapted by Herman
Geuvers [Geuvers] to show the inconsistency in the pure calculus of
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: JMeq.v,v 1.8 2003/11/29 17:28:33 herbelin Exp $ i*)
+(*i $Id: JMeq.v,v 1.8.2.2 2004/08/03 17:42:32 herbelin Exp $ i*)
-(*#* John Major's Equality as proposed by C. Mc Bride *)
+(*#* John Major's Equality as proposed by C. Mc Bride
+
+ Reference:
+
+ [McBride] Elimination with a Motive, Proceedings of TYPES 2000,
+ LNCS 2277, pp 197-216, 2002.
+
+*)
(* UNEXPORTED
Set Implicit Arguments.
include "Coq.ma".
-(*#***************************************************************************)
+(*#***********************************************************************)
-(* The Calculus of Inductive Constructions *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* Projet LogiCal *)
+(* \VV/ **************************************************************)
-(* *)
+(* // * This file is distributed under the terms of the *)
-(* INRIA LRI-CNRS *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(* Rocquencourt Orsay *)
-
-(* *)
-
-(* May 29th 2002 *)
-
-(* *)
-
-(*#***************************************************************************)
+(*#***********************************************************************)
(*#* This is a proof in the pure Calculus of Construction that
classical logic in Prop + dependent elimination of disjunction entails
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: RelationalChoice.v,v 1.3 2003/12/15 19:48:19 barras Exp $ i*)
+(*i $Id: RelationalChoice.v,v 1.3.2.2 2004/08/01 09:29:59 herbelin Exp $ i*)
-(* This file axiomatizes the relational form of the axiom of choice *)
+(*#* This file axiomatizes the relational form of the axiom of choice *)
inline procedural "cic:/Coq/Logic/RelationalChoice/relational_choice.con".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: BinNat.v,v 1.7 2003/11/29 17:28:34 herbelin Exp $ i*)
+(*i $Id: BinNat.v,v 1.7.2.1 2004/07/16 19:31:07 herbelin Exp $ i*)
include "NArith/BinPos.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: BinPos.v,v 1.7 2003/12/15 19:48:20 barras Exp $ i*)
+(*i $Id: BinPos.v,v 1.7.2.1 2004/07/16 19:31:07 herbelin Exp $ i*)
(*#*********************************************************************)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* $Id: NArith.v,v 1.2 2003/11/29 17:28:34 herbelin Exp $ *)
+(* $Id: NArith.v,v 1.2.2.1 2004/07/16 19:31:07 herbelin Exp $ *)
(*#* Library for binary natural numbers *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Pnat.v,v 1.3 2003/12/15 19:48:20 barras Exp $ i*)
+(*i $Id: Pnat.v,v 1.3.2.1 2004/07/16 19:31:07 herbelin Exp $ i*)
include "NArith/BinPos.ma".
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 *)
-
-(*#**********************************************************************)
-
include "Num/Axioms.ma".
include "Num/EqAxioms.ma".
-(*#* This file contains basic properties of addition with respect to equality *)
-
-(*#* Properties of Addition *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/AddProps/add_x_0.con ******************)
inline procedural "cic:/Coq/Num/AddProps/add_x_0.con" as lemma.
-(* UNEXPORTED
-Hints Resolve add_x_0 : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/AddProps/add_x_Sy.con *****************)
inline procedural "cic:/Coq/Num/AddProps/add_x_Sy.con" as lemma.
-(* UNEXPORTED
-Hints Resolve add_x_Sy : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/AddProps/add_x_Sy_swap.con ************)
inline procedural "cic:/Coq/Num/AddProps/add_x_Sy_swap.con" as lemma.
-(* UNEXPORTED
-Hints Resolve add_x_Sy_swap : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/AddProps/add_Sx_y_swap.con ************)
inline procedural "cic:/Coq/Num/AddProps/add_Sx_y_swap.con" as lemma.
-(* UNEXPORTED
-Hints Resolve add_Sx_y_swap : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/AddProps/add_assoc_r.con **************)
inline procedural "cic:/Coq/Num/AddProps/add_assoc_r.con" as lemma.
-(* UNEXPORTED
-Hints Resolve add_assoc_r : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/AddProps/add_x_y_z_perm.con ***********)
inline procedural "cic:/Coq/Num/AddProps/add_x_y_z_perm.con" as lemma.
-(* UNEXPORTED
-Hints Resolve add_x_y_z_perm : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/AddProps/add_x_one_S.con **************)
inline procedural "cic:/Coq/Num/AddProps/add_x_one_S.con" as lemma.
-(* UNEXPORTED
-Hints Resolve add_x_one_S : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/AddProps/add_one_x_S.con **************)
inline procedural "cic:/Coq/Num/AddProps/add_one_x_S.con" as lemma.
-(* UNEXPORTED
-Hints Resolve add_one_x_S : num.
-*)
-
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: Axioms.v,v 1.6 2002/02/14 14:39:02 filliatr Exp $ i*)
-
-(*#* Axioms for the basic numerical operations *)
-
include "Num/Params.ma".
include "Num/EqParams.ma".
include "Num/NSyntax.ma".
-(*#* Axioms for [eq] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/eq_refl.con ********************)
inline procedural "cic:/Coq/Num/Axioms/eq_refl.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/eq_sym.con *********************)
+
inline procedural "cic:/Coq/Num/Axioms/eq_sym.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/eq_trans.con *******************)
+
inline procedural "cic:/Coq/Num/Axioms/eq_trans.con".
-(*#* Axioms for [add] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/add_sym.con ********************)
inline procedural "cic:/Coq/Num/Axioms/add_sym.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/add_assoc_l.con ****************)
+
inline procedural "cic:/Coq/Num/Axioms/add_assoc_l.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/add_0_x.con ********************)
+
inline procedural "cic:/Coq/Num/Axioms/add_0_x.con".
-(*#* Axioms for [S] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/add_Sx_y.con *******************)
inline procedural "cic:/Coq/Num/Axioms/add_Sx_y.con".
-(*#* Axioms for [one] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/S_0_1.con **********************)
inline procedural "cic:/Coq/Num/Axioms/S_0_1.con".
-(*#* Axioms for [<],
- properties of [>], [<=] and [>=] will be derived from [<] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/lt_trans.con *******************)
inline procedural "cic:/Coq/Num/Axioms/lt_trans.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/lt_anti_refl.con ***************)
+
inline procedural "cic:/Coq/Num/Axioms/lt_anti_refl.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/lt_x_Sx.con ********************)
+
inline procedural "cic:/Coq/Num/Axioms/lt_x_Sx.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/lt_S_compat.con ****************)
+
inline procedural "cic:/Coq/Num/Axioms/lt_S_compat.con".
-inline procedural "cic:/Coq/Num/Axioms/lt_add_compat_l.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/lt_add_compat_l.con ************)
-(* UNEXPORTED
-Hints Resolve add_sym add_assoc_l add_0_x add_Sx_y S_0_1 lt_x_Sx lt_S_compat
- lt_trans lt_anti_refl lt_add_compat_l : num.
-*)
+inline procedural "cic:/Coq/Num/Axioms/lt_add_compat_l.con".
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: Definitions.v,v 1.3 2002/02/14 14:39:02 filliatr Exp $ i*)
-
-(*#* Axiomatisation of a numerical set
-
- It will be instantiated by Z and R later on
- We choose to introduce many operation to allow flexibility in definition
- ([S] is primitive in the definition of [nat] while [add] and [one]
- are primitive in the definition
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/N.con *********************)
inline procedural "cic:/Coq/Num/Definitions/N.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/zero.con ******************)
+
inline procedural "cic:/Coq/Num/Definitions/zero.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/one.con *******************)
+
inline procedural "cic:/Coq/Num/Definitions/one.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/add.con *******************)
+
inline procedural "cic:/Coq/Num/Definitions/add.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/S.con *********************)
+
inline procedural "cic:/Coq/Num/Definitions/S.con".
-(*#* Relations *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/eq.con ********************)
inline procedural "cic:/Coq/Num/Definitions/eq.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/lt.con ********************)
+
inline procedural "cic:/Coq/Num/Definitions/lt.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/le.con ********************)
+
inline procedural "cic:/Coq/Num/Definitions/le.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/gt.con ********************)
+
inline procedural "cic:/Coq/Num/Definitions/gt.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/ge.con ********************)
+
inline procedural "cic:/Coq/Num/Definitions/ge.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Definitions/neq.con *******************)
+
inline procedural "cic:/Coq/Num/Definitions/neq.con" as definition.
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: DiscrAxioms.v,v 1.4 2002/02/14 14:39:02 filliatr Exp $ i*)
-
include "Num/Params.ma".
include "Num/NSyntax.ma".
-(*#* Axiom for a discrete set *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/DiscrAxioms/lt_x_Sy_le.con ************)
inline procedural "cic:/Coq/Num/DiscrAxioms/lt_x_Sy_le.con".
-(* UNEXPORTED
-Hints Resolve lt_x_Sy_le : num.
-*)
-
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: DiscrProps.v,v 1.4 2002/04/17 11:30:20 herbelin Exp $ i*)
-
include "Num/DiscrAxioms.ma".
include "Num/LtProps.ma".
-(*#* Properties of a discrete order *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/DiscrProps/lt_le_Sx_y.con *************)
inline procedural "cic:/Coq/Num/DiscrProps/lt_le_Sx_y.con" as lemma.
-(* UNEXPORTED
-Hints Resolve lt_le_Sx_y : num.
-*)
-
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: EqAxioms.v,v 1.3 2002/02/14 14:39:02 filliatr Exp $ i*)
-
-(*#* Axioms for equality *)
-
include "Num/Params.ma".
include "Num/EqParams.ma".
include "Num/NSyntax.ma".
-(*#* Basic Axioms for [eq] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/EqAxioms/eq_refl.con ******************)
inline procedural "cic:/Coq/Num/EqAxioms/eq_refl.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/EqAxioms/eq_sym.con *******************)
+
inline procedural "cic:/Coq/Num/EqAxioms/eq_sym.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/EqAxioms/eq_trans.con *****************)
+
inline procedural "cic:/Coq/Num/EqAxioms/eq_trans.con".
-(*#* Axioms for [eq] and [add] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/EqAxioms/add_eq_compat.con ************)
inline procedural "cic:/Coq/Num/EqAxioms/add_eq_compat.con".
-(*#* Axioms for [eq] and [S] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/EqAxioms/S_eq_compat.con **************)
inline procedural "cic:/Coq/Num/EqAxioms/S_eq_compat.con".
-(*#* Axioms for [eq] and [<] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/EqAxioms/lt_eq_compat.con *************)
inline procedural "cic:/Coq/Num/EqAxioms/lt_eq_compat.con".
-(* UNEXPORTED
-Hints Resolve eq_refl eq_trans add_eq_compat S_eq_compat lt_eq_compat : num.
-*)
-
-(* UNEXPORTED
-Hints Immediate eq_sym : num.
-*)
-
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: EqParams.v,v 1.4 2003/03/21 17:37:16 barras Exp $ i*)
-
-(*#* Equality is introduced as an independant parameter, it could be
- instantiated with Leibniz equality *)
-
include "Num/Params.ma".
-inline procedural "cic:/Coq/Num/EqParams/eqN.con".
-
-(*i Infix 6 "=" eqN V8only 50. i*)
-
-(* NOTATION
-Grammar constr constr1 :=
-eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ].
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/EqParams/eqN.con **********************)
-(* NOTATION
-Syntax constr
- level 1:
- equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "=" $t2:E ] ]
-.
-*)
+inline procedural "cic:/Coq/Num/EqParams/eqN.con".
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: GeAxioms.v,v 1.3 2002/02/14 14:39:02 filliatr Exp $ i*)
-
include "Num/Axioms.ma".
include "Num/LtProps.ma".
-(*#* Axiomatizing [>=] from [<] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/GeAxioms/not_lt_ge.con ****************)
inline procedural "cic:/Coq/Num/GeAxioms/not_lt_ge.con".
-inline procedural "cic:/Coq/Num/GeAxioms/ge_not_lt.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/GeAxioms/ge_not_lt.con ****************)
-(* UNEXPORTED
-Hints Resolve not_lt_ge : num.
-*)
-
-(* UNEXPORTED
-Hints Immediate ge_not_lt : num.
-*)
+inline procedural "cic:/Coq/Num/GeAxioms/ge_not_lt.con".
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 *)
-
-(*#**********************************************************************)
-
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: GtAxioms.v,v 1.3 2002/02/14 14:39:02 filliatr Exp $ i*)
-
include "Num/Axioms.ma".
include "Num/LeProps.ma".
-(*#* Axiomatizing [>] from [<] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/GtAxioms/not_le_gt.con ****************)
inline procedural "cic:/Coq/Num/GtAxioms/not_le_gt.con".
-inline procedural "cic:/Coq/Num/GtAxioms/gt_not_le.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/GtAxioms/gt_not_le.con ****************)
-(* UNEXPORTED
-Hints Resolve not_le_gt : num.
-*)
-
-(* UNEXPORTED
-Hints Immediate gt_not_le : num.
-*)
+inline procedural "cic:/Coq/Num/GtAxioms/gt_not_le.con".
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 *)
-
-(*#**********************************************************************)
-
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: LeAxioms.v,v 1.3 2002/02/14 14:39:02 filliatr Exp $ i*)
-
include "Num/Axioms.ma".
include "Num/LtProps.ma".
-(*#* Axiomatizing [<=] from [<] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeAxioms/lt_or_eq_le.con **************)
inline procedural "cic:/Coq/Num/LeAxioms/lt_or_eq_le.con".
-inline procedural "cic:/Coq/Num/LeAxioms/le_lt_or_eq.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeAxioms/le_lt_or_eq.con **************)
-(* UNEXPORTED
-Hints Resolve lt_or_eq_le : num.
-*)
-
-(* UNEXPORTED
-Hints Immediate le_lt_or_eq : num.
-*)
+inline procedural "cic:/Coq/Num/LeAxioms/le_lt_or_eq.con".
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 *)
-
-(*#**********************************************************************)
-
include "Num/LtProps.ma".
include "Num/LeAxioms.ma".
-(*#* Properties of the relation [<=] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/lt_le.con *********************)
inline procedural "cic:/Coq/Num/LeProps/lt_le.con" as lemma.
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/eq_le.con *********************)
+
inline procedural "cic:/Coq/Num/LeProps/eq_le.con" as lemma.
-(*#* compatibility with equality *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_eq_compat.con **************)
inline procedural "cic:/Coq/Num/LeProps/le_eq_compat.con" as lemma.
-(* UNEXPORTED
-Hints Resolve le_eq_compat : num.
-*)
-
-(*#* Transitivity *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_trans.con ******************)
inline procedural "cic:/Coq/Num/LeProps/le_trans.con" as lemma.
-(* UNEXPORTED
-Hints Resolve le_trans : num.
-*)
-
-(*#* compatibility with equality, addition and successor *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_add_compat_l.con ***********)
inline procedural "cic:/Coq/Num/LeProps/le_add_compat_l.con" as lemma.
-(* UNEXPORTED
-Hints Resolve le_add_compat_l : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_add_compat_r.con ***********)
inline procedural "cic:/Coq/Num/LeProps/le_add_compat_r.con" as lemma.
-(* UNEXPORTED
-Hints Resolve le_add_compat_r : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_add_compat.con *************)
inline procedural "cic:/Coq/Num/LeProps/le_add_compat.con" as lemma.
-(* UNEXPORTED
-Hints Immediate le_add_compat : num.
-*)
-
-(* compatibility with successor *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_S_compat.con ***************)
inline procedural "cic:/Coq/Num/LeProps/le_S_compat.con" as lemma.
-(* UNEXPORTED
-Hints Resolve le_S_compat : num.
-*)
-
-(*#* relating [<=] with [<] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_lt_x_Sy.con ****************)
inline procedural "cic:/Coq/Num/LeProps/le_lt_x_Sy.con" as lemma.
-(* UNEXPORTED
-Hints Immediate le_lt_x_Sy : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_le_x_Sy.con ****************)
inline procedural "cic:/Coq/Num/LeProps/le_le_x_Sy.con" as lemma.
-(* UNEXPORTED
-Hints Immediate le_le_x_Sy : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_Sx_y_lt.con ****************)
inline procedural "cic:/Coq/Num/LeProps/le_Sx_y_lt.con" as lemma.
-(* UNEXPORTED
-Hints Immediate le_Sx_y_lt : num.
-*)
-
-(*#* Combined transitivity *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/lt_le_trans.con ***************)
inline procedural "cic:/Coq/Num/LeProps/lt_le_trans.con" as lemma.
-inline procedural "cic:/Coq/Num/LeProps/le_lt_trans.con" as lemma.
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_lt_trans.con ***************)
-(* UNEXPORTED
-Hints Immediate lt_le_trans le_lt_trans : num.
-*)
+inline procedural "cic:/Coq/Num/LeProps/le_lt_trans.con" as lemma.
-(*#* weaker compatibility results involving [<] and [<=] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/lt_add_compat_weak_l.con ******)
inline procedural "cic:/Coq/Num/LeProps/lt_add_compat_weak_l.con" as lemma.
-(* UNEXPORTED
-Hints Immediate lt_add_compat_weak_l : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/lt_add_compat_weak_r.con ******)
inline procedural "cic:/Coq/Num/LeProps/lt_add_compat_weak_r.con" as lemma.
-(* UNEXPORTED
-Hints Immediate lt_add_compat_weak_r : num.
-*)
-
include "Coq.ma".
-(*s Instantiating [eqN] with Leibniz equality *)
-
include "Num/NSyntax.ma".
-inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/eqN.con" as definition.
-
-(* UNEXPORTED
-Hints Unfold eqN : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/EqAxioms/eqN.con **************)
-(* NOTATION
-Grammar constr constr1 :=
-eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ].
-*)
-
-(* NOTATION
-Syntax constr
- level 1:
- equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "=" $t2:E ] ].
-*)
+inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/eqN.con" as definition.
-(*s Lemmas for [eqN] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/EqAxioms/eq_refl.con **********)
inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/eq_refl.con" as lemma.
-inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/eq_sym.con" as lemma.
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/EqAxioms/eq_sym.con ***********)
-inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/eq_trans.con" as lemma.
+inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/eq_sym.con" as lemma.
-(* UNEXPORTED
-Hints Resolve eq_refl eq_trans : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/EqAxioms/eq_trans.con *********)
-(* UNEXPORTED
-Hints Immediate eq_sym : num.
-*)
+inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/eq_trans.con" as lemma.
-(*s Compatibility lemmas for [S], [add], [lt] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/EqAxioms/S_eq_compat.con ******)
inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/S_eq_compat.con" as lemma.
-(* UNEXPORTED
-Hints Resolve S_eq_compat : nat.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/EqAxioms/add_eq_compat.con ****)
inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/add_eq_compat.con" as lemma.
-(* UNEXPORTED
-Hints Resolve add_eq_compat : nat.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/EqAxioms/lt_eq_compat.con *****)
inline procedural "cic:/Coq/Num/Leibniz/EqAxioms/lt_eq_compat.con" as lemma.
-(* UNEXPORTED
-Hints Resolve add_eq_compat S_eq_compat lt_eq_compat : num.
-*)
-
include "Coq.ma".
-(*s Syntax for arithmetic *)
-
include "Num/Params.ma".
-(* NOTATION
-Infix 6 "<" lt.
-*)
-
-(* NOTATION
-Infix 6 "<=" le.
-*)
-
-(* NOTATION
-Infix 6 ">" gt.
-*)
-
-(* NOTATION
-Infix 6 ">=" ge.
-*)
-
-(*i Infix 7 "+" plus. i*)
-
-(* NOTATION
-Grammar constr lassoc_constr4 :=
- squash_sum
- [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
- case [$c2] of
- (SQUASH $T2) ->
- case [$c1] of
- (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
- | $_ -> [ (sumor $c1 $T2) ] (* c1+{T2} *)
- esac
- | $_ -> [ (add $c1 $c2) ] (* c1+c2 *)
- esac.
-*)
-
-(* NOTATION
-Syntax constr
- level 1:
- equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "=" $t2:E ] ]
- ;
-
- level 4:
- sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
-.
-*)
-
include "Coq.ma".
-(*i $Id $ i*)
-
-(*s
- Axiomatisation of a numerical set
- It will be instantiated by Z and R later on
- We choose to introduce many operation to allow flexibility in definition
- ([S] is primitive in the definition of [nat] while [add] and [one]
- are primitive in the definition
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/Params/N.con ******************)
inline procedural "cic:/Coq/Num/Leibniz/Params/N.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/Params/zero.con ***************)
+
inline procedural "cic:/Coq/Num/Leibniz/Params/zero.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/Params/one.con ****************)
+
inline procedural "cic:/Coq/Num/Leibniz/Params/one.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/Params/add.con ****************)
+
inline procedural "cic:/Coq/Num/Leibniz/Params/add.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/Params/S.con ******************)
+
inline procedural "cic:/Coq/Num/Leibniz/Params/S.con".
-(*s Relations, equality is defined separately *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/Params/lt.con *****************)
inline procedural "cic:/Coq/Num/Leibniz/Params/lt.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/Params/le.con *****************)
+
inline procedural "cic:/Coq/Num/Leibniz/Params/le.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/Params/gt.con *****************)
+
inline procedural "cic:/Coq/Num/Leibniz/Params/gt.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/Params/ge.con *****************)
+
inline procedural "cic:/Coq/Num/Leibniz/Params/ge.con".
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 *)
-
-(*#**********************************************************************)
-
include "Num/Axioms.ma".
include "Num/AddProps.ma".
include "Num/NeqProps.ma".
-(*#* This file contains basic properties of the less than relation *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LtProps/lt_anti_sym.con ***************)
inline procedural "cic:/Coq/Num/LtProps/lt_anti_sym.con" as lemma.
-(* UNEXPORTED
-Hints Resolve lt_anti_refl : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LtProps/eq_not_lt.con *****************)
inline procedural "cic:/Coq/Num/LtProps/eq_not_lt.con" as lemma.
-(* UNEXPORTED
-Hints Resolve eq_not_lt : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LtProps/lt_0_1.con ********************)
inline procedural "cic:/Coq/Num/LtProps/lt_0_1.con" as lemma.
-(* UNEXPORTED
-Hints Resolve lt_0_1 : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LtProps/eq_lt_x_Sy.con ****************)
inline procedural "cic:/Coq/Num/LtProps/eq_lt_x_Sy.con" as lemma.
-(* UNEXPORTED
-Hints Resolve eq_lt_x_Sy : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LtProps/lt_lt_x_Sy.con ****************)
inline procedural "cic:/Coq/Num/LtProps/lt_lt_x_Sy.con" as lemma.
-(* UNEXPORTED
-Hints Immediate lt_lt_x_Sy : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LtProps/lt_Sx_y_lt.con ****************)
inline procedural "cic:/Coq/Num/LtProps/lt_Sx_y_lt.con" as lemma.
-(* UNEXPORTED
-Hints Immediate lt_Sx_y_lt : num.
-*)
-
-(*#* Relating [<] and [=] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LtProps/lt_neq.con ********************)
inline procedural "cic:/Coq/Num/LtProps/lt_neq.con" as lemma.
-(* UNEXPORTED
-Hints Immediate lt_neq : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LtProps/lt_neq_sym.con ****************)
inline procedural "cic:/Coq/Num/LtProps/lt_neq_sym.con" as lemma.
-(* UNEXPORTED
-Hints Immediate lt_neq_sym : num.
-*)
-
-(*#* Application to inequalities properties *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LtProps/neq_x_Sx.con ******************)
inline procedural "cic:/Coq/Num/LtProps/neq_x_Sx.con" as lemma.
-(* UNEXPORTED
-Hints Resolve neq_x_Sx : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LtProps/neq_0_1.con *******************)
inline procedural "cic:/Coq/Num/LtProps/neq_0_1.con" as lemma.
-(* UNEXPORTED
-Hints Resolve neq_0_1 : num.
-*)
-
-(*#* Relating [<] and [+] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LtProps/lt_add_compat_r.con ***********)
inline procedural "cic:/Coq/Num/LtProps/lt_add_compat_r.con" as lemma.
-(* UNEXPORTED
-Hints Resolve lt_add_compat_r : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LtProps/lt_add_compat.con *************)
inline procedural "cic:/Coq/Num/LtProps/lt_add_compat.con" as lemma.
-(* UNEXPORTED
-Hints Immediate lt_add_compat : num.
-*)
-
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 *)
-
-(*#**********************************************************************)
-
-(*#* Syntax for arithmetic *)
-
include "Num/Params.ma".
-(* NOTATION
-Infix 6 "<" lt V8only 70.
-*)
-
-(* NOTATION
-Infix 6 "<=" le V8only 70.
-*)
-
-(* NOTATION
-Infix 6 ">" gt V8only 70.
-*)
-
-(* NOTATION
-Infix 6 ">=" ge V8only 70.
-*)
-
-(*i Infix 7 "+" plus V8only 50. i*)
-
-(* NOTATION
-Grammar constr lassoc_constr4 :=
- squash_sum
- [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
- case [$c2] of
- (SQUASH $T2) ->
- case [$c1] of
- (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
- | $_ -> [ (sumor $c1 $T2) ] (* c1+{T2} *)
- esac
- | $_ -> [ (add $c1 $c2) ] (* c1+c2 *)
- esac.
-*)
-
-(* NOTATION
-Syntax constr
- level 4:
- sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
-.
-*)
-
include "Coq.ma".
-(*i $Id: i*)
-
-(*s Axioms for the basic numerical operations *)
-
include "Num/Params.ma".
include "Num/EqAxioms.ma".
include "Num/NSyntax.ma".
-(*s Lemmas for [add] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/add_Sx_y.con ***************)
inline procedural "cic:/Coq/Num/Nat/Axioms/add_Sx_y.con" as lemma.
-(* UNEXPORTED
-Hints Resolve add_Sx_y : nat.
-*)
-
-(*s Lemmas for [add] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/add_0_x.con ****************)
inline procedural "cic:/Coq/Num/Nat/Axioms/add_0_x.con" as lemma.
-(* UNEXPORTED
-Hints Resolve add_0_x : nat.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/add_sym.con ****************)
inline procedural "cic:/Coq/Num/Nat/Axioms/add_sym.con" as lemma.
-(* UNEXPORTED
-Hints Resolve add_sym : nat.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/add_eq_compat.con **********)
inline procedural "cic:/Coq/Num/Nat/Axioms/add_eq_compat.con" as lemma.
-(* UNEXPORTED
-Hints Resolve add_eq_compat : nat.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/add_assoc_l.con ************)
inline procedural "cic:/Coq/Num/Nat/Axioms/add_assoc_l.con" as lemma.
-(*s Lemmas for [one] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/S_0_1.con ******************)
inline procedural "cic:/Coq/Num/Nat/Axioms/S_0_1.con" as lemma.
-(*s Lemmas for [<],
- properties of [>], [<=] and [>=] will be derived from [<] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/lt_trans.con ***************)
inline procedural "cic:/Coq/Num/Nat/Axioms/lt_trans.con" as lemma.
-(* UNEXPORTED
-Hints Resolve lt_trans : nat.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/lt_x_Sx.con ****************)
inline procedural "cic:/Coq/Num/Nat/Axioms/lt_x_Sx.con" as lemma.
-(* UNEXPORTED
-Hints Resolve lt_x_Sx : nat.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/lt_S_compat.con ************)
inline procedural "cic:/Coq/Num/Nat/Axioms/lt_S_compat.con" as lemma.
-(* UNEXPORTED
-Hints Resolve lt_S_compat : nat.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/lt_eq_compat.con ***********)
inline procedural "cic:/Coq/Num/Nat/Axioms/lt_eq_compat.con" as lemma.
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/lt_add_compat_l.con ********)
+
inline procedural "cic:/Coq/Num/Nat/Axioms/lt_add_compat_l.con" as lemma.
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/lt_Sx_Sy_lt.con ************)
+
inline procedural "cic:/Coq/Num/Nat/Axioms/lt_Sx_Sy_lt.con" as lemma.
-(* UNEXPORTED
-Hints Immediate lt_Sx_Sy_lt : nat.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/lt_anti_refl.con ***********)
inline procedural "cic:/Coq/Num/Nat/Axioms/lt_anti_refl.con" as lemma.
include "Coq.ma".
-(*s Syntax for arithmetic *)
-
-(* NOTATION
-Infix 6 "<" lt.
-*)
-
-(* NOTATION
-Infix 6 "<=" le.
-*)
-
-(* NOTATION
-Infix 6 ">" gt.
-*)
-
-(* NOTATION
-Infix 6 ">=" ge.
-*)
-
-(*i Infix 7 "+" plus. i*)
-
-(* NOTATION
-Grammar constr lassoc_constr4 :=
- squash_sum
- [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
- case [$c2] of
- (SQUASH $T2) ->
- case [$c1] of
- (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
- | $_ -> [ (sumor $c1 $T2) ] (* c1+{T2} *)
- esac
- | $_ -> [ (add $c1 $c2) ] (* c1+c2 *)
- esac.
-*)
-
-(* NOTATION
-Syntax constr
- level 4:
- sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
-.
-*)
-
include "Coq.ma".
-(*s Definition of inequality *)
-
include "Num/Params.ma".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/NeqDef/neq.con ********************)
+
inline procedural "cic:/Coq/Num/Nat/NeqDef/neq.con" as definition.
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: NeqAxioms.v,v 1.2 2002/02/14 14:39:03 filliatr Exp $ i*)
-
-(*#* InEquality is introduced as an independant parameter, it could be
- instantiated with the negation of equality *)
-
include "Num/EqParams.ma".
include "Num/NeqParams.ma".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqAxioms/eq_not_neq.con **************)
+
inline procedural "cic:/Coq/Num/NeqAxioms/eq_not_neq.con".
-(* UNEXPORTED
-Hints Immediate eq_not_neq : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqAxioms/neq_sym.con *****************)
inline procedural "cic:/Coq/Num/NeqAxioms/neq_sym.con".
-(* UNEXPORTED
-Hints Resolve neq_sym : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqAxioms/neq_not_neq_trans.con *******)
inline procedural "cic:/Coq/Num/NeqAxioms/neq_not_neq_trans.con".
-(* UNEXPORTED
-Hints Resolve neq_not_neq_trans : num.
-*)
-
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: NeqDef.v,v 1.6 2003/10/22 10:35:03 barras Exp $ i*)
-
-(*#* DisEquality is defined as the negation of equality *)
-
include "Num/Params.ma".
include "Num/EqParams.ma".
include "Num/EqAxioms.ma".
-inline procedural "cic:/Coq/Num/NeqDef/neq.con" as definition.
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqDef/neq.con ************************)
-(* NOTATION
-Infix 6 "<>" neq V8only 70.
-*)
+inline procedural "cic:/Coq/Num/NeqDef/neq.con" as definition.
-(* Proofs of axioms *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqDef/eq_not_neq.con *****************)
inline procedural "cic:/Coq/Num/NeqDef/eq_not_neq.con" as lemma.
-(* UNEXPORTED
-Hints Immediate eq_not_neq : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqDef/neq_sym.con ********************)
inline procedural "cic:/Coq/Num/NeqDef/neq_sym.con" as lemma.
-(* UNEXPORTED
-Hints Resolve neq_sym : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqDef/neq_not_neq_trans.con **********)
inline procedural "cic:/Coq/Num/NeqDef/neq_not_neq_trans.con" as lemma.
-(* UNEXPORTED
-Hints Resolve neq_not_neq_trans : num.
-*)
-
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: NeqParams.v,v 1.4 2003/10/22 10:35:03 barras Exp $ i*)
-
-(*#* InEquality is introduced as an independant parameter, it could be
- instantiated with the negation of equality *)
-
include "Num/Params.ma".
-inline procedural "cic:/Coq/Num/NeqParams/neq.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqParams/neq.con *********************)
-(* NOTATION
-Infix 6 "<>" neq V8only 70.
-*)
+inline procedural "cic:/Coq/Num/NeqParams/neq.con".
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 *)
-
-(*#**********************************************************************)
-
include "Num/NeqParams.ma".
include "Num/NeqAxioms.ma".
include "Num/EqAxioms.ma".
-(*#* This file contains basic properties of disequality *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqProps/neq_antirefl.con *************)
inline procedural "cic:/Coq/Num/NeqProps/neq_antirefl.con" as lemma.
-(* UNEXPORTED
-Hints Resolve neq_antirefl : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqProps/eq_not_neq_y_x.con ***********)
inline procedural "cic:/Coq/Num/NeqProps/eq_not_neq_y_x.con" as lemma.
-(* UNEXPORTED
-Hints Immediate eq_not_neq_y_x : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqProps/neq_not_eq.con ***************)
inline procedural "cic:/Coq/Num/NeqProps/neq_not_eq.con" as lemma.
-(* UNEXPORTED
-Hints Immediate neq_not_eq : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqProps/neq_not_eq_y_x.con ***********)
inline procedural "cic:/Coq/Num/NeqProps/neq_not_eq_y_x.con" as lemma.
-(* UNEXPORTED
-Hints Immediate neq_not_eq_y_x : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqProps/not_neq_neq_trans.con ********)
inline procedural "cic:/Coq/Num/NeqProps/not_neq_neq_trans.con" as lemma.
-(* UNEXPORTED
-Hints Resolve not_neq_neq_trans : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqProps/neq_eq_compat.con ************)
inline procedural "cic:/Coq/Num/NeqProps/neq_eq_compat.con" as lemma.
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 *)
-
-(*#**********************************************************************)
-
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 *)
-
-(*#**********************************************************************)
-
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: Params.v,v 1.2 2002/02/14 14:39:04 filliatr Exp $ i*)
-
-(*#*
- Axiomatisation of a numerical set
-
- It will be instantiated by Z and R later on
- We choose to introduce many operation to allow flexibility in definition
- ([S] is primitive in the definition of [nat] while [add] and [one]
- are primitive in the definition
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/N.con **************************)
inline procedural "cic:/Coq/Num/Params/N.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/zero.con ***********************)
+
inline procedural "cic:/Coq/Num/Params/zero.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/one.con ************************)
+
inline procedural "cic:/Coq/Num/Params/one.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/add.con ************************)
+
inline procedural "cic:/Coq/Num/Params/add.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/S.con **************************)
+
inline procedural "cic:/Coq/Num/Params/S.con".
-(*#* Relations, equality is defined separately *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/lt.con *************************)
inline procedural "cic:/Coq/Num/Params/lt.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/le.con *************************)
+
inline procedural "cic:/Coq/Num/Params/le.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/gt.con *************************)
+
inline procedural "cic:/Coq/Num/Params/gt.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/Params/ge.con *************************)
+
inline procedural "cic:/Coq/Num/Params/ge.con".
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 *)
-
-(*#**********************************************************************)
-
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Alembert.v,v 1.14 2003/12/24 10:27:06 barras Exp $ i*)
+(*i $Id: Alembert.v,v 1.14.2.1 2004/07/16 19:31:10 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: AltSeries.v,v 1.12 2003/12/24 10:27:06 barras Exp $ i*)
+(*i $Id: AltSeries.v,v 1.12.2.1 2004/07/16 19:31:10 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: ArithProp.v,v 1.11 2003/12/24 10:27:06 barras Exp $ i*)
+(*i $Id: ArithProp.v,v 1.11.2.1 2004/07/16 19:31:10 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Binomial.v,v 1.9 2003/12/24 10:27:06 barras Exp $ i*)
+(*i $Id: Binomial.v,v 1.9.2.1 2004/07/16 19:31:10 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Cauchy_prod.v,v 1.10 2003/12/24 10:27:06 barras Exp $ i*)
+(*i $Id: Cauchy_prod.v,v 1.10.2.1 2004/07/16 19:31:10 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Cos_plus.v,v 1.11 2003/12/24 10:27:06 barras Exp $ i*)
+(*i $Id: Cos_plus.v,v 1.11.2.1 2004/07/16 19:31:10 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Cos_rel.v,v 1.12 2003/12/24 10:27:06 barras Exp $ i*)
+(*i $Id: Cos_rel.v,v 1.12.2.1 2004/07/16 19:31:10 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: DiscrR.v,v 1.21 2003/11/29 17:28:35 herbelin Exp $ i*)
+(*i $Id: DiscrR.v,v 1.21.2.1 2004/07/16 19:31:10 herbelin Exp $ i*)
include "Reals/RIneq.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Exp_prop.v,v 1.16 2003/12/24 10:27:06 barras Exp $ i*)
+(*i $Id: Exp_prop.v,v 1.16.2.1 2004/07/16 19:31:10 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Integration.v,v 1.1 2002/11/27 21:17:05 desmettr Exp $ i*)
+(*i $Id: Integration.v,v 1.1.6.1 2004/07/16 19:31:10 herbelin Exp $ i*)
include "Reals/NewtonInt.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: MVT.v,v 1.10 2003/12/24 10:27:06 barras Exp $ i*)
+(*i $Id: MVT.v,v 1.10.2.1 2004/07/16 19:31:10 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: NewtonInt.v,v 1.11 2003/12/24 10:27:06 barras Exp $ i*)
+(*i $Id: NewtonInt.v,v 1.11.2.1 2004/07/16 19:31:10 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: PSeries_reg.v,v 1.12 2003/12/24 10:27:06 barras Exp $ i*)
+(*i $Id: PSeries_reg.v,v 1.12.2.1 2004/07/16 19:31:10 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: PartSum.v,v 1.11 2003/12/24 10:27:06 barras Exp $ i*)
+(*i $Id: PartSum.v,v 1.11.2.1 2004/07/16 19:31:11 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: RIneq.v,v 1.23 2003/12/15 19:48:20 barras Exp $ i*)
+(*i $Id: RIneq.v,v 1.23.2.1 2004/07/16 19:31:11 herbelin Exp $ i*)
(*#**************************************************************************)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: RList.v,v 1.10 2003/12/15 19:48:20 barras Exp $ i*)
+(*i $Id: RList.v,v 1.10.2.1 2004/07/16 19:31:11 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: R_Ifp.v,v 1.14 2003/12/15 19:48:20 barras Exp $ i*)
+(*i $Id: R_Ifp.v,v 1.14.2.1 2004/07/16 19:31:12 herbelin Exp $ i*)
(*#*********************************************************)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: R_sqr.v,v 1.19 2003/11/29 17:28:35 herbelin Exp $ i*)
+(*i $Id: R_sqr.v,v 1.19.2.1 2004/07/16 19:31:12 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: R_sqrt.v,v 1.10 2003/11/29 17:28:35 herbelin Exp $ i*)
+(*i $Id: R_sqrt.v,v 1.10.2.1 2004/07/16 19:31:12 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Ranalysis.v,v 1.19 2003/11/29 17:28:37 herbelin Exp $ i*)
+(*i $Id: Ranalysis.v,v 1.19.2.1 2004/07/16 19:31:12 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Ranalysis1.v,v 1.21 2003/12/24 10:27:06 barras Exp $ i*)
+(*i $Id: Ranalysis1.v,v 1.21.2.1 2004/07/16 19:31:12 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Ranalysis2.v,v 1.11 2003/12/15 19:48:20 barras Exp $ i*)
+(*i $Id: Ranalysis2.v,v 1.11.2.1 2004/07/16 19:31:12 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Ranalysis3.v,v 1.10 2003/11/29 17:28:37 herbelin Exp $ i*)
+(*i $Id: Ranalysis3.v,v 1.10.2.1 2004/07/16 19:31:12 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Ranalysis4.v,v 1.19 2003/11/29 17:28:37 herbelin Exp $ i*)
+(*i $Id: Ranalysis4.v,v 1.19.2.1 2004/07/16 19:31:12 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Raxioms.v,v 1.20 2004/01/13 15:12:11 herbelin Exp $ i*)
+(*i $Id: Raxioms.v,v 1.20.2.1 2004/07/16 19:31:12 herbelin Exp $ i*)
(*#********************************************************)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Rbase.v,v 1.39 2003/11/29 17:28:37 herbelin Exp $ i*)
+(*i $Id: Rbase.v,v 1.39.2.1 2004/07/16 19:31:12 herbelin Exp $ i*)
include "Reals/Rdefinitions.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Rbasic_fun.v,v 1.22 2003/11/29 17:28:37 herbelin Exp $ i*)
+(*i $Id: Rbasic_fun.v,v 1.22.2.1 2004/07/16 19:31:12 herbelin Exp $ i*)
(*#********************************************************)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Rcomplete.v,v 1.10 2003/12/24 10:27:06 barras Exp $ i*)
+(*i $Id: Rcomplete.v,v 1.10.2.1 2004/07/16 19:31:12 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Rdefinitions.v,v 1.14 2003/11/29 17:28:37 herbelin Exp $ i*)
+(*i $Id: Rdefinitions.v,v 1.14.2.1 2004/07/16 19:31:12 herbelin Exp $ i*)
(*#********************************************************)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Rderiv.v,v 1.15 2003/11/29 17:28:37 herbelin Exp $ i*)
+(*i $Id: Rderiv.v,v 1.15.2.1 2004/07/16 19:31:12 herbelin Exp $ i*)
(*#********************************************************)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Reals.v,v 1.24 2003/11/29 17:28:37 herbelin Exp $ i*)
+(*i $Id: Reals.v,v 1.24.2.1 2004/07/16 19:31:12 herbelin Exp $ i*)
(* The library REALS is divided in 6 parts :
- Rbase: basic lemmas on R
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Rfunctions.v,v 1.31 2004/03/12 10:15:44 mohring Exp $ i*)
+(*i $Id: Rfunctions.v,v 1.31.2.1 2004/07/16 19:31:12 herbelin Exp $ i*)
(*i Some properties about pow and sum have been made with John Harrison i*)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Rgeom.v,v 1.13 2003/11/29 17:28:37 herbelin Exp $ i*)
+(*i $Id: Rgeom.v,v 1.13.2.1 2004/07/16 19:31:13 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: RiemannInt.v,v 1.18 2003/12/24 10:27:07 barras Exp $ i*)
+(*i $Id: RiemannInt.v,v 1.18.2.1 2004/07/16 19:31:13 herbelin Exp $ i*)
include "Reals/Rfunctions.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: RiemannInt_SF.v,v 1.16 2004/01/09 19:02:57 barras Exp $ i*)
+(*i $Id: RiemannInt_SF.v,v 1.16.2.1 2004/07/16 19:31:13 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Rlimit.v,v 1.23 2003/12/15 19:48:21 barras Exp $ i*)
+(*i $Id: Rlimit.v,v 1.23.2.1 2004/07/16 19:31:13 herbelin Exp $ i*)
(*#********************************************************)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Rpower.v,v 1.17 2003/12/24 10:27:07 barras Exp $ i*)
+(*i $Id: Rpower.v,v 1.17.2.1 2004/07/16 19:31:13 herbelin Exp $ i*)
(*i Due to L.Thery i*)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Rprod.v,v 1.10 2003/11/29 17:28:38 herbelin Exp $ i*)
+(*i $Id: Rprod.v,v 1.10.2.1 2004/07/16 19:31:13 herbelin Exp $ i*)
include "Arith/Compare.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Rseries.v,v 1.11 2003/12/15 19:48:21 barras Exp $ i*)
+(*i $Id: Rseries.v,v 1.11.2.1 2004/07/16 19:31:13 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Rsigma.v,v 1.12 2003/11/29 17:28:39 herbelin Exp $ i*)
+(*i $Id: Rsigma.v,v 1.12.2.1 2004/07/16 19:31:13 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Rsqrt_def.v,v 1.14 2003/12/24 10:27:07 barras Exp $ i*)
+(*i $Id: Rsqrt_def.v,v 1.14.2.1 2004/07/16 19:31:13 herbelin Exp $ i*)
include "Bool/Sumbool.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Rtopology.v,v 1.19 2003/12/24 10:27:07 barras Exp $ i*)
+(*i $Id: Rtopology.v,v 1.19.2.1 2004/07/16 19:31:13 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Rtrigo.v,v 1.40 2003/12/24 10:27:07 barras Exp $ i*)
+(*i $Id: Rtrigo.v,v 1.40.2.1 2004/07/16 19:31:14 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Rtrigo_alt.v,v 1.16 2003/12/24 10:27:08 barras Exp $ i*)
+(*i $Id: Rtrigo_alt.v,v 1.16.2.1 2004/07/16 19:31:14 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Rtrigo_calc.v,v 1.15 2003/11/29 17:28:39 herbelin Exp $ i*)
+(*i $Id: Rtrigo_calc.v,v 1.15.2.1 2004/07/16 19:31:14 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Rtrigo_def.v,v 1.17 2003/12/15 19:48:21 barras Exp $ i*)
+(*i $Id: Rtrigo_def.v,v 1.17.2.1 2004/07/16 19:31:14 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Rtrigo_fun.v,v 1.7 2003/11/29 17:28:39 herbelin Exp $ i*)
+(*i $Id: Rtrigo_fun.v,v 1.7.2.1 2004/07/16 19:31:15 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Rtrigo_reg.v,v 1.15 2003/12/24 10:27:08 barras Exp $ i*)
+(*i $Id: Rtrigo_reg.v,v 1.15.2.1 2004/07/16 19:31:15 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: SeqProp.v,v 1.13 2003/12/24 10:27:08 barras Exp $ i*)
+(*i $Id: SeqProp.v,v 1.13.2.1 2004/07/16 19:31:15 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: SeqSeries.v,v 1.14 2003/12/24 10:27:08 barras Exp $ i*)
+(*i $Id: SeqSeries.v,v 1.14.2.1 2004/07/16 19:31:15 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: SplitAbsolu.v,v 1.6 2003/11/29 17:28:40 herbelin Exp $ i*)
+(*i $Id: SplitAbsolu.v,v 1.6.2.1 2004/07/16 19:31:15 herbelin Exp $ i*)
include "Reals/Rbasic_fun.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: SplitRmult.v,v 1.7 2003/11/29 17:28:40 herbelin Exp $ i*)
+(*i $Id: SplitRmult.v,v 1.7.2.1 2004/07/16 19:31:15 herbelin Exp $ i*)
(*i Lemma mult_non_zero :(r1,r2:R)``r1<>0`` /\ ``r2<>0`` -> ``r1*r2<>0``. i*)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Sqrt_reg.v,v 1.9 2003/12/24 10:27:08 barras Exp $ i*)
+(*i $Id: Sqrt_reg.v,v 1.9.2.1 2004/07/16 19:31:15 herbelin Exp $ i*)
include "Reals/Rbase.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Newman.v,v 1.7 2003/11/29 17:28:41 herbelin Exp $ i*)
+(*i $Id: Newman.v,v 1.7.2.1 2004/07/16 19:31:16 herbelin Exp $ i*)
include "Relations/Rstar.ma".
cic:/Coq/Relations/Newman/Newman/R.var
*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Relations/Newman/Newman/Rstar.con *********)
+
inline procedural "cic:/Coq/Relations/Newman/Newman/Rstar.con" "Newman__" as definition.
+(* UNAVAILABLE OBJECT: cic:/Coq/Relations/Newman/Newman/Rstar_reflexive.con *)
+
inline procedural "cic:/Coq/Relations/Newman/Newman/Rstar_reflexive.con" "Newman__" as definition.
+(* UNAVAILABLE OBJECT: cic:/Coq/Relations/Newman/Newman/Rstar_transitive.con *)
+
inline procedural "cic:/Coq/Relations/Newman/Newman/Rstar_transitive.con" "Newman__" as definition.
+(* UNAVAILABLE OBJECT: cic:/Coq/Relations/Newman/Newman/Rstar_Rstar'.con **)
+
inline procedural "cic:/Coq/Relations/Newman/Newman/Rstar_Rstar'.con" "Newman__" as definition.
inline procedural "cic:/Coq/Relations/Newman/coherence.con" as definition.
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Operators_Properties.v,v 1.7 2003/11/29 17:28:41 herbelin Exp $ i*)
+(*i $Id: Operators_Properties.v,v 1.7.2.1 2004/07/16 19:31:16 herbelin Exp $ i*)
(*#***************************************************************************)
cic:/Coq/Relations/Operators_Properties/Properties/R.var
*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Relations/Operators_Properties/Properties/incl.con *)
+
inline procedural "cic:/Coq/Relations/Operators_Properties/Properties/incl.con" "Properties__" as definition.
(* UNEXPORTED
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Relation_Definitions.v,v 1.6 2003/12/15 19:48:22 barras Exp $ i*)
+(*i $Id: Relation_Definitions.v,v 1.6.2.1 2004/07/16 19:31:16 herbelin Exp $ i*)
(* UNEXPORTED
Section Relation_Definition
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * 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*)
+(*i $Id: Relation_Operators.v,v 1.8.2.1 2004/07/16 19:31:16 herbelin Exp $ i*)
(*#***************************************************************************)
cic:/Coq/Relations/Relation_Operators/Lexicographic_Exponentiation/leA.var
*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Relations/Relation_Operators/Lexicographic_Exponentiation/Nil.con *)
+
inline procedural "cic:/Coq/Relations/Relation_Operators/Lexicographic_Exponentiation/Nil.con" "Lexicographic_Exponentiation__" as definition.
+(* UNAVAILABLE OBJECT: cic:/Coq/Relations/Relation_Operators/Lexicographic_Exponentiation/List.con *)
+
inline procedural "cic:/Coq/Relations/Relation_Operators/Lexicographic_Exponentiation/List.con" "Lexicographic_Exponentiation__" as definition.
inline procedural "cic:/Coq/Relations/Relation_Operators/Ltl.ind".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Relations.v,v 1.6 2003/11/29 17:28:41 herbelin Exp $ i*)
+(*i $Id: Relations.v,v 1.6.2.1 2004/07/16 19:31:16 herbelin Exp $ i*)
include "Relations/Relation_Definitions.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Rstar.v,v 1.8 2003/12/15 19:48:22 barras Exp $ i*)
+(*i $Id: Rstar.v,v 1.8.2.1 2004/07/16 19:31:16 herbelin Exp $ i*)
(*#* Properties of a binary relation [R] on type [A] *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Setoid.v,v 1.5 2003/11/29 17:28:41 herbelin Exp $: i*)
+(*i $Id: Setoid.v,v 1.5.2.1 2004/07/16 19:31:17 herbelin Exp $: i*)
(* UNEXPORTED
Section Setoid
Hint Resolve (Seq_trans Prop iff Prop_S): setoid.
*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Setoids/Setoid/or_ext1.con ****************)
+
inline procedural "cic:/Coq/Setoids/Setoid/or_ext1.con" as theorem.
inline procedural "cic:/Coq/Setoids/Setoid/or_ext2.con" as theorem.
+(* UNAVAILABLE OBJECT: cic:/Coq/Setoids/Setoid/and_ext1.con ***************)
+
inline procedural "cic:/Coq/Setoids/Setoid/and_ext1.con" as theorem.
inline procedural "cic:/Coq/Setoids/Setoid/and_ext2.con" as theorem.
+(* UNAVAILABLE OBJECT: cic:/Coq/Setoids/Setoid/not_ext1.con ***************)
+
inline procedural "cic:/Coq/Setoids/Setoid/not_ext1.con" as theorem.
inline procedural "cic:/Coq/Setoids/Setoid/not_ext2.con" as theorem.
inline procedural "cic:/Coq/Setoids/Setoid/fleche.con" as definition.
+(* UNAVAILABLE OBJECT: cic:/Coq/Setoids/Setoid/fleche_ext1.con ************)
+
inline procedural "cic:/Coq/Setoids/Setoid/fleche_ext1.con" as theorem.
inline procedural "cic:/Coq/Setoids/Setoid/fleche_ext2.con" as theorem.
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
(*#***************************************************************************)
(*#***************************************************************************)
-(*i $Id: Classical_sets.v,v 1.4 2003/11/29 17:28:41 herbelin Exp $ i*)
+(*i $Id: Classical_sets.v,v 1.4.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
include "Sets/Ensembles.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
(*#***************************************************************************)
(*#***************************************************************************)
-(*i $Id: Constructive_sets.v,v 1.5 2003/11/29 17:28:41 herbelin Exp $ i*)
+(*i $Id: Constructive_sets.v,v 1.5.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
include "Sets/Ensembles.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
(*#***************************************************************************)
(*#***************************************************************************)
-(*i $Id: Cpo.v,v 1.5 2003/12/15 19:48:22 barras Exp $ i*)
+(*i $Id: Cpo.v,v 1.5.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
include "Sets/Ensembles.ma".
cic:/Coq/Sets/Cpo/Bounds/D.var
*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Sets/Cpo/Bounds/C.con *********************)
+
inline procedural "cic:/Coq/Sets/Cpo/Bounds/C.con" "Bounds__" as definition.
+(* UNAVAILABLE OBJECT: cic:/Coq/Sets/Cpo/Bounds/R.con *********************)
+
inline procedural "cic:/Coq/Sets/Cpo/Bounds/R.con" "Bounds__" as definition.
inline procedural "cic:/Coq/Sets/Cpo/Upper_Bound.ind".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
(*#***************************************************************************)
(*#***************************************************************************)
-(*i $Id: Ensembles.v,v 1.7 2003/11/29 17:28:41 herbelin Exp $ i*)
+(*i $Id: Ensembles.v,v 1.7.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
(* UNEXPORTED
Section Ensembles
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
(*#***************************************************************************)
(*#***************************************************************************)
-(*i $Id: Finite_sets.v,v 1.6 2003/12/15 19:48:22 barras Exp $ i*)
+(*i $Id: Finite_sets.v,v 1.6.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
include "Sets/Ensembles.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
(*#***************************************************************************)
(*#***************************************************************************)
-(*i $Id: Finite_sets_facts.v,v 1.7 2003/12/15 19:48:22 barras Exp $ i*)
+(*i $Id: Finite_sets_facts.v,v 1.7.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
include "Sets/Finite_sets.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
(*#***************************************************************************)
(*#***************************************************************************)
-(*i $Id: Image.v,v 1.6 2003/12/15 19:48:22 barras Exp $ i*)
+(*i $Id: Image.v,v 1.6.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
include "Sets/Finite_sets.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
(*#***************************************************************************)
(*#***************************************************************************)
-(*i $Id: Infinite_sets.v,v 1.5 2003/12/15 19:48:22 barras Exp $ i*)
+(*i $Id: Infinite_sets.v,v 1.5.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
include "Sets/Finite_sets.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
(*#***************************************************************************)
(*#***************************************************************************)
-(*i $Id: Integers.v,v 1.6 2003/12/15 19:48:22 barras Exp $ i*)
+(*i $Id: Integers.v,v 1.6.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
include "Sets/Finite_sets.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Multiset.v,v 1.9 2003/11/29 17:28:42 herbelin Exp $ i*)
+(*i $Id: Multiset.v,v 1.9.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
(* G. Huet 1-9-95 *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
(*#***************************************************************************)
(*#***************************************************************************)
-(*i $Id: Partial_Order.v,v 1.6 2003/12/15 19:48:22 barras Exp $ i*)
+(*i $Id: Partial_Order.v,v 1.6.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
include "Sets/Ensembles.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Permut.v,v 1.6 2003/11/29 17:28:42 herbelin Exp $ i*)
+(*i $Id: Permut.v,v 1.6.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
(* G. Huet 1-9-95 *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
(*#***************************************************************************)
(*#***************************************************************************)
-(*i $Id: Powerset.v,v 1.5 2003/11/29 17:28:43 herbelin Exp $ i*)
+(*i $Id: Powerset.v,v 1.5.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
include "Sets/Ensembles.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
(*#***************************************************************************)
(*#***************************************************************************)
-(*i $Id: Powerset_Classical_facts.v,v 1.5 2003/12/15 19:48:23 barras Exp $ i*)
+(*i $Id: Powerset_Classical_facts.v,v 1.5.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
include "Sets/Ensembles.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
(*#***************************************************************************)
(*#***************************************************************************)
-(*i $Id: Powerset_facts.v,v 1.8 2003/12/15 19:48:23 barras Exp $ i*)
+(*i $Id: Powerset_facts.v,v 1.8.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
include "Sets/Ensembles.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
(*#***************************************************************************)
(*#***************************************************************************)
-(*i $Id: Relations_1.v,v 1.4 2003/11/29 17:28:43 herbelin Exp $ i*)
+(*i $Id: Relations_1.v,v 1.4.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
(* UNEXPORTED
Section Relations_1
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
(*#***************************************************************************)
(*#***************************************************************************)
-(*i $Id: Relations_1_facts.v,v 1.7 2003/11/29 17:28:43 herbelin Exp $ i*)
+(*i $Id: Relations_1_facts.v,v 1.7.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
include "Sets/Relations_1.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
(*#***************************************************************************)
(*#***************************************************************************)
-(*i $Id: Relations_2.v,v 1.4 2003/11/29 17:28:43 herbelin Exp $ i*)
+(*i $Id: Relations_2.v,v 1.4.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
include "Sets/Relations_1.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
(*#***************************************************************************)
(*#***************************************************************************)
-(*i $Id: Relations_2_facts.v,v 1.6 2003/12/15 19:48:23 barras Exp $ i*)
+(*i $Id: Relations_2_facts.v,v 1.6.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
include "Sets/Relations_1.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
(*#***************************************************************************)
(*#***************************************************************************)
-(*i $Id: Relations_3.v,v 1.7 2003/12/15 19:48:23 barras Exp $ i*)
+(*i $Id: Relations_3.v,v 1.7.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
include "Sets/Relations_1.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
(*#***************************************************************************)
(*#***************************************************************************)
-(*i $Id: Relations_3_facts.v,v 1.6 2003/11/29 17:28:43 herbelin Exp $ i*)
+(*i $Id: Relations_3_facts.v,v 1.6.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
include "Sets/Relations_1.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Uniset.v,v 1.9 2003/11/29 17:28:43 herbelin Exp $ i*)
+(*i $Id: Uniset.v,v 1.9.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
(*#* Sets as characteristic functions *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Heap.v,v 1.3 2003/11/29 17:28:44 herbelin Exp $ i*)
+(*i $Id: Heap.v,v 1.3.2.1 2004/07/16 19:31:19 herbelin Exp $ i*)
(*#* A development of Treesort on Heap trees *)
cic:/Coq/Sorting/Heap/defs/eqA.var
*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Sorting/Heap/defs/gtA.con *****************)
+
inline procedural "cic:/Coq/Sorting/Heap/defs/gtA.con" "defs__" as definition.
(* UNEXPORTED
Hint Immediate eqA_dec leA_dec leA_antisym.
*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Sorting/Heap/defs/emptyBag.con ************)
+
inline procedural "cic:/Coq/Sorting/Heap/defs/emptyBag.con" "defs__" as definition.
+(* UNAVAILABLE OBJECT: cic:/Coq/Sorting/Heap/defs/singletonBag.con ********)
+
inline procedural "cic:/Coq/Sorting/Heap/defs/singletonBag.con" "defs__" as definition.
inline procedural "cic:/Coq/Sorting/Heap/Tree.ind".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Permutation.v,v 1.4 2003/11/29 17:28:44 herbelin Exp $ i*)
+(*i $Id: Permutation.v,v 1.4.2.1 2004/07/16 19:31:19 herbelin Exp $ i*)
include "Relations/Relations.ma".
cic:/Coq/Sorting/Permutation/defs/eqA.var
*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Sorting/Permutation/defs/gtA.con **********)
+
inline procedural "cic:/Coq/Sorting/Permutation/defs/gtA.con" "defs__" as definition.
(* UNEXPORTED
Hint Immediate eqA_dec leA_dec leA_antisym: default.
*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Sorting/Permutation/defs/emptyBag.con *****)
+
inline procedural "cic:/Coq/Sorting/Permutation/defs/emptyBag.con" "defs__" as definition.
+(* UNAVAILABLE OBJECT: cic:/Coq/Sorting/Permutation/defs/singletonBag.con *)
+
inline procedural "cic:/Coq/Sorting/Permutation/defs/singletonBag.con" "defs__" as definition.
(*#* contents of a list *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Sorting.v,v 1.4 2003/11/29 17:28:44 herbelin Exp $ i*)
+(*i $Id: Sorting.v,v 1.4.2.1 2004/07/16 19:31:19 herbelin Exp $ i*)
include "Lists/List.ma".
cic:/Coq/Sorting/Sorting/defs/eqA.var
*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Sorting/Sorting/defs/gtA.con **************)
+
inline procedural "cic:/Coq/Sorting/Sorting/defs/gtA.con" "defs__" as definition.
(* UNEXPORTED
Hint Immediate eqA_dec leA_dec leA_antisym.
*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Sorting/Sorting/defs/emptyBag.con *********)
+
inline procedural "cic:/Coq/Sorting/Sorting/defs/emptyBag.con" "defs__" as definition.
+(* UNAVAILABLE OBJECT: cic:/Coq/Sorting/Sorting/defs/singletonBag.con *****)
+
inline procedural "cic:/Coq/Sorting/Sorting/defs/singletonBag.con" "defs__" as definition.
(*#* [lelistA] *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Disjoint_Union.v,v 1.9 2003/11/29 17:28:44 herbelin Exp $ i*)
+(*i $Id: Disjoint_Union.v,v 1.9.2.1 2004/07/16 19:31:19 herbelin Exp $ i*)
(*#* Author: Cristina Cornes
From : Constructing Recursion Operators in Type Theory
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Inclusion.v,v 1.7 2003/11/29 17:28:44 herbelin Exp $ i*)
+(*i $Id: Inclusion.v,v 1.7.2.1 2004/07/16 19:31:19 herbelin Exp $ i*)
(*#* Author: Bruno Barras *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Inverse_Image.v,v 1.10 2003/12/15 19:48:23 barras Exp $ i*)
+(*i $Id: Inverse_Image.v,v 1.10.2.1 2004/07/16 19:31:19 herbelin Exp $ i*)
(*#* Author: Bruno Barras *)
cic:/Coq/Wellfounded/Inverse_Image/Inverse_Image/f.var
*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Wellfounded/Inverse_Image/Inverse_Image/Rof.con *)
+
inline procedural "cic:/Coq/Wellfounded/Inverse_Image/Inverse_Image/Rof.con" "Inverse_Image__" as definition.
inline procedural "cic:/Coq/Wellfounded/Inverse_Image/Acc_lemma.con" as remark.
cic:/Coq/Wellfounded/Inverse_Image/Inverse_Image/F.var
*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Wellfounded/Inverse_Image/Inverse_Image/RoF.con *)
+
inline procedural "cic:/Coq/Wellfounded/Inverse_Image/Inverse_Image/RoF.con" "Inverse_Image__" as definition.
inline procedural "cic:/Coq/Wellfounded/Inverse_Image/Acc_inverse_rel.con" as lemma.
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Lexicographic_Exponentiation.v,v 1.10 2003/12/15 19:48:23 barras Exp $ i*)
+(*i $Id: Lexicographic_Exponentiation.v,v 1.10.2.1 2004/07/16 19:31:19 herbelin Exp $ i*)
(*#* Author: Cristina Cornes
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Lexicographic_Product.v,v 1.12 2003/11/29 17:28:44 herbelin Exp $ i*)
+(*i $Id: Lexicographic_Product.v,v 1.12.2.1 2004/07/16 19:31:19 herbelin Exp $ i*)
(*#* Authors: Bruno Barras, Cristina Cornes *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Transitive_Closure.v,v 1.7 2003/11/29 17:28:44 herbelin Exp $ i*)
+(*i $Id: Transitive_Closure.v,v 1.7.2.1 2004/07/16 19:31:19 herbelin Exp $ i*)
(*#* Author: Bruno Barras *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Union.v,v 1.9 2003/12/15 19:48:23 barras Exp $ i*)
+(*i $Id: Union.v,v 1.9.2.1 2004/07/16 19:31:19 herbelin Exp $ i*)
(*#* Author: Bruno Barras *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Well_Ordering.v,v 1.7 2003/11/29 17:28:44 herbelin Exp $ i*)
+(*i $Id: Well_Ordering.v,v 1.7.2.1 2004/07/16 19:31:19 herbelin Exp $ i*)
(*#* Author: Cristina Cornes.
From: Constructing Recursion Operators in Type Theory
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Wellfounded.v,v 1.4 2003/11/29 17:28:44 herbelin Exp $ i*)
+(*i $Id: Wellfounded.v,v 1.4.2.1 2004/07/16 19:31:19 herbelin Exp $ i*)
include "Wellfounded/Disjoint_Union.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: BinInt.v,v 1.5 2003/11/29 17:28:45 herbelin Exp $ i*)
+(*i $Id: BinInt.v,v 1.5.2.1 2004/07/16 19:31:20 herbelin Exp $ i*)
(*#**********************************************************)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Wf_Z.v,v 1.20 2003/12/24 10:27:08 barras Exp $ i*)
+(*i $Id: Wf_Z.v,v 1.20.2.1 2004/07/16 19:31:20 herbelin Exp $ i*)
include "ZArith/BinInt.ma".
(*#* [natlike_rec2] is the same as [natlike_rec], but with a different proof, designed
to give a better extracted term. *)
+(* UNAVAILABLE OBJECT: cic:/Coq/ZArith/Wf_Z/Efficient_Rec/R.con ***********)
+
inline procedural "cic:/Coq/ZArith/Wf_Z/Efficient_Rec/R.con" "Efficient_Rec__" as definition.
+(* UNAVAILABLE OBJECT: cic:/Coq/ZArith/Wf_Z/Efficient_Rec/R_wf.con ********)
+
inline procedural "cic:/Coq/ZArith/Wf_Z/Efficient_Rec/R_wf.con" "Efficient_Rec__" as definition.
inline procedural "cic:/Coq/ZArith/Wf_Z/natlike_rec2.con" as lemma.
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: ZArith.v,v 1.5 2003/11/29 17:28:45 herbelin Exp $ i*)
+(*i $Id: ZArith.v,v 1.5.2.2 2004/08/03 17:56:30 herbelin Exp $ i*)
(*#* Library for manipulating integers based on binary encoding *)
include "ZArith/Zlogarithm.ma".
-include "ZArith/Zbool.ma".
-
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* $Id: ZArith_base.v,v 1.5 2003/11/29 17:28:45 herbelin Exp $ *)
+(* $Id: ZArith_base.v,v 1.5.2.1 2004/07/16 19:31:20 herbelin Exp $ *)
(*#* Library for manipulating integers based on binary encoding.
These are the basic modules, required by [Omega] and [Ring] for instance.
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: ZArith_dec.v,v 1.11 2003/11/29 17:28:45 herbelin Exp $ i*)
+(*i $Id: ZArith_dec.v,v 1.11.2.1 2004/07/16 19:31:20 herbelin Exp $ i*)
include "Bool/Sumbool.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Zabs.v,v 1.4 2003/11/29 17:28:45 herbelin Exp $ i*)
+(*i $Id: Zabs.v,v 1.4.2.1 2004/07/16 19:31:21 herbelin Exp $ i*)
(*#* Binary Integers (Pierre Cr\233\gut (CNET, Lannion, France) *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Zbinary.v,v 1.6 2004/02/10 15:38:01 marche Exp $ i*)
+(*i $Id: Zbinary.v,v 1.6.2.1 2004/07/16 19:31:21 herbelin Exp $ i*)
(*#* Bit vectors interpreted as integers.
Contribution by Jean Duprat (ENS Lyon). *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* $Id: Zbool.v,v 1.4 2003/11/29 17:28:45 herbelin Exp $ *)
+(* $Id: Zbool.v,v 1.4.2.1 2004/07/16 19:31:21 herbelin Exp $ *)
include "ZArith/BinInt.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
(*i $$ i*)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Zcomplements.v,v 1.26 2003/11/29 17:28:45 herbelin Exp $ i*)
+(*i $Id: Zcomplements.v,v 1.26.2.1 2004/07/16 19:31:21 herbelin Exp $ i*)
include "ZArith/ZArith_base.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Zdiv.v,v 1.21 2003/11/29 17:28:45 herbelin Exp $ i*)
+(*i $Id: Zdiv.v,v 1.21.2.1 2004/07/16 19:31:21 herbelin Exp $ i*)
(* Contribution by Claude March\233\ and Xavier Urbain *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Zeven.v,v 1.3 2003/11/29 17:28:45 herbelin Exp $ i*)
+(*i $Id: Zeven.v,v 1.3.2.1 2004/07/16 19:31:21 herbelin Exp $ i*)
include "ZArith/BinInt.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Zhints.v,v 1.8 2003/11/29 17:28:45 herbelin Exp $ i*)
+(*i $Id: Zhints.v,v 1.8.2.1 2004/07/16 19:31:21 herbelin Exp $ i*)
(*#* This file centralizes the lemmas about [Z], classifying them
according to the way they can be used in automatic search *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Zlogarithm.v,v 1.14 2003/12/15 19:48:23 barras Exp $ i*)
+(*i $Id: Zlogarithm.v,v 1.14.2.1 2004/07/16 19:31:21 herbelin Exp $ i*)
(*#*********************************************************************)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Zmin.v,v 1.3 2003/11/29 17:28:45 herbelin Exp $ i*)
+(*i $Id: Zmin.v,v 1.3.2.1 2004/07/16 19:31:21 herbelin Exp $ i*)
(*#* Binary Integers (Pierre Cr\233\gut (CNET, Lannion, France) *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Zmisc.v,v 1.20 2003/11/29 17:28:45 herbelin Exp $ i*)
+(*i $Id: Zmisc.v,v 1.20.2.1 2004/07/16 19:31:22 herbelin Exp $ i*)
include "ZArith/BinInt.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Znat.v,v 1.3 2003/12/15 19:48:23 barras Exp $ i*)
+(*i $Id: Znat.v,v 1.3.2.1 2004/07/16 19:31:22 herbelin Exp $ i*)
(*#* Binary Integers (Pierre Cr\233\gut, CNET, Lannion, France) *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Znumtheory.v,v 1.5 2003/12/16 15:03:50 herbelin Exp $ i*)
+(*i $Id: Znumtheory.v,v 1.5.2.1 2004/07/16 19:31:22 herbelin Exp $ i*)
include "ZArith/ZArith_base.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Zorder.v,v 1.6 2003/11/29 17:28:45 herbelin Exp $ i*)
+(*i $Id: Zorder.v,v 1.6.2.1 2004/07/16 19:31:22 herbelin Exp $ i*)
(*#* Binary Integers (Pierre Cr\233\gut (CNET, Lannion, France) *)
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: Zpower.v,v 1.11 2003/11/29 17:28:46 herbelin Exp $ i*)
+(*i $Id: Zpower.v,v 1.11.2.1 2004/07/16 19:31:22 herbelin Exp $ i*)
include "ZArith/ZArith_base.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* $Id: Zsqrt.v,v 1.11 2003/12/15 19:48:23 barras Exp $ *)
+(* $Id: Zsqrt.v,v 1.11.2.1 2004/07/16 19:31:22 herbelin Exp $ *)
include "ZArith/ZArith_base.ma".
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* $Id: Zwf.v,v 1.7 2003/11/29 17:28:46 herbelin Exp $ *)
+(* $Id: Zwf.v,v 1.7.2.1 2004/07/16 19:31:22 herbelin Exp $ *)
include "ZArith/ZArith_base.ma".
(*#* The proof of well-foundness is classic: we do the proof by induction
on a measure in nat, which is here [|x-c|] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/ZArith/Zwf/wf_proof/f.con *****************)
+
inline procedural "cic:/Coq/ZArith/Zwf/wf_proof/f.con" "wf_proof__" as definition.
inline procedural "cic:/Coq/ZArith/Zwf/Zwf_well_founded.con" as lemma.
(*#* The proof of well-foundness is classic: we do the proof by induction
on a measure in nat, which is here [|c-x|] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/ZArith/Zwf/wf_proof_up/f.con **************)
+
inline procedural "cic:/Coq/ZArith/Zwf/wf_proof_up/f.con" "wf_proof_up__" as definition.
inline procedural "cic:/Coq/ZArith/Zwf/Zwf_up_well_founded.con" as lemma.
include "Coq.ma".
-(*#**********************************************************************)
+(*#***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ *************************************************************)
+(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
+(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(*#**********************************************************************)
+(*#***********************************************************************)
-(*i $Id: auxiliary.v,v 1.12 2003/11/29 17:28:46 herbelin Exp $ i*)
+(*i $Id: auxiliary.v,v 1.12.2.1 2004/07/16 19:31:22 herbelin Exp $ i*)
(*#* Binary Integers (Pierre Cr\233\gut, CNET, Lannion, France) *)
endif
mma: $(DEVEL).conf.xml clean.ma
- $(H)$(TRANSCRIPT) -C $(BIN) $(DEVEL)
+ $(H)$(TRANSCRIPT) -g -C $(BIN) $(DEVEL)
projects / helm.git / commitdiff