buildTimeConf.cmo matitaprover.cmi
matitaprover.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \
buildTimeConf.cmx matitaprover.cmi
-matitaScript.cmo: matitaTypes.cmi matitaMisc.cmi matitaGtkMisc.cmi \
- matitaEngine.cmi buildTimeConf.cmo applyTransformation.cmi \
- matitaScript.cmi
-matitaScript.cmx: matitaTypes.cmx matitaMisc.cmx matitaGtkMisc.cmx \
- matitaEngine.cmx buildTimeConf.cmx applyTransformation.cmx \
- matitaScript.cmi
+matitaScript.cmo: matitacLib.cmi matitaTypes.cmi matitaMisc.cmi \
+ matitaGtkMisc.cmi matitaEngine.cmi buildTimeConf.cmo \
+ applyTransformation.cmi matitaScript.cmi
+matitaScript.cmx: matitacLib.cmx matitaTypes.cmx matitaMisc.cmx \
+ matitaGtkMisc.cmx matitaEngine.cmx buildTimeConf.cmx \
+ applyTransformation.cmx matitaScript.cmi
matitaTypes.cmo: matitaTypes.cmi
matitaTypes.cmx: matitaTypes.cmi
matitaWiki.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \
buildTimeConf.cmx matitaprover.cmi
matitaprover.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \
buildTimeConf.cmx matitaprover.cmi
-matitaScript.cmo: matitaTypes.cmi matitaMisc.cmi matitaGtkMisc.cmi \
- matitaEngine.cmi buildTimeConf.cmx applyTransformation.cmi \
- matitaScript.cmi
-matitaScript.cmx: matitaTypes.cmx matitaMisc.cmx matitaGtkMisc.cmx \
- matitaEngine.cmx buildTimeConf.cmx applyTransformation.cmx \
- matitaScript.cmi
+matitaScript.cmo: matitacLib.cmi matitaTypes.cmi matitaMisc.cmi \
+ matitaGtkMisc.cmi matitaEngine.cmi buildTimeConf.cmx \
+ applyTransformation.cmi matitaScript.cmi
+matitaScript.cmx: matitacLib.cmx matitaTypes.cmx matitaMisc.cmx \
+ matitaGtkMisc.cmx matitaEngine.cmx buildTimeConf.cmx \
+ applyTransformation.cmx matitaScript.cmi
matitaTypes.cmo: matitaTypes.cmi
matitaTypes.cmx: matitaTypes.cmi
matitaWiki.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \
--- /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 *)
+(* *)
+(**************************************************************************)
+
+
+
+include "Q/q.ma".
+include "ordered_divisible_group.ma".
+
+definition strong_decidable ≝
+ λA:Prop.A ∨ ¬ A.
+
+theorem strong_decidable_to_Not_Not_eq:
+ ∀T:Type.∀eq: T → T → Prop.∀x,y:T.
+ strong_decidable (x=y) → ¬x≠y → x=y.
+ intros;
+ cases s;
+ [ assumption
+ | elim (H H1)
+ ]
+qed.
+
+definition apartness_of_strong_decidable:
+ ∀T:Type.(∀x,y:T.strong_decidable (x=y)) → apartness.
+ intros;
+ constructor 1;
+ [ apply T
+ | apply (λx,y:T.x ≠ y);
+ | simplify;
+ intros 2;
+ apply (H (refl_eq ??));
+ | simplify;
+ intros 4;
+ apply H;
+ symmetry;
+ assumption
+ | simplify;
+ intros;
+ elim (f x z);
+ [ elim (f z y);
+ [ elim H;
+ transitivity z;
+ assumption
+ | right;
+ assumption
+ ]
+ | left;
+ assumption
+ ]
+ ]
+qed.
+
+theorem strong_decidable_to_strong_ext:
+ ∀T:Type.∀sd:∀x,y:T.strong_decidable (x=y).
+ ∀op:T→T. strong_ext (apartness_of_strong_decidable ? sd) op.
+ intros 6;
+ intro;
+ apply a;
+ apply eq_f;
+ assumption;
+qed.
+
+theorem strong_decidable_to_transitive_to_cotransitive:
+ ∀T:Type.∀le:T→T→Prop.(∀x,y:T.strong_decidable (le x y)) →
+ transitive ? le → cotransitive ? (λx,y.¬ (le x y)).
+ intros;
+ whd;
+ simplify;
+ intros;
+ elim (f x z);
+ [ elim (f z y);
+ [ elim H;
+ apply (t ? z);
+ assumption
+ | right;
+ assumption
+ ]
+ | left;
+ assumption
+ ]
+qed.
+
+theorem reflexive_to_coreflexive:
+ ∀T:Type.∀le:T→T→Prop.reflexive ? le → coreflexive ? (λx,y.¬(le x y)).
+ intros;
+ unfold;
+ simplify;
+ intros 2;
+ apply H1;
+ apply H;
+qed.
+
+definition ordered_set_of_strong_decidable:
+ ∀T:Type.∀le:T→T→Prop.(∀x,y:T.strong_decidable (le x y)) →
+ transitive ? le → reflexive ? le → excess.
+ intros;
+ constructor 1;
+ [ apply T
+ | apply (λx,y.¬(le x y));
+ | apply reflexive_to_coreflexive;
+ assumption
+ | apply strong_decidable_to_transitive_to_cotransitive;
+ assumption
+ ]
+qed.
+
+definition abelian_group_of_strong_decidable:
+ ∀T:Type.∀plus:T→T→T.∀zero:T.∀opp:T→T.
+ (∀x,y:T.strong_decidable (x=y)) →
+ associative ? plus (eq T) →
+ commutative ? plus (eq T) →
+ (∀x:T. plus zero x = x) →
+ (∀x:T. plus (opp x) x = zero) →
+ abelian_group.
+ intros;
+ constructor 1;
+ [apply (apartness_of_strong_decidable ? f);]
+ try assumption;
+ [ change with (associative ? plus (λx,y:T.¬x≠y));
+ simplify;
+ intros;
+ intro;
+ apply H2;
+ apply a;
+ | intros 2;
+ intro;
+ apply a1;
+ apply c;
+ | intro;
+ intro;
+ apply a1;
+ apply H
+ | intro;
+ intro;
+ apply a1;
+ apply H1
+ | intros;
+ apply strong_decidable_to_strong_ext;
+ assumption
+ ]
+qed.
+
+definition left_neutral ≝ λC:Type.λop.λe:C. ∀x:C. op e x = x.
+definition left_inverse ≝ λC:Type.λop.λe:C.λinv:C→C. ∀x:C. op (inv x) x = e.
+
+record nabelian_group : Type ≝
+ { ncarr:> Type;
+ nplus: ncarr → ncarr → ncarr;
+ nzero: ncarr;
+ nopp: ncarr → ncarr;
+ nplus_assoc: associative ? nplus (eq ncarr);
+ nplus_comm: commutative ? nplus (eq ncarr);
+ nzero_neutral: left_neutral ? nplus nzero;
+ nopp_inverse: left_inverse ? nplus nzero nopp
+ }.
+
+definition abelian_group_of_nabelian_group:
+ ∀G:nabelian_group.(∀x,y:G.strong_decidable (x=y)) → abelian_group.
+ intros;
+ apply abelian_group_of_strong_decidable;
+ [2: apply (nplus G)
+ | skip
+ | apply (nzero G)
+ | apply (nopp G)
+ | assumption
+ | apply nplus_assoc;
+ | apply nplus_comm;
+ | apply nzero_neutral;
+ | apply nopp_inverse
+ ]
+qed.
+
+definition Z_abelian_group: abelian_group.
+ apply abelian_group_of_nabelian_group;
+ [ constructor 1;
+ [ apply Z
+ | apply Zplus
+ | apply OZ
+ | apply Zopp
+ | whd;
+ intros;
+ symmetry;
+ apply associative_Zplus
+ | apply sym_Zplus
+ | intro;
+ reflexivity
+ | intro;
+ rewrite > sym_Zplus;
+ apply Zplus_Zopp;
+ ]
+ | simplify;
+ intros;
+ unfold;
+ generalize in match (eqZb_to_Prop x y);
+ elim (eqZb x y);
+ simplify in H;
+ [ left ; assumption
+ | right; assumption
+ ]
+ ]
+qed.
+
+record nordered_set: Type ≝
+ { nos_carr:> Type;
+ nos_le: nos_carr → nos_carr → Prop;
+ nos_reflexive: reflexive ? nos_le;
+ nos_transitive: transitive ? nos_le
+ }.
+
+definition excess_of_nordered_group:
+ ∀O:nordered_set.(∀x,y:O. strong_decidable (nos_le ? x y)) → excess.
+ intros;
+ constructor 1;
+ [ apply (nos_carr O)
+ | apply (λx,y.¬(nos_le ? x y))
+ | apply reflexive_to_coreflexive;
+ apply nos_reflexive
+ | apply strong_decidable_to_transitive_to_cotransitive;
+ [ assumption
+ | apply nos_transitive
+ ]
+ ]
+qed.
+
+lemma non_deve_stare_qui: reflexive ? Zle.
+ intro;
+ elim x;
+ [ exact I
+ |2,3: simplify;
+ apply le_n;
+ ]
+qed.
+
+axiom non_deve_stare_qui3: ∀x,y:Z. x < y → x ≤ y.
+
+axiom non_deve_stare_qui4: ∀x,y:Z. x < y → y ≰ x.
+
+definition Z_excess: excess.
+ apply excess_of_nordered_group;
+ [ constructor 1;
+ [ apply Z
+ | apply Zle
+ | apply non_deve_stare_qui
+ | apply transitive_Zle
+ ]
+ | simplify;
+ intros;
+ unfold;
+ generalize in match (Z_compare_to_Prop x y);
+ cases (Z_compare x y); simplify; intro;
+ [ left;
+ apply non_deve_stare_qui3;
+ assumption
+ | left;
+ rewrite > H;
+ apply non_deve_stare_qui
+ | right;
+ apply non_deve_stare_qui4;
+ assumption
+ ]
+ ]
+qed.
\ No newline at end of file
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/fields/".
+
include "attic/rings.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/integration_algebras/".
+
include "attic/vector_spaces.ma".
include "lattice.ma".
].
qed.
-coercion cic:/matita/integration_algebras/rs_lattice.con.
+coercion cic:/matita/attic/integration_algebras/rs_lattice.con.
lemma rs_ordered_abelian_group: ∀K.pre_riesz_space K → ordered_abelian_group.
intros (K V);
]
qed.
-coercion cic:/matita/integration_algebras/rs_ordered_abelian_group.con.
+coercion cic:/matita/attic/integration_algebras/rs_ordered_abelian_group.con.
record is_riesz_space (K:ordered_field_ch0) (V:pre_riesz_space K) : Prop ≝
{ rs_compat_le_times: ∀a:K.∀f:V. 0≤a → 0≤f → 0≤a*f
λR:real.λV:riesz_space R.λnorm:riesz_norm ? V.
n_function R V (rn_norm ? ? norm).
-coercion cic:/matita/integration_algebras/rn_function.con 1.
+coercion cic:/matita/attic/integration_algebras/rn_function.con 1.
(************************** L-SPACES *************************************)
(*
}.
interpretation "Algebra product" 'times a b =
- (cic:/matita/integration_algebras/a_mult.con _ a b).
+ (cic:/matita/attic/integration_algebras/a_mult.con _ a b).
definition ring_of_algebra ≝
λK.λA:algebra K.
mk_ring A (a_mult ? A) (a_one ? A)
(a_ring ? ? ? ? (a_algebra_properties ? A)).
-coercion cic:/matita/integration_algebras/ring_of_algebra.con.
+coercion cic:/matita/attic/integration_algebras/ring_of_algebra.con.
record pre_f_algebra (K:ordered_field_ch0) : Type ≝
{ fa_archimedean_riesz_space:> archimedean_riesz_space K;
]
qed.
-coercion cic:/matita/integration_algebras/fa_algebra.con.
+coercion cic:/matita/attic/integration_algebras/fa_algebra.con.
record is_f_algebra (K) (A:pre_f_algebra K) : Prop ≝
{ compat_mult_le: ∀f,g:A.0 ≤ f → 0 ≤ g → 0 ≤ f*g;
axiom ifa_f_algebra: ∀R:real.integration_f_algebra R → f_algebra R.
-coercion cic:/matita/integration_algebras/ifa_f_algebra.con.
+coercion cic:/matita/attic/integration_algebras/ifa_f_algebra.con.
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/ordered_fields_ch0/".
+
include "attic/fields.ma".
include "ordered_group.ma".
]
qed.
-coercion cic:/matita/ordered_fields_ch0/of_ordered_abelian_group.con.
+coercion cic:/matita/attic/ordered_fields_ch0/of_ordered_abelian_group.con.
(*CSC: I am not able to prove this since unfold is undone by coercion composition*)
axiom of_with1:
]
qed.
-coercion cic:/matita/ordered_fields_ch0/of_cotransitively_ordered_set.con.
+coercion cic:/matita/attic/ordered_fields_ch0/of_cotransitively_ordered_set.con.
record is_ordered_field_ch0 (F:pre_ordered_field_ch0) : Type \def
{ of_mult_compat: ∀a,b:F. 0≤a → 0≤b → 0≤a*b;
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/reals/".
+
include "attic/ordered_fields_ch0.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/rings/".
+
include "group.ma".
qed.
interpretation "Ring mult" 'times a b =
- (cic:/matita/rings/mult.con _ a b).
+ (cic:/matita/attic/rings/mult.con _ a b).
notation "1" with precedence 89
for @{ 'one }.
interpretation "Ring one" 'one =
- (cic:/matita/rings/one.con _).
+ (cic:/matita/attic/rings/one.con _).
lemma eq_mult_zero_x_zero: ∀R:ring.∀x:R.0*x=0.
intros;
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/vector_spaces/".
+
include "attic/reals.ma".
}.
interpretation "Vector space external product" 'times a b =
- (cic:/matita/vector_spaces/emult.con _ _ a b).
+ (cic:/matita/attic/vector_spaces/emult.con _ _ a b).
record is_semi_norm (R:real) (V: vector_space R) (semi_norm:V→R) : Prop \def
{ sn_positive: ∀x:V. zero R ≤ semi_norm x;
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/classical_pointwise/ordered_sets/".
+
include "excess.ma".
for @{ 'hide_everything_but $a }.
interpretation "mk_bounded_above_sequence" 'hide_everything_but a
-= (cic:/matita/ordered_set/bounded_above_sequence.ind#xpointer(1/1/1) _ _ a _).
+= (cic:/matita/classical_pointfree/ordered_sets/bounded_above_sequence.ind#xpointer(1/1/1) _ _ a _).
interpretation "mk_bounded_below_sequence" 'hide_everything_but a
-= (cic:/matita/ordered_set/bounded_below_sequence.ind#xpointer(1/1/1) _ _ a _).
+= (cic:/matita/classical_pointfree/ordered_sets/bounded_below_sequence.ind#xpointer(1/1/1) _ _ a _).
theorem eq_f_sup_sup_f:
∀O':dedekind_sigma_complete_ordered_set.
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/classical_pointfree/ordered_sets2".
+
include "classical_pointfree/ordered_sets.ma".
qed.
interpretation "mk_bounded_sequence" 'hide_everything_but a
-= (cic:/matita/ordered_set/bounded_sequence.ind#xpointer(1/1/1) _ _ a _ _).
+= (cic:/matita/classical_pointfree/ordered_sets/bounded_sequence.ind#xpointer(1/1/1) _ _ a _ _).
lemma reduce_bas_seq:
∀O:ordered_set.∀a:nat→O.∀p.∀i.
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/sets/".
+
include "nat/nat.ma".
+include "logic/connectives.ma".
+
definition set ≝ λX:Type.X → Prop.
for @{ 'member_of $x $A }.
interpretation "Member of" 'member_of x A =
- (cic:/matita/sets/member_of.con _ A x).
+ (cic:/matita/classical_pointwise/sets/member_of.con _ A x).
notation "hvbox(x break ∉ A)" with precedence 60
for @{ 'not_member_of $x $A }.
interpretation "Not member of" 'not_member_of x A =
(cic:/matita/logic/connectives/Not.con
- (cic:/matita/sets/member_of.con _ A x)).
+ (cic:/matita/classical_pointwise/sets/member_of.con _ A x)).
definition emptyset : ∀X.set X ≝ λX:Type.λx:X.False.
notation "∅︀" with precedence 100 for @{ 'emptyset }.
interpretation "Emptyset" 'emptyset =
- (cic:/matita/sets/emptyset.con _).
+ (cic:/matita/classical_pointwise/sets/emptyset.con _).
definition subset: ∀X. set X → set X → Prop≝ λX.λA,B:set X.∀x. x ∈ A → x ∈ B.
for @{ 'subset $A $B }.
interpretation "Subset" 'subset A B =
- (cic:/matita/sets/subset.con _ A B).
+ (cic:/matita/classical_pointwise/sets/subset.con _ A B).
definition intersection: ∀X. set X → set X → set X ≝
λX.λA,B:set X.λx. x ∈ A ∧ x ∈ B.
for @{ 'intersection $A $B }.
interpretation "Intersection" 'intersection A B =
- (cic:/matita/sets/intersection.con _ A B).
+ (cic:/matita/classical_pointwise/sets/intersection.con _ A B).
definition union: ∀X. set X → set X → set X ≝ λX.λA,B:set X.λx. x ∈ A ∨ x ∈ B.
for @{ 'union $A $B }.
interpretation "Union" 'union A B =
- (cic:/matita/sets/union.con _ A B).
+ (cic:/matita/classical_pointwise/sets/union.con _ A B).
definition seq ≝ λX:Type.nat → X.
for @{ 'nth $A $i }.
interpretation "nth" 'nth A i =
- (cic:/matita/sets/nth.con _ A i).
+ (cic:/matita/classical_pointwise/sets/nth.con _ A i).
definition countable_union: ∀X. seq (set X) → set X ≝
λX.λA:seq (set X).λx.∃j.x ∈ A \sub j.
for @{ 'big_union ${default @{(λ${ident i}:$ty.$B)} @{(λ${ident i}.$B)}}}.
interpretation "countable_union" 'big_union η.t =
- (cic:/matita/sets/countable_union.con _ t).
+ (cic:/matita/classical_pointwise/sets/countable_union.con _ t).
definition complement: ∀X. set X \to set X ≝ λX.λA:set X.λx. x ∉ A.
for @{ 'complement $A }.
interpretation "Complement" 'complement A =
- (cic:/matita/sets/complement.con _ A).
+ (cic:/matita/classical_pointwise/sets/complement.con _ A).
definition inverse_image: ∀X,Y.∀f: X → Y.set Y → set X ≝
λX,Y,f,B,x. f x ∈ B.
for @{ 'finverse $f }.
interpretation "Inverse image" 'finverse f =
- (cic:/matita/sets/inverse_image.con _ _ f).
\ No newline at end of file
+ (cic:/matita/classical_pointwise/sets/inverse_image.con _ _ f).
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/sigma_algebra/".
+
include "classical_pointwise/topology.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/topology/".
+
include "classical_pointwise/sets.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/constructive_connectives/".
+include "logic/connectives.ma".
inductive Or (A,B:Type) : Type ≝
Left : A → Or A B
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/constructive_higher_order_relations".
+
include "constructive_connectives.ma".
+include "higher_order_defs/relations.ma".
definition cotransitive ≝
λC:Type.λlt:C→C→Type.∀x,y,z:C. lt x y → lt x z ∨ lt z y.
unfold; intros (x y H); cases H; [right|left] assumption;
qed.
-
\ No newline at end of file
+
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/lebesgue/".
+
include "metric_lattice.ma".
include "sequence.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/divisible_group/".
+
include "nat/orders.ma".
include "group.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/excess/".
+
include "higher_order_defs/relations.ma".
include "nat/plus.ma".
-include "constructive_connectives.ma".
include "constructive_higher_order_relations.ma".
+include "constructive_connectives.ma".
record excess : Type ≝ {
exc_carr:> Type;
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/group/".
+
include "excess.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/lattice/".
+
include "excess.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/metric_lattice/".
+
include "metric_space.ma".
include "lattice.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/metric_space/".
+
include "ordered_divisible_group.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/ordered_divisible_group/".
+
include "nat/orders.ma".
include "nat/times.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/ordered_group/".
+
include "group.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/premetric_lattice/".
+
include "metric_space.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/prevalued_lattice/".
+
include "ordered_group.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/sandwich/".
+
include "nat/plus.ma".
include "nat/orders.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/sequence/".
+
include "excess.ma".
match targets with
| [] ->
(match Librarian.find_roots_in_dir (Sys.getcwd ()) with
- | [x] -> [], x
+ | [x] -> [], Filename.dirname x
| [] ->
prerr_endline "No targets and no root found"; exit 1
| roots ->
let baseuri_of_inv = Hashtbl.create 13 in
let dot_file = ref "" in
(* helpers *)
- let include_paths =
- Helm_registry.get_list Helm_registry.string "matita.includes"
- in
+ let include_paths = ref [] in
let baseuri_of_script s =
try Hashtbl.find baseuri_of s
with Not_found ->
- let _,b,_,_ = Librarian.baseuri_of_script ~include_paths s in
+ let _,b,_,_ =
+ Librarian.baseuri_of_script ~include_paths:!include_paths s
+ in
Hashtbl.add baseuri_of s b;
Hashtbl.add baseuri_of_inv b s;
b
in
- let script_of_baseuri b =
- try Hashtbl.find baseuri_of_inv b
+ let script_of_baseuri ma b =
+ try Some (Hashtbl.find baseuri_of_inv b)
with Not_found ->
- assert false
- (* should be called only after baseuri_of_script is
- * called on every file *)
+ HLog.error ("Skipping dependency of '"^ma^"' over '"^b^"'");
+ HLog.error ("Plase include the file defining such baseuri, or fix");
+ HLog.error ("possibly incorrect verbatim URIs in the .ma file.");
+ None
in
let buri alias = U.buri_of_uri (U.uri_of_string alias) in
let resolve alias current_buri =
exit 1
| [x] ->
Sys.chdir (Filename.dirname x);
+ let opts = Librarian.load_root_file "root" in
+ include_paths :=
+ (try Str.split (Str.regexp " ") (List.assoc "include_paths" opts)
+ with Not_found -> []) @
+ (Helm_registry.get_list Helm_registry.string "matita.includes");
HExtlib.find ~test:(fun x -> Filename.check_suffix x ".ma") "."
| _ ->
let roots = List.map (HExtlib.chop_prefix (Sys.getcwd()^"/")) roots in
let dep = resolve uri ma_baseuri in
(match dep with
| None -> ()
- | Some u -> Hashtbl.add include_deps ma_file (script_of_baseuri u))
+ | Some u ->
+ match script_of_baseuri ma_file u with
+ | Some d -> Hashtbl.add include_deps ma_file d
+ | None -> ())
| DependenciesParser.IncludeDep path ->
+ ignore (baseuri_of_script path);
Hashtbl.add include_deps ma_file path)
dependencies)
ma_files;
projects / helm.git / commitdiff