From 0b76904a3f10bfd6390d26172fd6979626bd72f4 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 25 Nov 2008 19:27:41 +0000 Subject: [PATCH] cicUtil: we moved here pp_term from proceduralHelpers cicDischarge: some bugs fixed transcript: we now support explicit declaration of dependences procedural/Coq: we added an explicit dependence to Init/Prelude where needed --- .../acic_procedural/proceduralHelpers.ml | 110 ++------------- .../acic_procedural/proceduralHelpers.mli | 2 - .../acic_procedural/proceduralOptimizer.ml | 5 +- .../components/binaries/transcript/engine.ml | 16 ++- helm/software/components/cic/cicUtil.ml | 125 +++++++++++++++++- helm/software/components/cic/cicUtil.mli | 5 + .../cic_proof_checking/cicDischarge.ml | 49 +++++-- .../contribs/procedural/Coq/Arith/EqNat.mma | 2 + .../contribs/procedural/Coq/Arith/Even.mma | 2 + .../contribs/procedural/Coq/Arith/Le.mma | 2 + .../contribs/procedural/Coq/Bool/Bool.mma | 2 + .../contribs/procedural/Coq/Bool/DecBool.mma | 2 + .../contribs/procedural/Coq/Bool/Sumbool.mma | 2 + .../contribs/procedural/Coq/Coq.conf.xml | 24 ++++ .../contribs/procedural/Coq/Lists/Streams.mma | 2 + .../contribs/procedural/Coq/Logic/Berardi.mma | 2 + .../procedural/Coq/Logic/ChoiceFacts.mma | 2 + .../procedural/Coq/Logic/ClassicalFacts.mma | 2 + .../procedural/Coq/Logic/Decidable.mma | 2 + .../contribs/procedural/Coq/Logic/Eqdep.mma | 2 + .../procedural/Coq/Logic/Eqdep_dec.mma | 2 + .../contribs/procedural/Coq/Logic/Hurkens.mma | 2 + .../procedural/Coq/Logic/RelationalChoice.mma | 2 + .../contribs/procedural/Coq/NArith/BinPos.mma | 2 + .../Coq/Relations/Relation_Definitions.mma | 2 + .../procedural/Coq/Relations/Rstar.mma | 2 + .../procedural/Coq/Setoids/Setoid.mma | 2 + .../procedural/Coq/Sets/Ensembles.mma | 2 + .../contribs/procedural/Coq/Sets/Permut.mma | 2 + .../procedural/Coq/Sets/Relations_1.mma | 2 + .../Coq/Wellfounded/Inverse_Image.mma | 2 + .../matita/contribs/procedural/Coq/depends | 46 +++---- 32 files changed, 281 insertions(+), 147 deletions(-) diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml index 7d95d8677..5807e185a 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.ml +++ b/helm/software/components/acic_procedural/proceduralHelpers.ml @@ -35,102 +35,6 @@ module D = Deannotate 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 = @@ -192,18 +96,24 @@ let compose f g x = f (g x) 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 diff --git a/helm/software/components/acic_procedural/proceduralHelpers.mli b/helm/software/components/acic_procedural/proceduralHelpers.mli index 1e0717efa..69df6d797 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.mli +++ b/helm/software/components/acic_procedural/proceduralHelpers.mli @@ -23,8 +23,6 @@ * 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: diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml index 52192f723..1b4cbd8e0 100644 --- a/helm/software/components/acic_procedural/proceduralOptimizer.ml +++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml @@ -35,6 +35,7 @@ module PEH = ProofEngineHelpers module TC = CicTypeChecker module Un = CicUniv module L = Librarian +module Ut = CicUtil module H = ProceduralHelpers module Cl = ProceduralClassify @@ -242,8 +243,8 @@ let optimize_obj = function 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 diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml index 120d31fdd..ccf07423f 100644 --- a/helm/software/components/binaries/transcript/engine.ml +++ b/helm/software/components/binaries/transcript/engine.ml @@ -27,7 +27,7 @@ module R = Helm_registry module X = HExtlib module T = Types module G = Grafite -module HP = Http_getter +module HG = Http_getter module O = Options @@ -48,6 +48,7 @@ type status = { 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; @@ -94,11 +95,11 @@ let init () = 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 @@ -117,7 +118,8 @@ let make registry = 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 @@ -218,6 +220,10 @@ let produce st = 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 @@ -231,7 +237,7 @@ let produce st = 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 diff --git a/helm/software/components/cic/cicUtil.ml b/helm/software/components/cic/cicUtil.ml index 8c42aed61..484814409 100644 --- a/helm/software/components/cic/cicUtil.ml +++ b/helm/software/components/cic/cicUtil.ml @@ -25,7 +25,8 @@ (* $Id$ *) -module C = Cic +module C = Cic +module UM = UriManager exception Meta_not_found of int exception Subst_not_found of int @@ -598,3 +599,125 @@ let is_sober c t = 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" + diff --git a/helm/software/components/cic/cicUtil.mli b/helm/software/components/cic/cicUtil.mli index 54a0a9bea..f6087be52 100644 --- a/helm/software/components/cic/cicUtil.mli +++ b/helm/software/components/cic/cicUtil.mli @@ -71,3 +71,8 @@ val alpha_equivalence: Cic.term -> Cic.term -> bool * 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 diff --git a/helm/software/components/cic_proof_checking/cicDischarge.ml b/helm/software/components/cic_proof_checking/cicDischarge.ml index 52b841952..066eb72c9 100644 --- a/helm/software/components/cic_proof_checking/cicDischarge.ml +++ b/helm/software/components/cic_proof_checking/cicDischarge.ml @@ -27,6 +27,8 @@ module UM = UriManager module C = Cic module Un = CicUniv module E = CicEnvironment +module Ut = CicUtil +module TC = CicTypeChecker let hashtbl_size = 11 @@ -35,8 +37,16 @@ let not_implemented = 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 @@ -122,28 +132,30 @@ let rec discharge_term st t = match t with 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 @@ -166,13 +178,13 @@ and discharge_usubst st s = match s with 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 = @@ -201,26 +213,30 @@ let rec discharge_object dn du obj = | 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 @@ -232,10 +248,15 @@ let rec discharge_object dn du obj = 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 = diff --git a/helm/software/matita/contribs/procedural/Coq/Arith/EqNat.mma b/helm/software/matita/contribs/procedural/Coq/Arith/EqNat.mma index e80c2a8db..141640e21 100644 --- a/helm/software/matita/contribs/procedural/Coq/Arith/EqNat.mma +++ b/helm/software/matita/contribs/procedural/Coq/Arith/EqNat.mma @@ -16,6 +16,8 @@ include "Coq.ma". +include "Init/Prelude.ma". + (*#***********************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) diff --git a/helm/software/matita/contribs/procedural/Coq/Arith/Even.mma b/helm/software/matita/contribs/procedural/Coq/Arith/Even.mma index 8ff5fa56f..eaa51f3c4 100644 --- a/helm/software/matita/contribs/procedural/Coq/Arith/Even.mma +++ b/helm/software/matita/contribs/procedural/Coq/Arith/Even.mma @@ -16,6 +16,8 @@ include "Coq.ma". +include "Init/Prelude.ma". + (*#***********************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) diff --git a/helm/software/matita/contribs/procedural/Coq/Arith/Le.mma b/helm/software/matita/contribs/procedural/Coq/Arith/Le.mma index b10f063f1..7fef16720 100644 --- a/helm/software/matita/contribs/procedural/Coq/Arith/Le.mma +++ b/helm/software/matita/contribs/procedural/Coq/Arith/Le.mma @@ -16,6 +16,8 @@ include "Coq.ma". +include "Init/Prelude.ma". + (*#***********************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) diff --git a/helm/software/matita/contribs/procedural/Coq/Bool/Bool.mma b/helm/software/matita/contribs/procedural/Coq/Bool/Bool.mma index 8dcff09e8..7de881884 100644 --- a/helm/software/matita/contribs/procedural/Coq/Bool/Bool.mma +++ b/helm/software/matita/contribs/procedural/Coq/Bool/Bool.mma @@ -16,6 +16,8 @@ include "Coq.ma". +include "Init/Prelude.ma". + (*#***********************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) diff --git a/helm/software/matita/contribs/procedural/Coq/Bool/DecBool.mma b/helm/software/matita/contribs/procedural/Coq/Bool/DecBool.mma index e5b248c57..8eaaef103 100644 --- a/helm/software/matita/contribs/procedural/Coq/Bool/DecBool.mma +++ b/helm/software/matita/contribs/procedural/Coq/Bool/DecBool.mma @@ -16,6 +16,8 @@ include "Coq.ma". +include "Init/Prelude.ma". + (*#***********************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) diff --git a/helm/software/matita/contribs/procedural/Coq/Bool/Sumbool.mma b/helm/software/matita/contribs/procedural/Coq/Bool/Sumbool.mma index 3659448aa..f79872f73 100644 --- a/helm/software/matita/contribs/procedural/Coq/Bool/Sumbool.mma +++ b/helm/software/matita/contribs/procedural/Coq/Bool/Sumbool.mma @@ -16,6 +16,8 @@ include "Coq.ma". +include "Init/Prelude.ma". + (*#***********************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) diff --git a/helm/software/matita/contribs/procedural/Coq/Coq.conf.xml b/helm/software/matita/contribs/procedural/Coq/Coq.conf.xml index 3d5308d80..4c7d882b8 100644 --- a/helm/software/matita/contribs/procedural/Coq/Coq.conf.xml +++ b/helm/software/matita/contribs/procedural/Coq/Coq.conf.xml @@ -9,6 +9,30 @@ contribs/procedural/Coq .v procedural + + Arith/EqNat Init/Prelude + Arith/Even Init/Prelude + Arith/Le Init/Prelude + Bool/Bool Init/Prelude + Bool/DecBool Init/Prelude + Bool/Sumbool Init/Prelude + Lists/Streams Init/Prelude + Logic/Berardi Init/Prelude + Logic/ChoiceFacts Init/Prelude + Logic/ClassicalFacts Init/Prelude + Logic/Decidable Init/Prelude + Logic/Eqdep Init/Prelude + Logic/Eqdep_dec Init/Prelude + Logic/Hurkens Init/Prelude + Logic/RelationalChoice Init/Prelude + NArith/BinPos Init/Prelude + Relations/Relation_Definitions Init/Prelude + Relations/Rstar Init/Prelude + Setoids/Setoid Init/Prelude + Sets/Ensembles Init/Prelude + Sets/Permut Init/Prelude + Sets/Relations_1 Init/Prelude + Wellfounded/Inverse_Image Init/Prelude