module PER = ProofEngineReduction
module Ut = CicUtil
-(* raw cic prettyprinter ****************************************************)
-
-let xiter out so ss sc map l =
- let rec aux = function
- | hd :: tl when tl <> [] -> map hd; out ss; aux tl
- | hd :: tl -> map hd; aux tl
- | [] -> ()
- in
- out so; aux l; out sc
-
-let abst s w = Some (s, C.Decl w)
-
-let abbr s v w = Some (s, C.Def (v, w))
-
-let pp_sort out = function
- | C.Type _ -> out "*Type"
- | C.Prop -> out "*Prop"
- | C.CProp _ -> out "*CProp"
- | C.Set -> out "*Set"
-
-let pp_name out = function
- | C.Name s -> out s
- | C.Anonymous -> out "_"
-
-let pp_rel out c i =
- try match List.nth c (pred i) with
- | None -> out (Printf.sprintf "%u[?]" i)
- | Some (s, _) -> out (Printf.sprintf "%u[" i); pp_name out s; out "]"
- with Failure "nth" -> out (Printf.sprintf "%u[%u]" i (List.length c - i))
-
-let pp_implict out = function
- | None -> out "?"
- | Some `Closed -> out "?[Closed]"
- | Some `Type -> out "?[Type]"
- | Some `Hole -> out "?[Hole]"
-
-let pp_uri out a =
- out (Printf.sprintf "%s<%s>" (UM.name_of_uri a) (UM.string_of_uri a))
-
-let rec pp_term out e c = function
- | C.Sort h -> pp_sort out h
- | C.Rel i -> pp_rel out c i
- | C.Implicit x -> pp_implict out x
- | C.Meta (i, iss) ->
- let map = function None -> out "_" | Some v -> pp_term out e c v in
- out (Printf.sprintf "?%u" i); xiter out "[" "; " "]" map iss
- | C.Var (a, xss) ->
- pp_uri out a; pp_xss out e c xss
- | C.Const (a, xss) ->
- pp_uri out a; pp_xss out e c xss
- | C.MutInd (a, m, xss) ->
- pp_uri out a; out (Printf.sprintf "/%u" m);
- pp_xss out e c xss
- | C.MutConstruct (a, m, n, xss) ->
- pp_uri out a; out (Printf.sprintf "/%u/%u" m n);
- pp_xss out e c xss
- | C.Cast (v, w) ->
- out "type "; pp_term out e c w; out " contains "; pp_term out e c v
- | C.Appl vs ->
- xiter out "(" " @ " ")" (pp_term out e c) vs
- | C.MutCase (a, m, w, v, vs) ->
- out "match "; pp_term out e c v;
- out " of "; pp_uri out a; out (Printf.sprintf "/%u" m);
- out " to "; pp_term out e c w;
- xiter out " cases " " | " "" (pp_term out e c) vs
- | C.Prod (s, w, t) ->
- out "forall "; pp_name out s; out " of "; pp_term out e c w;
- out " in "; pp_term out e (abst s w :: c) t
- | C.Lambda (s, w, t) ->
- out "fun "; pp_name out s; out " of "; pp_term out e c w;
- out " in "; pp_term out e (abst s w :: c) t
- | C.LetIn (s, v, w, t) ->
- out "let "; pp_name out s;
- out " def "; pp_term out e c v; out " of "; pp_term out e c w;
- out " in "; pp_term out e (abbr s v w :: c) t
- | C.Fix (i, fs) ->
- let map c (s, _, w, v) = abbr (C.Name s) v w :: c in
- let c' = List.fold_left map c fs in
- let map (s, i, w, v) =
- out (Printf.sprintf "%s[%u] def " s i); pp_term out e c' v;
- out " of "; pp_term out e c w;
- in
- xiter out "let rec " " and " " in " map fs; pp_rel out c' (succ i)
- | C.CoFix (i, fs) ->
- let map c (s, w, v) = abbr (C.Name s) v w :: c in
- let c' = List.fold_left map c fs in
- let map (s, w, v) =
- out s; pp_term out e c' v;
- out " of "; pp_term out e c w;
- in
- xiter out "let corec " " and " " in " map fs; pp_rel out c' (succ i)
-
-and pp_xss out e c xss =
- let map (a, v) = pp_uri out a; out " <- "; pp_term out e c v in
- xiter out "[" "; " "]" map xss
-
(* fresh name generator *****************************************************)
let split name =
let fst3 (x, _, _) = x
let refine c t =
- try let t, _, _, _ = Rf.type_of_aux' [] c t Un.default_ugraph in t
- with e ->
- Printf.eprintf "REFINE EROR: %s\n" (Printexc.to_string e);
+ let error e =
Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c);
Printf.eprintf "Ref: term : %s\n" (Pp.ppterm t);
raise e
+ in
+ try let t, _, _, _ = Rf.type_of_aux' [] c t Un.default_ugraph in t with
+ | Rf.RefineFailure s as e ->
+ Printf.eprintf "REFINE FAILURE: %s\n" (Lazy.force s);
+ error e
+ | e ->
+ Printf.eprintf "REFINE ERROR: %s\n" (Printexc.to_string e);
+ error e
let get_type msg c t =
let log s =
prerr_endline ("TC: " ^ s);
prerr_endline ("TC: context: " ^ Pp.ppcontext c);
- prerr_string "TC: term : "; pp_term prerr_string [] c t;
+ prerr_string "TC: term : "; Ut.pp_term prerr_string [] c t;
prerr_newline (); prerr_endline ("TC: location: " ^ msg)
in
try let ty, _ = TC.type_of_aux' [] c t Un.default_ugraph in ty with
* http://cs.unibo.it/helm/.
*)
-val pp_term:
- (string -> unit) -> Cic.metasenv -> Cic.context -> Cic.term -> unit
val mk_fresh_name:
Cic.context -> Cic.name -> Cic.name
val list_fold_right_cps:
module TC = CicTypeChecker
module Un = CicUniv
module L = Librarian
+module Ut = CicUtil
module H = ProceduralHelpers
module Cl = ProceduralClassify
let g st bo =
if !debug then begin
Printf.eprintf "Optimized : %s\n" (Pp.ppterm bo);
- prerr_string "H.pp_term : ";
- H.pp_term prerr_string [] c bo; prerr_newline ()
+ prerr_string "Ut.pp_term : ";
+ Ut.pp_term prerr_string [] c bo; prerr_newline ()
end;
(* let _ = H.get_type "opt" [] (C.Cast (bo, ty)) in *)
let nodes = Printf.sprintf "Optimized nodes: %u" (I.count_nodes 0 bo) in
module X = HExtlib
module T = Types
module G = Grafite
-module HP = Http_getter
+module HG = Http_getter
module O = Options
output_path: string;
input_type: string;
output_type: T.output_kind;
+ includes: (string * string) list;
coercions: (string * string) list;
files: string list;
requires: (string * string) list;
let matita_registry = Filename.concat !O.cwd "matita" in
load_registry default_registry;
load_registry matita_registry;
- HP.init ()
+ HG.init ()
let make registry =
let id x = x in
- let get_coercions = R.get_list (R.pair id id) in
+ let get_pairs = R.get_list (R.pair id id) in
let get_output_type key =
match R.get_string key with
| "procedural" -> T.Procedural
output_path = R.get_string "package.output_path";
input_type = R.get_string "package.input_type";
output_type = get_output_type "package.output_type";
- coercions = get_coercions "package.coercion";
+ includes = get_pairs "package.include";
+ coercions = get_pairs "package.coercion";
files = [];
requires = [];
scripts = Array.make default_scripts default_script
path, Some item
| item -> path, Some item
in
+ let set_includes st name =
+ try require st name (List.assoc name st.includes)
+ with Not_found -> ()
+ in
Printf.eprintf "processing file name: %s ...\n" name; flush stderr;
let file = Filename.concat st.input_path (name ^ st.input_type) in
let ich = open_in file in
let comment = T.Line (Printf.sprintf "From %s" name) in
if global_items <> [] then
set_items st st.input_package (comment :: global_items);
- init name; require st name st.input_package;
+ init name; require st name st.input_package; set_includes st name;
set_items st name local_items; commit st name
with e ->
prerr_endline (Printexc.to_string e); close_in ich
(* $Id$ *)
-module C = Cic
+module C = Cic
+module UM = UriManager
exception Meta_not_found of int
exception Subst_not_found of int
List.fold_left map g
in
sober_term c (fun b -> b) t true
+
+(* raw cic prettyprinter ****************************************************)
+
+let xiter out so ss sc map l =
+ let rec aux = function
+ | hd :: tl when tl <> [] -> map hd; out ss; aux tl
+ | hd :: tl -> map hd; aux tl
+ | [] -> ()
+ in
+ out so; aux l; out sc
+
+let abst s w = Some (s, C.Decl w)
+
+let abbr s v w = Some (s, C.Def (v, w))
+
+let pp_sort out = function
+ | C.Type _ -> out "*Type"
+ | C.Prop -> out "*Prop"
+ | C.CProp _ -> out "*CProp"
+ | C.Set -> out "*Set"
+
+let pp_name out = function
+ | C.Name s -> out s
+ | C.Anonymous -> out "_"
+
+let pp_rel out c i =
+ try match List.nth c (pred i) with
+ | None -> out (Printf.sprintf "%u[?]" i)
+ | Some (s, _) -> out (Printf.sprintf "%u[" i); pp_name out s; out "]"
+ with Failure "nth" -> out (Printf.sprintf "%u[%u]" i (List.length c - i))
+
+let pp_implict out = function
+ | None -> out "?"
+ | Some `Closed -> out "?[Closed]"
+ | Some `Type -> out "?[Type]"
+ | Some `Hole -> out "?[Hole]"
+
+let pp_uri out a =
+ out (Printf.sprintf "%s<%s>" (UM.name_of_uri a) (UM.string_of_uri a))
+
+let rec pp_term out e c = function
+ | C.Sort h -> pp_sort out h
+ | C.Rel i -> pp_rel out c i
+ | C.Implicit x -> pp_implict out x
+ | C.Meta (i, iss) ->
+ let map = function None -> out "_" | Some v -> pp_term out e c v in
+ out (Printf.sprintf "?%u" i); xiter out "[" "; " "]" map iss
+ | C.Var (a, xss) ->
+ pp_uri out a; pp_xss out e c xss
+ | C.Const (a, xss) ->
+ pp_uri out a; pp_xss out e c xss
+ | C.MutInd (a, m, xss) ->
+ pp_uri out a; out (Printf.sprintf "/%u" m);
+ pp_xss out e c xss
+ | C.MutConstruct (a, m, n, xss) ->
+ pp_uri out a; out (Printf.sprintf "/%u/%u" m n);
+ pp_xss out e c xss
+ | C.Cast (v, w) ->
+ out "type "; pp_term out e c w; out " contains "; pp_term out e c v
+ | C.Appl vs ->
+ xiter out "(" " @ " ")" (pp_term out e c) vs
+ | C.MutCase (a, m, w, v, vs) ->
+ out "match "; pp_term out e c v;
+ out " of "; pp_uri out a; out (Printf.sprintf "/%u" m);
+ out " to "; pp_term out e c w;
+ xiter out " cases " " | " "" (pp_term out e c) vs
+ | C.Prod (s, w, t) ->
+ out "forall "; pp_name out s; out " of "; pp_term out e c w;
+ out " in "; pp_term out e (abst s w :: c) t
+ | C.Lambda (s, w, t) ->
+ out "fun "; pp_name out s; out " of "; pp_term out e c w;
+ out " in "; pp_term out e (abst s w :: c) t
+ | C.LetIn (s, v, w, t) ->
+ out "let "; pp_name out s;
+ out " def "; pp_term out e c v; out " of "; pp_term out e c w;
+ out " in "; pp_term out e (abbr s v w :: c) t
+ | C.Fix (i, fs) ->
+ let map c (s, _, w, v) = abbr (C.Name s) v w :: c in
+ let c' = List.fold_left map c fs in
+ let map (s, i, w, v) =
+ out (Printf.sprintf "%s[%u] def " s i); pp_term out e c' v;
+ out " of "; pp_term out e c w;
+ in
+ xiter out "let rec " " and " " in " map fs; pp_rel out c' (succ i)
+ | C.CoFix (i, fs) ->
+ let map c (s, w, v) = abbr (C.Name s) v w :: c in
+ let c' = List.fold_left map c fs in
+ let map (s, w, v) =
+ out s; pp_term out e c' v;
+ out " of "; pp_term out e c w;
+ in
+ xiter out "let corec " " and " " in " map fs; pp_rel out c' (succ i)
+
+and pp_xss out e c xss =
+ let map (a, v) = pp_uri out a; out " <- "; pp_term out e c v in
+ xiter out "[" "; " "]" map xss
+
+and pp_attrs out attrs =
+ let map = function
+ | _ -> ()
+ in
+ xiter out "[" "; " "] " map attrs
+
+let pp_pars out pars =
+ xiter out " (" ", " ")\n" (pp_uri out) pars
+
+let pp_obj out = function
+ | C.Constant (s, None, u, pars, attrs) ->
+ out "fun "; pp_attrs out attrs; out s; pp_pars out pars;
+ out " of "; pp_term out [] [] u
+ | C.Constant (s, Some t, u, pars, attrs) ->
+ out "let "; pp_attrs out attrs; out s; pp_pars out pars;
+ out " def "; pp_term out [] [] t; out " of "; pp_term out [] [] u
+ | C.Variable (s, None, u, pars, attrs) ->
+ out "Local declaration"
+ | C.Variable (s, Some t, u, pars, attrs) ->
+ out "Local definition"
+ | C.CurrentProof (s, e, t, u, pars, attrs) ->
+ out "Current Proof"
+ | C.InductiveDefinition (us, pars, lpno, attrs) ->
+ out "Inductive Definition"
+
* detects applications without arguments
*)
val is_sober: Cic.context -> Cic.term -> bool
+
+val pp_term:
+ (string -> unit) -> Cic.metasenv -> Cic.context -> Cic.term -> unit
+val pp_obj:
+ (string -> unit) -> Cic.obj -> unit
module C = Cic
module Un = CicUniv
module E = CicEnvironment
+module Ut = CicUtil
+module TC = CicTypeChecker
let hashtbl_size = 11
let debug = ref false
+let out = prerr_string
+
(* helper functions *********************************************************)
+let typecheck t =
+ if !debug then begin
+ let _ = TC.type_of_aux' [] [] t Un.default_ugraph in
+ out "Typecheck : OK\n"
+ end
+
let list_pos found l =
let rec aux n = function
| [] -> raise Not_found
if vs' == vs then t else C.Appl (flatten vs')
| C.Cast (v, w) ->
let v', w' = discharge_term st v, discharge_term st w in
- if v' = v && w' = w then t else
+ if v' == v && w' == w then t else
C.Cast (sh v v', sh w w')
| C.MutCase (u, m, w, v, vs) ->
+ let args = get_args st u in
+ let u' = if args = [] then u else st.du u in
let w', v', vs' =
discharge_term st w, discharge_term st v,
list_map_sh (discharge_term st) vs
in
- if w' = w && v' = v && vs' == vs then t else
- C.MutCase (st.du u, m, sh w w', sh v v', sh vs vs')
+ if UM.eq u u' && w' == w && v' == v && vs' == vs then t else
+ C.MutCase (u', m, sh w w', sh v v', sh vs vs')
| C.Prod (b, w, v) ->
let w', v' = discharge_term st w, discharge_term (add st 1) v in
- if w' = w && v' = v then t else
+ if w' == w && v' == v then t else
C.Prod (b, sh w w', sh v v')
| C.Lambda (b, w, v) ->
let w', v' = discharge_term st w, discharge_term (add st 1) v in
- if w' = w && v' = v then t else
+ if w' == w && v' == v then t else
C.Lambda (b, sh w w', sh v v')
| C.LetIn (b, y, w, v) ->
let y', w', v' =
discharge_term st y, discharge_term st w, discharge_term (add st 1) v
in
- if y' = y && w' = w && v' == v then t else
+ if y' == y && w' == w && v' == v then t else
C.LetIn (b, sh y y', sh w w', sh v v')
| C.CoFix (i, s) ->
let no = List.length s in
and discharge_cofun st no f =
let b, w, v = f in
let w', v' = discharge_term st w, discharge_term (add st no) v in
- if w' = w && v' = v then f else
+ if w' == w && v' == v then f else
b, sh w w', sh v v'
and discharge_fun st no f =
let b, i, w, v = f in
let w', v' = discharge_term st w, discharge_term (add st no) v in
- if w' = w && v' = v then f else
+ if w' == w && v' == v then f else
b, i, sh w w', sh v v'
let close is_type st t =
| C.Variable (b, None, w, vars, attrs) ->
let st = init_status dn du ls vars in
let w' = discharge_term st w in
- if w' = w && vars = [] then obj else
+ if w' == w && vars = [] then obj else
let w'' = sh w w' in
+ let _ = typecheck w'' in
C.Variable (dn b, None, w'', [], attrs)
| C.Variable (b, Some v, w, vars, attrs) ->
let st = init_status dn du ls vars in
let w', v' = discharge_term st w, discharge_term st v in
- if w' = w && v' = v && vars = [] then obj else
+ if w' == w && v' == v && vars = [] then obj else
let w'', v'' = sh w w', sh v v' in
+ let _ = typecheck (C.Cast (v'', w'')) in
C.Variable (dn b, Some v'', w'', [], attrs)
| C.Constant (b, None, w, vars, attrs) ->
let st = init_status dn du ls vars in
let w' = discharge_term st w in
- if w' = w && vars = [] then obj else
+ if w' == w && vars = [] then obj else
let w'' = close true st (sh w w') in
+ let _ = typecheck w'' in
C.Constant (dn b, None, w'', [], attrs)
| C.Constant (b, Some v, w, vars, attrs) ->
let st = init_status dn du ls vars in
let w', v' = discharge_term st w, discharge_term st v in
- if w' = w && v' = v && vars = [] then obj else
+ if w' == w && v' == v && vars = [] then obj else
let w'', v'' = close true st (sh w w'), close false st (sh v v') in
+ let _ = typecheck (C.Cast (v'', w'')) in
C.Constant (dn b, Some v'', w'', [], attrs)
| C.InductiveDefinition (types, vars, lpsno, attrs) ->
let st = init_status dn du ls vars in
HLog.warn not_implemented; obj
and discharge_uri dn du uri =
+ let prerr msg obj =
+ if !debug then begin
+ out msg; Ut.pp_obj out obj; out "\n"
+ end
+ in
let obj, _ = E.get_obj Un.default_ugraph uri in
- if !debug then prerr_endline ("Plain : " ^ CicPp.ppobj obj);
+ prerr "Plain : " obj;
let obj' = discharge_object dn du obj in
- if !debug then prerr_endline ("Discharged: " ^ CicPp.ppobj obj');
+ prerr "Discharged: " obj';
obj', obj' == obj
and discharge_vars dn du vars =
include "Coq.ma".
+include "Init/Prelude.ma".
+
(*#***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
include "Coq.ma".
+include "Init/Prelude.ma".
+
(*#***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
include "Coq.ma".
+include "Init/Prelude.ma".
+
(*#***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
include "Coq.ma".
+include "Init/Prelude.ma".
+
(*#***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
include "Coq.ma".
+include "Init/Prelude.ma".
+
(*#***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
include "Coq.ma".
+include "Init/Prelude.ma".
+
(*#***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
<key name="output_path">contribs/procedural/Coq</key>
<key name="input_type">.v</key>
<key name="output_type">procedural</key>
+
+ <key name="include">Arith/EqNat Init/Prelude</key>
+ <key name="include">Arith/Even Init/Prelude</key>
+ <key name="include">Arith/Le Init/Prelude</key>
+ <key name="include">Bool/Bool Init/Prelude</key>
+ <key name="include">Bool/DecBool Init/Prelude</key>
+ <key name="include">Bool/Sumbool Init/Prelude</key>
+ <key name="include">Lists/Streams Init/Prelude</key>
+ <key name="include">Logic/Berardi Init/Prelude</key>
+ <key name="include">Logic/ChoiceFacts Init/Prelude</key>
+ <key name="include">Logic/ClassicalFacts Init/Prelude</key>
+ <key name="include">Logic/Decidable Init/Prelude</key>
+ <key name="include">Logic/Eqdep Init/Prelude</key>
+ <key name="include">Logic/Eqdep_dec Init/Prelude</key>
+ <key name="include">Logic/Hurkens Init/Prelude</key>
+ <key name="include">Logic/RelationalChoice Init/Prelude</key>
+ <key name="include">NArith/BinPos Init/Prelude</key>
+ <key name="include">Relations/Relation_Definitions Init/Prelude</key>
+ <key name="include">Relations/Rstar Init/Prelude</key>
+ <key name="include">Setoids/Setoid Init/Prelude</key>
+ <key name="include">Sets/Ensembles Init/Prelude</key>
+ <key name="include">Sets/Permut Init/Prelude</key>
+ <key name="include">Sets/Relations_1 Init/Prelude</key>
+ <key name="include">Wellfounded/Inverse_Image Init/Prelude</key>
<!--
<key name="coercion">Z_of_nat cic:/Coq/ZArith/BinInt/Z_of_nat.con</key>
<key name="coercion">Zpos cic:/Coq/ZArith/BinInt/Z.ind#xpointer(1/1/2)</key>
include "Coq.ma".
+include "Init/Prelude.ma".
+
(*#***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
include "Coq.ma".
+include "Init/Prelude.ma".
+
(*#***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
include "Coq.ma".
+include "Init/Prelude.ma".
+
(*#***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
include "Coq.ma".
+include "Init/Prelude.ma".
+
(*#***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
include "Coq.ma".
+include "Init/Prelude.ma".
+
(*#***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
include "Coq.ma".
+include "Init/Prelude.ma".
+
(*#***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
include "Coq.ma".
+include "Init/Prelude.ma".
+
(*#***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
include "Coq.ma".
+include "Init/Prelude.ma".
+
(*#***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
include "Coq.ma".
+include "Init/Prelude.ma".
+
(*#***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
include "Coq.ma".
+include "Init/Prelude.ma".
+
(*#***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
include "Coq.ma".
+include "Init/Prelude.ma".
+
(*#***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
include "Coq.ma".
+include "Init/Prelude.ma".
+
(*#***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
include "Coq.ma".
+include "Init/Prelude.ma".
+
(*#***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
include "Coq.ma".
+include "Init/Prelude.ma".
+
(*#***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
include "Coq.ma".
+include "Init/Prelude.ma".
+
(*#***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
include "Coq.ma".
+include "Init/Prelude.ma".
+
(*#***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
include "Coq.ma".
+include "Init/Prelude.ma".
+
(*#***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
Reals/Rseries.mma Arith/Compare.ma Coq.ma Logic/Classical.ma Reals/Rbase.ma Reals/Rfunctions.ma
Lists/ListSet.mma Coq.ma Lists/List.ma
Arith/Le.ma Arith/Le.mma
-Setoids/Setoid.mma Coq.ma
+Setoids/Setoid.mma Coq.ma Init/Prelude.ma
Logic/ProofIrrelevance.ma Logic/ProofIrrelevance.mma
ZArith/Zeven.mma Coq.ma ZArith/BinInt.ma
ZArith/Zcompare.mma Arith/Gt.ma Arith/Lt.ma Arith/Mult.ma Arith/Plus.ma Coq.ma NArith/BinPos.ma ZArith/BinInt.ma
Coq.ma preamble.ma
ZArith/Znat.mma Arith/Arith.ma Arith/Compare_dec.ma Arith/Peano_dec.ma Coq.ma Logic/Decidable.ma NArith/BinPos.ma ZArith/BinInt.ma ZArith/Zcompare.ma ZArith/Zorder.ma
Reals/Integration.ma Reals/Integration.mma
-Logic/RelationalChoice.mma Coq.ma
+Logic/RelationalChoice.mma Coq.ma Init/Prelude.ma
ZArith/Zpower.ma ZArith/Zpower.mma
Init/Prelude.mma Coq.ma Init/Datatypes.ma Init/Logic.ma Init/Notations.ma Init/Peano.ma Init/Specif.ma Init/Wf.ma
Bool/IfProp.mma Bool/Bool.ma Coq.ma
-Arith/Even.mma Coq.ma
+Arith/Even.mma Coq.ma Init/Prelude.ma
Lists/TheoryList.ma Lists/TheoryList.mma
Arith/Wf_nat.ma Arith/Wf_nat.mma
IntMap/Mapsubset.mma Arith/Arith.ma Bool/Bool.ma Bool/Sumbool.ma Coq.ma IntMap/Addec.ma IntMap/Addr.ma IntMap/Adist.ma IntMap/Fset.ma IntMap/Map.ma IntMap/Mapaxioms.ma IntMap/Mapiter.ma ZArith/ZArith.ma
Sets/Multiset.ma Sets/Multiset.mma
Logic/ClassicalFacts.ma Logic/ClassicalFacts.mma
Reals/RiemannInt.mma Arith/Max.ma Coq.ma Logic/Classical_Pred_Type.ma Logic/Classical_Prop.ma Reals/Ranalysis.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/RiemannInt_SF.ma Reals/SeqSeries.ma
-Wellfounded/Inverse_Image.mma Coq.ma
+Wellfounded/Inverse_Image.mma Coq.ma Init/Prelude.ma
Reals/Rsigma.ma Reals/Rsigma.mma
Bool/BoolEq.ma Bool/BoolEq.mma
Wellfounded/Disjoint_Union.ma Wellfounded/Disjoint_Union.mma
Sets/Uniset.ma Sets/Uniset.mma
Sorting/Sorting.mma Coq.ma Lists/List.ma Relations/Relations.ma Sets/Multiset.ma Sorting/Permutation.ma
Init/Wf.mma Coq.ma Init/Datatypes.ma Init/Logic.ma Init/Notations.ma
-Sets/Ensembles.mma Coq.ma
+Sets/Ensembles.mma Coq.ma Init/Prelude.ma
Reals/Cos_plus.mma Arith/Max.ma Coq.ma Reals/Cos_rel.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo_def.ma Reals/SeqSeries.ma
Reals/SplitAbsolu.mma Coq.ma Reals/Rbasic_fun.ma
Relations/Operators_Properties.ma Relations/Operators_Properties.mma
Arith/Div.ma Arith/Div.mma
Sets/Relations_3_facts.mma Coq.ma Sets/Relations_1.ma Sets/Relations_1_facts.ma Sets/Relations_2.ma Sets/Relations_2_facts.ma Sets/Relations_3.ma
Arith/Compare.ma Arith/Compare.mma
-Logic/Hurkens.mma Coq.ma
+Logic/Hurkens.mma Coq.ma Init/Prelude.ma
Arith/Min.mma Arith/Arith.ma Coq.ma
Reals/R_sqr.mma Coq.ma Reals/Rbase.ma Reals/Rbasic_fun.ma
-Bool/Bool.mma Coq.ma
+Bool/Bool.mma Coq.ma Init/Prelude.ma
Reals/Alembert.ma Reals/Alembert.mma
IntMap/Allmaps.mma Coq.ma IntMap/Adalloc.ma IntMap/Addec.ma IntMap/Addr.ma IntMap/Adist.ma IntMap/Fset.ma IntMap/Lsort.ma IntMap/Map.ma IntMap/Mapaxioms.ma IntMap/Mapc.ma IntMap/Mapcanon.ma IntMap/Mapcard.ma IntMap/Mapfold.ma IntMap/Mapiter.ma IntMap/Maplists.ma IntMap/Mapsubset.ma
Sets/Relations_2.mma Coq.ma Sets/Relations_1.ma
Reals/Alembert.mma Arith/Max.ma Coq.ma Reals/PartSum.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rseries.ma Reals/SeqProp.ma
ZArith/Zbool.ma ZArith/Zbool.mma
Sets/Partial_Order.mma Coq.ma Sets/Ensembles.ma Sets/Relations_1.ma
-Logic/ClassicalFacts.mma Coq.ma
+Logic/ClassicalFacts.mma Coq.ma Init/Prelude.ma
Reals/Rdefinitions.mma Coq.ma ZArith/ZArith_base.ma
Reals/PSeries_reg.ma Reals/PSeries_reg.mma
IntMap/Adalloc.ma IntMap/Adalloc.mma
Reals/Rbase.mma Coq.ma Reals/DiscrR.ma Reals/RIneq.ma Reals/Raxioms.ma Reals/Rdefinitions.ma
Sets/Powerset_facts.ma Sets/Powerset_facts.mma
IntMap/Adist.mma Arith/Arith.ma Arith/Min.ma Bool/Bool.ma Coq.ma IntMap/Addr.ma ZArith/ZArith.ma
-NArith/BinPos.mma Coq.ma
+NArith/BinPos.mma Coq.ma Init/Prelude.ma
Lists/Streams.ma Lists/Streams.mma
NArith/NArith.ma NArith/NArith.mma
Relations/Newman.ma Relations/Newman.mma
Arith/Mult.ma Arith/Mult.mma
ZArith/Wf_Z.ma ZArith/Wf_Z.mma
Arith/Div.mma Arith/Compare_dec.ma Arith/Le.ma Coq.ma
-Arith/EqNat.mma Coq.ma
-Bool/DecBool.mma Coq.ma
+Arith/EqNat.mma Coq.ma Init/Prelude.ma
+Bool/DecBool.mma Coq.ma Init/Prelude.ma
Arith/Minus.ma Arith/Minus.mma
ZArith/Zbool.mma Bool/Sumbool.ma Coq.ma ZArith/BinInt.ma ZArith/ZArith_dec.ma ZArith/Zcompare.ma ZArith/Zeven.ma ZArith/Zorder.ma
NArith/BinNat.mma Coq.ma NArith/BinPos.ma
Logic/Classical_Type.mma Coq.ma Logic/Classical_Pred_Type.ma Logic/Classical_Prop.ma
Wellfounded/Transitive_Closure.mma Coq.ma Relations/Relation_Definitions.ma Relations/Relation_Operators.ma
-Logic/Eqdep.mma Coq.ma
+Logic/Eqdep.mma Coq.ma Init/Prelude.ma
Reals/Rtrigo_reg.ma Reals/Rtrigo_reg.mma
Init/Specif.mma Coq.ma Init/Datatypes.ma Init/Logic.ma Init/Notations.ma
Sets/Infinite_sets.mma Arith/Gt.ma Arith/Le.ma Arith/Lt.ma Coq.ma Logic/Classical_Type.ma Sets/Classical_sets.ma Sets/Constructive_sets.ma Sets/Finite_sets.ma Sets/Finite_sets_facts.ma Sets/Image.ma Sets/Powerset.ma Sets/Powerset_Classical_facts.ma Sets/Powerset_facts.ma
NArith/NArith.mma Coq.ma NArith/BinNat.ma NArith/BinPos.ma
NArith/BinNat.ma NArith/BinNat.mma
ZArith/ZArith_dec.mma Bool/Sumbool.ma Coq.ma ZArith/BinInt.ma ZArith/Zcompare.ma ZArith/Zorder.ma
-Relations/Relation_Definitions.mma Coq.ma
+Relations/Relation_Definitions.mma Coq.ma Init/Prelude.ma
Sorting/Sorting.ma Sorting/Sorting.mma
Sets/Image.mma Arith/Gt.ma Arith/Le.ma Arith/Lt.ma Coq.ma Logic/Classical_Type.ma Sets/Classical_sets.ma Sets/Constructive_sets.ma Sets/Finite_sets.ma Sets/Finite_sets_facts.ma Sets/Powerset.ma Sets/Powerset_Classical_facts.ma Sets/Powerset_facts.ma
Reals/Rlimit.mma Coq.ma Logic/Classical_Prop.ma Reals/Rbase.ma Reals/Rfunctions.ma
Reals/Rtrigo_def.ma Reals/Rtrigo_def.mma
IntMap/Adalloc.mma Arith/Arith.ma Bool/Bool.ma Bool/Sumbool.ma Coq.ma IntMap/Addec.ma IntMap/Addr.ma IntMap/Adist.ma IntMap/Fset.ma IntMap/Map.ma ZArith/ZArith.ma
Reals/Rgeom.ma Reals/Rgeom.mma
-Bool/Sumbool.mma Coq.ma
+Bool/Sumbool.mma Coq.ma Init/Prelude.ma
Arith/Compare_dec.mma Arith/Gt.ma Arith/Le.ma Arith/Lt.ma Coq.ma Logic/Decidable.ma
Sorting/Permutation.mma Coq.ma Lists/List.ma Relations/Relations.ma Sets/Multiset.ma
Sets/Classical_sets.mma Coq.ma Logic/Classical_Type.ma Sets/Constructive_sets.ma Sets/Ensembles.ma
IntMap/Mapiter.ma IntMap/Mapiter.mma
Reals/SplitAbsolu.ma Reals/SplitAbsolu.mma
Reals/Ranalysis3.ma Reals/Ranalysis3.mma
-Logic/ChoiceFacts.mma Coq.ma
+Logic/ChoiceFacts.mma Coq.ma Init/Prelude.ma
Reals/Ranalysis3.mma Coq.ma Reals/Ranalysis1.ma Reals/Ranalysis2.ma Reals/Rbase.ma Reals/Rfunctions.ma
Arith/Lt.mma Arith/Le.ma Coq.ma
Reals/Rpower.mma Coq.ma Reals/Exp_prop.ma Reals/MVT.ma Reals/R_sqrt.ma Reals/Ranalysis1.ma Reals/Ranalysis4.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rsqrt_def.ma Reals/Rtrigo.ma Reals/SeqSeries.ma
Reals/Cos_plus.ma Reals/Cos_plus.mma
Reals/MVT.ma Reals/MVT.mma
Reals/SeqProp.ma Reals/SeqProp.mma
-Arith/Le.mma Coq.ma
+Arith/Le.mma Coq.ma Init/Prelude.ma
ZArith/auxiliary.ma ZArith/auxiliary.mma
Sets/Powerset.mma Coq.ma Sets/Cpo.ma Sets/Ensembles.ma Sets/Partial_Order.ma Sets/Relations_1.ma Sets/Relations_1_facts.ma
Reals/SeqSeries.mma Arith/Max.ma Coq.ma Reals/Alembert.ma Reals/AltSeries.ma Reals/Binomial.ma Reals/Cauchy_prod.ma Reals/PartSum.ma Reals/Rbase.ma Reals/Rcomplete.ma Reals/Rfunctions.ma Reals/Rprod.ma Reals/Rseries.ma Reals/Rsigma.ma Reals/SeqProp.ma
IntMap/Mapfold.ma IntMap/Mapfold.mma
Wellfounded/Lexicographic_Product.mma Coq.ma Logic/Eqdep.ma Relations/Relation_Operators.ma Wellfounded/Transitive_Closure.ma
Sets/Integers.ma Sets/Integers.mma
-Logic/Berardi.mma Coq.ma
+Logic/Berardi.mma Coq.ma Init/Prelude.ma
IntMap/Mapcard.ma IntMap/Mapcard.mma
ZArith/Zlogarithm.ma ZArith/Zlogarithm.mma
ZArith/Zhints.mma Coq.ma ZArith/BinInt.ma ZArith/Wf_Z.ma ZArith/Zabs.ma ZArith/Zcompare.ma ZArith/Zmin.ma ZArith/Zmisc.ma ZArith/Znat.ma ZArith/Zorder.ma ZArith/auxiliary.ma
Reals/Cauchy_prod.mma Coq.ma Reals/PartSum.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rseries.ma
Lists/MonoList.ma Lists/MonoList.mma
Reals/Integration.mma Coq.ma Reals/NewtonInt.ma Reals/RiemannInt.ma Reals/RiemannInt_SF.ma
-Sets/Permut.mma Coq.ma
+Sets/Permut.mma Coq.ma Init/Prelude.ma
Reals/Rtrigo_calc.ma Reals/Rtrigo_calc.mma
Reals/DiscrR.ma Reals/DiscrR.mma
Sets/Relations_2_facts.mma Coq.ma Sets/Relations_1.ma Sets/Relations_1_facts.ma Sets/Relations_2.ma
NArith/Pnat.mma Arith/Gt.ma Arith/Le.ma Arith/Lt.ma Arith/Minus.ma Arith/Mult.ma Arith/Plus.ma Coq.ma NArith/BinPos.ma
Sets/Relations_3_facts.ma Sets/Relations_3_facts.mma
Reals/MVT.mma Coq.ma Reals/Ranalysis1.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtopology.ma
-Sets/Relations_1.mma Coq.ma
+Sets/Relations_1.mma Coq.ma Init/Prelude.ma
IntMap/Fset.ma IntMap/Fset.mma
Logic/JMeq.mma Coq.ma Logic/Eqdep.ma
ZArith/Zsqrt.mma Coq.ma ZArith/ZArith_base.ma
Reals/ArithProp.mma Arith/Div2.ma Arith/Even.ma Coq.ma Reals/Rbase.ma Reals/Rbasic_fun.ma
Reals/Ranalysis2.ma Reals/Ranalysis2.mma
Arith/Wf_nat.mma Arith/Lt.ma Coq.ma
-Logic/Eqdep_dec.mma Coq.ma
+Logic/Eqdep_dec.mma Coq.ma Init/Prelude.ma
Reals/Rcomplete.ma Reals/Rcomplete.mma
Sets/Ensembles.ma Sets/Ensembles.mma
-Logic/Decidable.mma Coq.ma
+Logic/Decidable.mma Coq.ma Init/Prelude.ma
ZArith/Zabs.ma ZArith/Zabs.mma
ZArith/Zmin.ma ZArith/Zmin.mma
Sets/Powerset_Classical_facts.mma Coq.ma Logic/Classical_Type.ma Sets/Classical_sets.ma Sets/Constructive_sets.ma Sets/Cpo.ma Sets/Ensembles.ma Sets/Partial_Order.ma Sets/Powerset.ma Sets/Powerset_facts.ma Sets/Relations_1.ma Sets/Relations_1_facts.ma
ZArith/Zbinary.ma ZArith/Zbinary.mma
Arith/Arith.ma Arith/Arith.mma
Logic/ClassicalDescription.ma Logic/ClassicalDescription.mma
-Lists/Streams.mma Coq.ma
+Lists/Streams.mma Coq.ma Init/Prelude.ma
Reals/SeqProp.mma Arith/Max.ma Coq.ma Logic/Classical.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rseries.ma
Reals/RIneq.mma Coq.ma Reals/Raxioms.ma
ZArith/ZArith.mma Coq.ma ZArith/ZArith_base.ma ZArith/Zcomplements.ma ZArith/Zdiv.ma ZArith/Zlogarithm.ma ZArith/Zpower.ma ZArith/Zsqrt.ma
Sorting/Heap.ma Sorting/Heap.mma
Sets/Cpo.ma Sets/Cpo.mma
-Relations/Rstar.mma Coq.ma
+Relations/Rstar.mma Coq.ma Init/Prelude.ma
Reals/Reals.mma Coq.ma Reals/Integration.ma Reals/Ranalysis.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo.ma Reals/SeqSeries.ma
IntMap/Mapcanon.mma Arith/Arith.ma Bool/Bool.ma Bool/Sumbool.ma Coq.ma IntMap/Addec.ma IntMap/Addr.ma IntMap/Adist.ma IntMap/Fset.ma IntMap/Lsort.ma IntMap/Map.ma IntMap/Mapaxioms.ma IntMap/Mapcard.ma IntMap/Mapiter.ma IntMap/Mapsubset.ma Lists/List.ma ZArith/ZArith.ma
Bool/Sumbool.ma Bool/Sumbool.mma
projects / helm.git / commitdiff