From e14fdca3a845ad0b88a34497f41472c3e7f8473b Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 26 Oct 2010 13:20:32 +0000 Subject: [PATCH] Last commit made matita FTBFS. Fixed. --- .../components/METAS/meta.helm-ng_kernel.src | 2 +- .../components/binaries/test_parser/Makefile | 18 +++---------- matita/components/grafite_parser/Makefile | 2 +- .../print_grammar.ml | 0 .../components/ng_paramodulation/nCicBlob.ml | 12 --------- .../components/ng_paramodulation/nCicBlob.mli | 1 - .../components/ng_paramodulation/nCicProof.ml | 26 ------------------- .../ng_paramodulation/nCicProof.mli | 1 - 8 files changed, 6 insertions(+), 56 deletions(-) rename matita/components/{binaries/test_parser => grafite_parser}/print_grammar.ml (100%) diff --git a/matita/components/METAS/meta.helm-ng_kernel.src b/matita/components/METAS/meta.helm-ng_kernel.src index df165a210..f35420375 100644 --- a/matita/components/METAS/meta.helm-ng_kernel.src +++ b/matita/components/METAS/meta.helm-ng_kernel.src @@ -1,4 +1,4 @@ -requires="" +requires="helm-extlib" version="0.0.1" archive(byte)="ng_kernel.cma" archive(native)="ng_kernel.cmxa" diff --git a/matita/components/binaries/test_parser/Makefile b/matita/components/binaries/test_parser/Makefile index 7d5981a57..52f1a4fea 100644 --- a/matita/components/binaries/test_parser/Makefile +++ b/matita/components/binaries/test_parser/Makefile @@ -6,11 +6,11 @@ INTERFACE_FILES = IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = \ - test_parser test_parser.opt test_dep test_dep.opt print_grammar print_grammar.opt + test_parser test_parser.opt test_dep test_dep.opt -all: test_parser test_dep print_grammar +all: test_parser test_dep $(H)echo -n -opt: test_parser.opt test_dep.opt print_grammar.opt +opt: test_parser.opt test_dep.opt $(H)echo -n test_parser: test_parser.ml @@ -33,19 +33,9 @@ test_dep.opt: test_dep.ml $(H)$(OCAMLFIND) ocamlopt \ -I ../../tactics/paramodulation/ -thread -package "$(REQUIRES)" -linkpkg -o $@ $< -print_grammar: print_grammar.ml - $(H)echo " OCAMLC $<" - $(H)$(OCAMLFIND) ocamlc \ - -I ../../tactics/paramodulation/ -rectypes -thread -package "$(REQUIRES)" -linkpkg -o $@ $< - -print_grammar.opt: print_grammar.ml - $(H)echo " OCAMLOPT $<" - $(H)$(OCAMLFIND) ocamlopt \ - -I ../../tactics/paramodulation/ -thread -package "$(REQUIRES)" -linkpkg -o $@ $< - clean: $(H)rm -f *.cm[iox] *.a *.o - $(H)rm -f test_parser test_parser.opt test_dep test_dep.opt print_grammar print_grammar.opt + $(H)rm -f test_parser test_parser.opt test_dep test_dep.opt depend: depend.opt: diff --git a/matita/components/grafite_parser/Makefile b/matita/components/grafite_parser/Makefile index 45ee2aa0f..5583ecb8a 100644 --- a/matita/components/grafite_parser/Makefile +++ b/matita/components/grafite_parser/Makefile @@ -7,7 +7,7 @@ INTERFACE_FILES = \ cicNotation2.mli \ nEstatus.mli \ grafiteDisambiguate.mli \ - print_grammar.mli \ + print_grammar.mli \ $(NULL) IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) diff --git a/matita/components/binaries/test_parser/print_grammar.ml b/matita/components/grafite_parser/print_grammar.ml similarity index 100% rename from matita/components/binaries/test_parser/print_grammar.ml rename to matita/components/grafite_parser/print_grammar.ml diff --git a/matita/components/ng_paramodulation/nCicBlob.ml b/matita/components/ng_paramodulation/nCicBlob.ml index fb9ee6245..d9679bf3a 100644 --- a/matita/components/ng_paramodulation/nCicBlob.ml +++ b/matita/components/ng_paramodulation/nCicBlob.ml @@ -33,18 +33,6 @@ let setoid_eq = let set_default_eqP() = eqPref := default_eqP -let set_reference_of_oxuri f = - let eqnew = function - _ -> - let r = f(UriManager.uri_of_string - "cic:/matita/logic/equality/eq.ind#xpointer(1/1)") - in - NCic.Const r - in - eqPref := eqnew -;; - - module type NCicContext = sig val metasenv : NCic.metasenv diff --git a/matita/components/ng_paramodulation/nCicBlob.mli b/matita/components/ng_paramodulation/nCicBlob.mli index a8b6a7b7e..5d0c7ae2b 100644 --- a/matita/components/ng_paramodulation/nCicBlob.mli +++ b/matita/components/ng_paramodulation/nCicBlob.mli @@ -11,7 +11,6 @@ (* $Id: terms.mli 9822 2009-06-03 15:37:06Z tassi $ *) -val set_reference_of_oxuri: (UriManager.uri -> NReference.reference) -> unit val set_eqP: NCic.term -> unit val set_default_eqP: unit -> unit diff --git a/matita/components/ng_paramodulation/nCicProof.ml b/matita/components/ng_paramodulation/nCicProof.ml index c5290694b..f840d91f9 100644 --- a/matita/components/ng_paramodulation/nCicProof.ml +++ b/matita/components/ng_paramodulation/nCicProof.ml @@ -39,32 +39,6 @@ let set_default_sig () = (*prerr_endline "setting default sig";*) eqsig := default_sig -let set_reference_of_oxuri reference_of_oxuri = - prerr_endline "setting oxuri in nCicProof"; - let nsig = function - | Eq -> - NCic.Const - (reference_of_oxuri - (UriManager.uri_of_string - "cic:/matita/logic/equality/eq.ind#xpointer(1/1)")) - | EqInd_l -> - NCic.Const - (reference_of_oxuri - (UriManager.uri_of_string - "cic:/matita/logic/equality/eq_ind.con")) - | EqInd_r -> - NCic.Const - (reference_of_oxuri - (UriManager.uri_of_string - "cic:/matita/logic/equality/eq_elim_r.con")) - | Refl -> - NCic.Const - (reference_of_oxuri - (UriManager.uri_of_string - "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)")) - in eqsig:= nsig - ;; - (* let debug c r = prerr_endline r; c *) let debug c _ = c;; diff --git a/matita/components/ng_paramodulation/nCicProof.mli b/matita/components/ng_paramodulation/nCicProof.mli index 2aa0a8dd8..f1e1e3b32 100644 --- a/matita/components/ng_paramodulation/nCicProof.mli +++ b/matita/components/ng_paramodulation/nCicProof.mli @@ -13,7 +13,6 @@ type eq_sig_type = Eq | EqInd_l | EqInd_r | Refl -val set_reference_of_oxuri: (UriManager.uri -> NReference.reference) -> unit val set_default_sig: unit -> unit val get_sig: eq_sig_type -> NCic.term -- 2.39.2