From f0a793f123683eaab6bab9968725febe7c311f05 Mon Sep 17 00:00:00 2001 From: filliatr Date: Tue, 31 Oct 2000 13:57:01 +0000 Subject: - simplification Makefile (compilation des fichiers .ml'; pas encore parfait car on passe par les fichiers .ml) - Require Export enfin rétabli avec la bonne sémantique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@792 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .depend | 68 +++++++++++++++++++++------------ .depend.camlp4 | 50 +++++++++++++----------- Makefile | 104 ++++++++++++++++++++++++-------------------------- kernel/safe_typing.ml | 13 +++++-- library/library.ml | 40 ++++++++++--------- parsing/.cvsignore | 7 ++++ scripts/.cvsignore | 1 + tactics/.cvsignore | 1 + 8 files changed, 162 insertions(+), 122 deletions(-) create mode 100644 tactics/.cvsignore diff --git a/.depend b/.depend index 757dd9860e..6f84cc27f7 100644 --- a/.depend +++ b/.depend @@ -126,12 +126,13 @@ proofs/refiner.cmi: lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ proofs/stock.cmi: kernel/names.cmi proofs/tacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/environ.cmi \ kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacmach.cmi \ - kernel/term.cmi + proofs/tactic_debug.cmi kernel/term.cmi proofs/tacmach.cmi: parsing/coqast.cmi kernel/environ.cmi \ proofs/evar_refiner.cmi kernel/evd.cmi kernel/names.cmi lib/pp.cmi \ proofs/proof_trees.cmi proofs/proof_type.cmi kernel/reduction.cmi \ proofs/refiner.cmi kernel/sign.cmi pretyping/tacred.cmi kernel/term.cmi -proofs/tactic_debug.cmi: parsing/coqast.cmi proofs/proof_type.cmi +proofs/tactic_debug.cmi: parsing/coqast.cmi kernel/environ.cmi \ + proofs/proof_type.cmi kernel/term.cmi tactics/auto.cmi: tactics/btermdn.cmi proofs/clenv.cmi parsing/coqast.cmi \ kernel/environ.cmi kernel/evd.cmi kernel/names.cmi parsing/pattern.cmi \ proofs/proof_type.cmi pretyping/rawterm.cmi kernel/sign.cmi \ @@ -161,7 +162,6 @@ tactics/tactics.cmi: proofs/clenv.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/names.cmi proofs/proof_type.cmi kernel/reduction.cmi \ proofs/tacmach.cmi pretyping/tacred.cmi tactics/tacticals.cmi \ kernel/term.cmi -tactics/tauto.cmi: proofs/tacmach.cmi kernel/term.cmi tactics/termdn.cmi: parsing/pattern.cmi kernel/term.cmi tactics/wcclausenv.cmi: proofs/clenv.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/names.cmi proofs/proof_type.cmi kernel/sign.cmi proofs/tacmach.cmi \ @@ -426,12 +426,30 @@ parsing/extend.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/lexer.cmi \ parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/extend.cmi parsing/extend.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/lexer.cmx \ parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/extend.cmi +parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \ + toplevel/vernac.cmi +parsing/g_basevernac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \ + toplevel/vernac.cmx +parsing/g_cases.cmo: parsing/coqast.cmi parsing/pcoq.cmi +parsing/g_cases.cmx: parsing/coqast.cmx parsing/pcoq.cmx +parsing/g_constr.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi +parsing/g_constr.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx parsing/g_natsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi \ parsing/coqast.cmi parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi \ lib/pp.cmi lib/util.cmi parsing/g_natsyntax.cmi parsing/g_natsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx \ parsing/coqast.cmx parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmx \ lib/pp.cmx lib/util.cmx parsing/g_natsyntax.cmi +parsing/g_prim.cmo: parsing/coqast.cmi parsing/pcoq.cmi +parsing/g_prim.cmx: parsing/coqast.cmx parsing/pcoq.cmx +parsing/g_tactic.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \ + lib/pp.cmi lib/util.cmi +parsing/g_tactic.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \ + lib/pp.cmx lib/util.cmx +parsing/g_vernac.cmo: parsing/coqast.cmi parsing/pcoq.cmi lib/pp.cmi \ + lib/util.cmi toplevel/vernac.cmi +parsing/g_vernac.cmx: parsing/coqast.cmx parsing/pcoq.cmx lib/pp.cmx \ + lib/util.cmx toplevel/vernac.cmx parsing/g_zsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \ parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi \ lib/util.cmi parsing/g_zsyntax.cmi @@ -472,6 +490,8 @@ parsing/printer.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \ library/global.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ parsing/pattern.cmx lib/pp.cmx kernel/sign.cmx kernel/term.cmx \ parsing/termast.cmx lib/util.cmx parsing/printer.cmi +parsing/q_coqast.cmo: parsing/coqast.cmi parsing/pcoq.cmi +parsing/q_coqast.cmx: parsing/coqast.cmx parsing/pcoq.cmx parsing/termast.cmo: parsing/ast.cmi pretyping/classops.cmi \ parsing/coqast.cmi library/declare.cmi pretyping/detyping.cmi \ kernel/environ.cmi library/impargs.cmi kernel/inductive.cmi \ @@ -724,10 +744,12 @@ proofs/tacmach.cmx: parsing/ast.cmx parsing/astterm.cmx library/declare.cmx \ kernel/reduction.cmx proofs/refiner.cmx kernel/sign.cmx lib/stamps.cmx \ pretyping/tacred.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ proofs/tacmach.cmi -proofs/tactic_debug.cmo: parsing/ast.cmi lib/pp.cmi proofs/proof_trees.cmi \ - proofs/tacmach.cmi proofs/tactic_debug.cmi -proofs/tactic_debug.cmx: parsing/ast.cmx lib/pp.cmx proofs/proof_trees.cmx \ - proofs/tacmach.cmx proofs/tactic_debug.cmi +proofs/tactic_debug.cmo: parsing/ast.cmi lib/pp.cmi parsing/printer.cmi \ + proofs/proof_trees.cmi proofs/tacmach.cmi proofs/tactic_debug.cmi +proofs/tactic_debug.cmx: parsing/ast.cmx lib/pp.cmx parsing/printer.cmx \ + proofs/proof_trees.cmx proofs/tacmach.cmx proofs/tactic_debug.cmi +scripts/coqc.cmo: config/coq_config.cmi toplevel/usage.cmi +scripts/coqc.cmx: config/coq_config.cmx toplevel/usage.cmx scripts/coqmktop.cmo: config/coq_config.cmi scripts/tolink.cmo scripts/coqmktop.cmx: config/coq_config.cmx scripts/tolink.cmx tactics/auto.cmo: parsing/astterm.cmi tactics/btermdn.cmi proofs/clenv.cmi \ @@ -912,18 +934,12 @@ tactics/tactics.cmx: parsing/ast.cmx parsing/astterm.cmx proofs/clenv.cmx \ kernel/sign.cmx lib/stamps.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \ pretyping/tacred.cmx tactics/tacticals.cmx kernel/term.cmx lib/util.cmx \ tactics/tactics.cmi -tactics/tauto.cmo: tactics/auto.cmi proofs/clenv.cmi library/declare.cmi \ - kernel/environ.cmi tactics/hipattern.cmi kernel/names.cmi \ - library/nametab.cmi parsing/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \ - kernel/reduction.cmi pretyping/retyping.cmi kernel/sign.cmi \ - proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \ - kernel/term.cmi lib/util.cmi tactics/tauto.cmi -tactics/tauto.cmx: tactics/auto.cmx proofs/clenv.cmx library/declare.cmx \ - kernel/environ.cmx tactics/hipattern.cmx kernel/names.cmx \ - library/nametab.cmx parsing/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \ - kernel/reduction.cmx pretyping/retyping.cmx kernel/sign.cmx \ - proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \ - kernel/term.cmx lib/util.cmx tactics/tauto.cmi +tactics/tauto.cmo: parsing/ast.cmi parsing/coqast.cmi tactics/hipattern.cmi \ + kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacinterp.cmi \ + proofs/tacmach.cmi tactics/tacticals.cmi +tactics/tauto.cmx: parsing/ast.cmx parsing/coqast.cmx tactics/hipattern.cmx \ + kernel/names.cmx lib/pp.cmx proofs/proof_type.cmx proofs/tacinterp.cmx \ + proofs/tacmach.cmx tactics/tacticals.cmx tactics/termdn.cmo: tactics/dn.cmi kernel/names.cmi parsing/pattern.cmi \ pretyping/rawterm.cmi kernel/term.cmi lib/util.cmi tactics/termdn.cmi tactics/termdn.cmx: tactics/dn.cmx kernel/names.cmx parsing/pattern.cmx \ @@ -936,8 +952,10 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx kernel/evd.cmx \ library/global.cmx proofs/logic.cmx kernel/names.cmx lib/pp.cmx \ proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \ proofs/tacmach.cmx kernel/term.cmx lib/util.cmx tactics/wcclausenv.cmi -tools/coqdep.cmo: config/coq_config.cmi -tools/coqdep.cmx: config/coq_config.cmx +tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo +tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx +tools/coqdep_lexer.cmo: config/coq_config.cmi +tools/coqdep_lexer.cmx: config/coq_config.cmx toplevel/command.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \ kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \ kernel/evd.cmi library/global.cmi library/indrec.cmi kernel/inductive.cmi \ @@ -1075,8 +1093,8 @@ toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \ proofs/proof_trees.cmi proofs/proof_type.cmi toplevel/record.cmi \ kernel/reduction.cmi proofs/refiner.cmi lib/stamps.cmi library/states.cmi \ lib/system.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \ - pretyping/tacred.cmi tactics/tactics.cmi kernel/term.cmi \ - kernel/typeops.cmi lib/util.cmi toplevel/vernacinterp.cmi \ + pretyping/tacred.cmi proofs/tactic_debug.cmi tactics/tactics.cmi \ + kernel/term.cmi kernel/typeops.cmi lib/util.cmi toplevel/vernacinterp.cmi \ toplevel/vernacentries.cmi toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \ pretyping/class.cmx toplevel/command.cmx parsing/coqast.cmx \ @@ -1089,8 +1107,8 @@ toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \ proofs/proof_trees.cmx proofs/proof_type.cmx toplevel/record.cmx \ kernel/reduction.cmx proofs/refiner.cmx lib/stamps.cmx library/states.cmx \ lib/system.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \ - pretyping/tacred.cmx tactics/tactics.cmx kernel/term.cmx \ - kernel/typeops.cmx lib/util.cmx toplevel/vernacinterp.cmx \ + pretyping/tacred.cmx proofs/tactic_debug.cmx tactics/tactics.cmx \ + kernel/term.cmx kernel/typeops.cmx lib/util.cmx toplevel/vernacinterp.cmx \ toplevel/vernacentries.cmi toplevel/vernacinterp.cmo: parsing/ast.cmi toplevel/command.cmi \ parsing/coqast.cmi lib/dyn.cmi toplevel/himsg.cmi kernel/names.cmi \ diff --git a/.depend.camlp4 b/.depend.camlp4 index b1c1782d10..2fb1b6be64 100644 --- a/.depend.camlp4 +++ b/.depend.camlp4 @@ -1,39 +1,45 @@ -parsing/extend.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/lexer.cmi \ - parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/extend.cmi -parsing/extend.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/lexer.cmx \ - parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/extend.cmi +tactics/tauto.cmo: parsing/ast.cmi parsing/coqast.cmi tactics/hipattern.cmi \ + kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacinterp.cmi \ + proofs/tacmach.cmi tactics/tacticals.cmi +tactics/tauto.cmx: parsing/ast.cmx parsing/coqast.cmx tactics/hipattern.cmx \ + kernel/names.cmx lib/pp.cmx proofs/proof_type.cmx proofs/tacinterp.cmx \ + proofs/tacmach.cmx tactics/tacticals.cmx +scripts/coqc.cmo: config/coq_config.cmi toplevel/usage.cmi +scripts/coqc.cmx: config/coq_config.cmx toplevel/usage.cmx +parsing/q_coqast.cmo: parsing/coqast.cmi parsing/pcoq.cmi +parsing/q_coqast.cmx: parsing/coqast.cmx parsing/pcoq.cmx +parsing/g_prim.cmo: parsing/coqast.cmi parsing/pcoq.cmi +parsing/g_prim.cmx: parsing/coqast.cmx parsing/pcoq.cmx +parsing/pcoq.cmo: parsing/coqast.cmi parsing/lexer.cmi lib/pp.cmi \ + lib/util.cmi parsing/pcoq.cmi +parsing/pcoq.cmx: parsing/coqast.cmx parsing/lexer.cmx lib/pp.cmx \ + lib/util.cmx parsing/pcoq.cmi parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \ toplevel/vernac.cmi parsing/g_basevernac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \ toplevel/vernac.cmx -parsing/g_cases.cmo: parsing/coqast.cmi parsing/pcoq.cmi -parsing/g_cases.cmx: parsing/coqast.cmx parsing/pcoq.cmx -parsing/g_constr.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi -parsing/g_constr.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx parsing/g_minicoq.cmo: kernel/environ.cmi parsing/lexer.cmi kernel/names.cmi \ lib/pp.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \ parsing/g_minicoq.cmi parsing/g_minicoq.cmx: kernel/environ.cmx parsing/lexer.cmx kernel/names.cmx \ lib/pp.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \ parsing/g_minicoq.cmi -parsing/g_prim.cmo: parsing/coqast.cmi parsing/pcoq.cmi -parsing/g_prim.cmx: parsing/coqast.cmx parsing/pcoq.cmx -parsing/g_tactic.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \ - lib/pp.cmi lib/util.cmi -parsing/g_tactic.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \ - lib/pp.cmx lib/util.cmx parsing/g_vernac.cmo: parsing/coqast.cmi parsing/pcoq.cmi lib/pp.cmi \ lib/util.cmi toplevel/vernac.cmi parsing/g_vernac.cmx: parsing/coqast.cmx parsing/pcoq.cmx lib/pp.cmx \ lib/util.cmx toplevel/vernac.cmx -parsing/pcoq.cmo: parsing/coqast.cmi parsing/lexer.cmi lib/pp.cmi \ - lib/util.cmi parsing/pcoq.cmi -parsing/pcoq.cmx: parsing/coqast.cmx parsing/lexer.cmx lib/pp.cmx \ - lib/util.cmx parsing/pcoq.cmi -parsing/q_coqast.cmo: parsing/coqast.cmi parsing/pcoq.cmi -parsing/q_coqast.cmx: parsing/coqast.cmx parsing/pcoq.cmi -scripts/coqc.cmo: config/coq_config.cmi toplevel/usage.cmi -scripts/coqc.cmx: config/coq_config.cmx toplevel/usage.cmx +parsing/g_cases.cmo: parsing/coqast.cmi parsing/pcoq.cmi +parsing/g_cases.cmx: parsing/coqast.cmx parsing/pcoq.cmx +parsing/g_constr.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi +parsing/g_constr.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx +parsing/g_tactic.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \ + lib/pp.cmi lib/util.cmi +parsing/g_tactic.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \ + lib/pp.cmx lib/util.cmx +parsing/extend.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/lexer.cmi \ + parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/extend.cmi +parsing/extend.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/lexer.cmx \ + parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/extend.cmi toplevel/mltop.cmo: library/lib.cmi library/libobject.cmi library/library.cmi \ lib/pp.cmi library/summary.cmi lib/system.cmi lib/util.cmi \ toplevel/vernacinterp.cmi toplevel/mltop.cmi diff --git a/Makefile b/Makefile index 1a0d3b749a..7c995fed35 100644 --- a/Makefile +++ b/Makefile @@ -39,10 +39,10 @@ OPTFLAGS=$(INCLUDES) $(CAMLTIMEPROF) OCAMLDEP=ocamldep DEPFLAGS=$(LOCALINCLUDES) -CAMLP4EXTEND=camlp4o $(INCLUDES) pa_extend.cmo +CAMLP4ARGS=$(INCLUDES) pa_extend.cmo OCAMLC_P4O=$(OCAMLC) -pp camlp4o $(BYTEFLAGS) OCAMLOPT_P4O=$(OCAMLOPT) -pp camlp4o $(OPTFLAGS) -CAMLP4IFDEF=camlp4o pa_ifdef.cmo -D$(OSTYPE) +CAMLP4IFDEF=pa_ifdef.cmo -D$(OSTYPE) COQINCLUDES=-I contrib/omega -I contrib/ring -I contrib/xml \ -I theories/Init -I theories/Logic -I theories/Arith \ @@ -120,6 +120,11 @@ HIGHTACTICS=tactics/dhyp.cmo tactics/auto.cmo tactics/equality.cmo \ tactics/refine.cmo SPECTAC=tactics/tauto.ml4 +USERTAC = $(SPECTAC) +ML4FILES += $(USERTAC) +USERTACML=$(USERTAC:.ml4=.ml) +USERTACCMO=$(USERTAC:.ml4=.cmo) +USERTACCMX=$(USERTAC:.ml4=.cmx) CONTRIB=contrib/omega/omega.cmo contrib/omega/coq_omega.cmo \ contrib/ring/quote.cmo contrib/ring/ring.cmo \ @@ -145,11 +150,11 @@ COQBINARIES= $(COQMKTOP) $(COQC) coqtop.byte $(BESTCOQTOP) world: $(COQBINARIES) states theories contrib tools -coqtop.opt: $(COQMKTOP) $(CMX) user-tac-opt +coqtop.opt: $(COQMKTOP) $(CMX) $(USERTACCMX) $(COQMKTOP) -opt $(OPTFLAGS) -o coqtop.opt $(STRIP) ./coqtop.opt -coqtop.byte: $(COQMKTOP) $(CMO) user-tac-byte Makefile +coqtop.byte: $(COQMKTOP) $(CMO) $(USERTACCMO) $(COQMKTOP) -top $(BYTEFLAGS) -o coqtop.byte # coqmktop @@ -169,7 +174,7 @@ scripts/tolink.ml: Makefile echo "let proofs = \""$(PROOFS)"\"" >> $@ echo "let tactics = \""$(TACTICS)"\"" >> $@ echo "let toplevel = \""$(TOPLEVEL)"\"" >> $@ - echo "let hightactics = \""$(HIGHTACTICS)" "$(USERTAC:.ml4=.cmo)"\"" >> $@ + echo "let hightactics = \""$(HIGHTACTICS)" "$(USERTACCMO)"\"" >> $@ echo "let contrib = \""$(CONTRIB)"\"" >> $@ beforedepend:: scripts/tolink.ml @@ -182,8 +187,8 @@ $(COQC): $(COQCCMO) coqtop.byte coqtop.$(BEST) $(OCAMLC) $(BYTEFLAGS) -o $(COQC) -custom unix.cma $(COQCCMO) \ $(OSDEPLIBS) -scripts/coqc.cmo: scripts/coqc.ml4 - $(OCAMLC) $(BYTEFLAGS) -c -pp "$(CAMLP4IFDEF) -impl" -impl $< +scripts/coqc.ml scripts/coqc.cmo scripts/coqc.cmx: CAMLP4ARGS=$(CAMLP4IFDEF) +ML4FILES += scripts/coqc.ml4 archclean:: rm -f scripts/coqc scripts/coqmktop @@ -345,19 +350,14 @@ archclean:: # (intended to be rather generic) ########################################################################### -USERTAC = $(SPECTAC) - -CAMLP4GRAMMAR = camlp4o -I parsing pa_extend.cmo grammar.cma -OPTCAMLP4GRAMMAR = camlp4o -I parsing pa_extend.cmo grammar.cma \ - $(OSDEPP4OPTFLAGS) +CAMLP4GRAMMAR = -I parsing pa_extend.cmo grammar.cma COQCMO = names.cmo ast.cmo g_tactic.cmo g_constr.cmo -user-tac-byte: parsing/grammar.cma - for i in $(USERTAC); do $(OCAMLC) $(BYTEFLAGS) -c -pp "$(CAMLP4GRAMMAR) -I kernel $(COQCMO) -impl" -impl $$i; done +$(USERTACML): CAMLP4ARGS=$(CAMLP4GRAMMAR) -I kernel $(COQCMO) +$(USERTACCMO): CAMLP4ARGS=$(CAMLP4GRAMMAR) -I kernel $(COQCMO) +$(USERTACCMX): CAMLP4ARGS=$(CAMLP4GRAMMAR) -I kernel $(COQCMO) -user-tac-opt: parsing/grammar.cma - for i in $(USERTAC); do $(OCAMLOPT) $(OPTFLAGS) -c -pp "$(OPTCAMLP4GRAMMAR) -I kernel $(COQCMO) -impl" -impl $$i; done ########################################################################### # tools @@ -481,16 +481,17 @@ beforedepend:: parsing/lexer.ml # grammar modules with camlp4 -parsing/q_coqast.cmo: parsing/q_coqast.ml4 - $(OCAMLC) $(BYTEFLAGS) -c -pp "camlp4o q_MLast.cmo -impl" -impl $< +QCOQAST=parsing/q_coqast.ml4 +ML4FILES += $(QCOQAST) +$(QCOQAST:.ml4=.ml): CAMLP4ARGS=q_MLast.cmo +$(QCOQAST:.ml4=.cmo): CAMLP4ARGS=q_MLast.cmo +$(QCOQAST:.ml4=.cmx): CAMLP4ARGS=q_MLast.cmo -# the generic rules could be used for g_prim.ml4, but this implies -# circular dependencies between g_prim and grammar -parsing/g_prim.cmo: parsing/g_prim.ml4 - $(OCAMLC) $(BYTEFLAGS) -c -pp "$(CAMLP4EXTEND) -impl" -impl $< - -parsing/g_prim.cmx: parsing/g_prim.ml4 - $(OCAMLOPT) $(OPTFLAGS) -c -pp "$(CAMLP4EXTEND) -impl" -impl $< +GPRIM=parsing/g_prim.ml4 parsing/pcoq.ml4 +ML4FILES += $(GPRIM) +$(GPRIM:.ml4=.ml): CAMLP4ARGS=pa_extend.cmo +$(GPRIM:.ml4=.cmo): CAMLP4ARGS=pa_extend.cmo +$(GPRIM:.ml4=.cmx): CAMLP4ARGS=pa_extend.cmo GRAMMARCMO=lib/pp_control.cmo lib/pp.cmo lib/util.cmo lib/dyn.cmo \ lib/hashcons.cmo parsing/coqast.cmo parsing/lexer.cmo \ @@ -502,34 +503,28 @@ parsing/grammar.cma: $(GRAMMARCMO) clean:: rm -f parsing/grammar.cma -parsing/g_%.cmo: parsing/g_%.ml4 parsing/grammar.cma - $(OCAMLC) $(BYTEFLAGS) -c -pp "$(CAMLP4GRAMMAR) -impl" -impl $< - -parsing/g_%.cmx: parsing/g_%.ml4 parsing/grammar.cma - $(OCAMLOPT) $(OPTFLAGS) -c -pp "$(OPTCAMLP4GRAMMAR) -impl" -impl $< - -parsing/extend.cmo: parsing/extend.ml4 parsing/grammar.cma - $(OCAMLC) $(BYTEFLAGS) -c -pp "$(CAMLP4GRAMMAR) -impl" -impl $< - -parsing/extend.cmx: parsing/extend.ml4 parsing/grammar.cma - $(OCAMLOPT) $(OPTFLAGS) -c -pp "$(CAMLP4GRAMMAR) -impl" -impl $< +PARSINGML4=parsing/g_basevernac.ml4 parsing/g_minicoq.ml4 \ + parsing/g_vernac.ml4 parsing/g_cases.ml4 \ + parsing/g_constr.ml4 parsing/g_tactic.ml4 parsing/extend.ml4 +ML4FILES += $(PARSINGML4) +$(PARSINGML4:.ml4=.ml): parsing/grammar.cma +$(PARSINGML4:.ml4=.cmo) $(PARSINGML4:.ml4=.cmx): parsing/grammar.cma +$(PARSINGML4:.ml4=.ml): CAMLP4ARGS=$(CAMLP4GRAMMAR) +$(PARSINGML4:.ml4=.cmo) $(PARSINGML4:.ml4=.cmx): CAMLP4ARGS=$(CAMLP4GRAMMAR) beforedepend:: $(GRAMMARCMO) -parsing/pcoq.ml: parsing/pcoq.ml4 - $(CAMLP4EXTEND) pr_o.cmo -impl $< -o $@ - -parsing/extend.ml: parsing/extend.ml4 parsing/grammar.cma - $(CAMLP4GRAMMAR) pr_o.cmo -impl $< -o $@ - beforedepend:: parsing/pcoq.ml parsing/extend.ml # toplevel/mltop.ml4 (ifdef Byte) +toplevel/mltop.ml: CAMLP4ARGS=$(CAMLP4IFDEF) toplevel/mltop.cmo: toplevel/mltop.ml4 - $(OCAMLC) $(BYTEFLAGS) -c -pp "$(CAMLP4IFDEF) -DByte -impl" -impl $< + $(OCAMLC) $(BYTEFLAGS) -pp "camlp4o $(CAMLP4IFDEF) -DByte -impl" \ + -c -impl $< toplevel/mltop.cmx: toplevel/mltop.ml4 - $(OCAMLOPT) $(OPTFLAGS) -c -pp "$(CAMLP4IFDEF) -impl" -impl $< + $(OCAMLOPT) $(OPTFLAGS) -pp "camlp4o $(CAMLP4IFDEF) -impl" -c -impl $< +ML4FILES += toplevel/mltop.ml4 ########################################################################### # Default rules @@ -550,10 +545,13 @@ toplevel/mltop.cmx: toplevel/mltop.ml4 ocamllex $< .ml4.cmo: - $(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4EXTEND) -impl" -c -impl $< + $(OCAMLC) $(BYTEFLAGS) -pp "camlp4o $(CAMLP4ARGS) -impl" -c -impl $< .ml4.cmx: - $(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4EXTEND) -impl" -c -impl $< + $(OCAMLOPT) $(OPTFLAGS) -pp "camlp4o $(CAMLP4ARGS) -impl" -c -impl $< + +.ml4.ml: + camlp4o pr_o.cmo $(CAMLP4ARGS) -impl $< > $@ || rm -f $@ .v.vo: $(COQC) -q -$(BEST) $(COQINCLUDES) $< @@ -614,14 +612,12 @@ depend: beforedepend dependcoq: beforedepend tools/coqdep $(COQINCLUDES) */*.v */*/*.v > .depend.coq -dependcamlp4: beforedepend - rm -f .depend.camlp4 - for f in */*.ml4; do \ - file=`dirname $$f`/`basename $$f .ml4`; \ - camlp4o $(INCLUDES) -I . pa_ifdef.cmo pa_extend.cmo q_MLast.cmo $(GRAMMARCMO) pr_o.cmo -impl $$f > $$file.ml; \ - ocamldep $(DEPFLAGS) $$file.ml >> .depend.camlp4; \ - rm -f $$file.ml; \ - done +ML4FILESML = $(ML4FILES:.ml4=.ml) +dependcamlp4: beforedepend $(ML4FILESML) + ocamldep $(DEPFLAGS) $(ML4FILESML) > .depend.camlp4 + +clean:: + rm -f $(ML4FILESML) include .depend include .depend.coq diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 7b7c95d4bf..af46e221e2 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -208,7 +208,8 @@ let unsafe_infer_type env constr = (* ``Type of'' machines. *) let type_of env c = - let (j,_) = safe_infer env c in nf_betaiota env Evd.empty (body_of_type j.uj_type) + let (j,_) = safe_infer env c in + nf_betaiota env Evd.empty (body_of_type j.uj_type) (* Typing of several terms. *) @@ -281,12 +282,15 @@ let add_constant_with_value sp body typ env = let (jt,cst') = safe_infer env ty in let env'' = add_constraints cst' env' in try - let cst'' = conv env'' Evd.empty (body_of_type jb.uj_type) jt.uj_val in + let cst'' = + conv env'' Evd.empty (body_of_type jb.uj_type) jt.uj_val + in let env'' = add_constraints cst'' env'' in (env'', assumption_of_judgment env'' Evd.empty jt, Constraint.union cst' cst'') with NotConvertible -> - error_actual_type CCI env jb.uj_val (body_of_type jb.uj_type) jt.uj_val + error_actual_type + CCI env jb.uj_val (body_of_type jb.uj_type) jt.uj_val in let ids = Idset.union (global_vars_set body) (global_vars_set (body_of_type ty)) @@ -396,7 +400,8 @@ let type_one_constructor env_ar nparams arsort c = let infos = let (params,dc) = mind_extract_params nparams c in let env_par = push_rels params env_ar in - infos_and_sort env_par dc in + infos_and_sort env_par dc + in (* Constructors are typed-checked here *) let (j,cst) = safe_infer_type env_ar c in diff --git a/library/library.ml b/library/library.ml index 85e9708fee..d938bd635c 100644 --- a/library/library.ml +++ b/library/library.ml @@ -8,7 +8,7 @@ open Environ open Libobject open Lib -(*s This generates commands Add Path, Remove Path, Print Path *) +(*s Load path. Used for commands Add Path, Remove Path, Print Path *) let loadpath_name = "LoadPath" @@ -77,7 +77,8 @@ let loaded_modules () = Stringmap.fold (fun s _ l -> s :: l) !modules_table [] let opened_modules () = - Stringmap.fold (fun s m l -> if m.module_opened then s :: l else l) + Stringmap.fold + (fun s m l -> if m.module_opened then s :: l else l) !modules_table [] let module_segment = function @@ -103,12 +104,18 @@ let segment_iter f = iter -(*s [open_module s] opens a module which is assumed to be already loaded. *) +(*s [open_module s] opens a module. The module [s] and all modules needed by + [s] are assumed to be already loaded. When opening [s] we recursively open + all the modules needed by [s] and tagged [exported]. *) -let open_module s = +let open_objects decls = + segment_iter open_object decls + +let rec open_module s = let m = find_module s in if not m.module_opened then begin - segment_iter open_object m.module_declarations; + List.iter (fun (m,_,exp) -> if exp then open_module m) m.module_deps; + open_objects m.module_declarations; m.module_opened <- true end @@ -122,7 +129,7 @@ let open_module s = let load_objects decls = segment_iter load_object decls -let rec load_module_from doexp s f = +let rec load_module_from s f = let (fname,ch) = raw_intern_module (get_load_path ()) f in let md = System.marshal_in ch in let digest = System.marshal_in ch in @@ -132,32 +139,31 @@ let rec load_module_from doexp s f = module_compiled_env = md.md_compiled_env; module_declarations = md.md_declarations; module_opened = false; - module_exported = doexp; + module_exported = false; module_deps = md.md_deps; module_digest = digest } in if s <> md.md_name then error ("The file " ^ fname ^ " does not contain module " ^ s); - List.iter (load_mandatory_module doexp s) m.module_deps; + List.iter (load_mandatory_module s) m.module_deps; Global.import m.module_compiled_env; load_objects m.module_declarations; modules_table := Stringmap.add s m !modules_table; m -and load_mandatory_module doexp caller (s,d,export) = - let m = find_module export s s in +and load_mandatory_module caller (s,d,_) = + let m = find_module s s in if d <> m.module_digest then - error ("module "^caller^" makes inconsistent assumptions over module "^s); - if doexp && export then open_module s + error ("module "^caller^" makes inconsistent assumptions over module "^s) -and find_module doexp s f = +and find_module s f = try Stringmap.find s !modules_table with Not_found -> - load_module_from doexp s f + load_module_from s f let load_module s = function - | None -> let _ = load_module_from true s s in () - | Some f -> let _ = load_module_from true s f in () + | None -> let _ = load_module_from s s in () + | Some f -> let _ = load_module_from s f in () (*s [require_module] loads and opens a module. *) @@ -166,7 +172,7 @@ let require_module spec name fileopt export = let file = match fileopt with | None -> name | Some f -> f in - let m = load_module_from true name file in + let m = load_module_from name file in open_module name; if export then m.module_exported <- true diff --git a/parsing/.cvsignore b/parsing/.cvsignore index 7d96a5222d..41e9ca1c99 100644 --- a/parsing/.cvsignore +++ b/parsing/.cvsignore @@ -2,3 +2,10 @@ lexer.ml *.ppo pcoq.ml extend.ml +g_prim.ml +q_coqast.ml +g_basevernac.ml +g_vernac.ml +g_tactic.ml +g_constr.ml +g_cases.ml diff --git a/scripts/.cvsignore b/scripts/.cvsignore index b95eb1ba95..ee865a5683 100644 --- a/scripts/.cvsignore +++ b/scripts/.cvsignore @@ -1,3 +1,4 @@ coqmktop tolink.ml coqc +coqc.ml diff --git a/tactics/.cvsignore b/tactics/.cvsignore new file mode 100644 index 0000000000..5ff239d459 --- /dev/null +++ b/tactics/.cvsignore @@ -0,0 +1 @@ +tauto.ml -- cgit v1.2.3