diff options
| -rw-r--r-- | Makefile.build | 22 | ||||
| -rw-r--r-- | Makefile.common | 14 | ||||
| -rw-r--r-- | lib/pp.ml | 2 | ||||
| -rw-r--r-- | ltac/tacinterp.ml | 16 |
4 files changed, 27 insertions, 27 deletions
diff --git a/Makefile.build b/Makefile.build index c6fef10b6a..4f3077e5da 100644 --- a/Makefile.build +++ b/Makefile.build @@ -78,8 +78,8 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) COQOPTS=$(COQ_XML) $(VM) $(NATIVECOMPUTE) BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile -# The SHOW and HIDE variables control whether make will echo complete commands -# or only abbreviated versions. +# The SHOW and HIDE variables control whether make will echo complete commands +# or only abbreviated versions. # Quiet mode is ON by default except if VERBOSE=1 option is given to make SHOW := $(if $(VERBOSE),@true "",@echo "") @@ -231,7 +231,7 @@ grammar/grammar.cma : $(GRAMCMO) $(HIDE)$(CAMLP4O) -I $(MYCAMLP4LIB) $^ -impl test.mlp -o test.ml $(HIDE)$(GRAMC) test.ml -o test-grammar @rm -f test-grammar test.* - $(SHOW)'OCAMLC -a $@' + $(SHOW)'OCAMLC -a $@' $(HIDE)$(GRAMC) $^ -linkall -a -o $@ ## Support of Camlp5 and Camlp5 @@ -283,7 +283,7 @@ minibyte: $(COQTOPBYTE) pluginsbyte ifeq ($(BEST),opt) $(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) - $(SHOW)'COQMKTOP -o $@' + $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) $(LINKMETADATA) -thread -o $@ $(STRIP) $@ $(CODESIGN) $@ @@ -293,7 +293,7 @@ $(COQTOPEXE): $(COQTOPBYTE) endif $(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) - $(SHOW)'COQMKTOP -o $@' + $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -thread -o $@ LOCALCHKLIBS:=$(addprefix -I , $(CHKSRCDIRS) ) @@ -896,7 +896,7 @@ install-emacs: install-latex: $(MKDIR) $(FULLCOQDOCDIR) - $(INSTALLLIB) tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR) + $(INSTALLLIB) tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR) # -$(UPDATETEX) ########################################################################### @@ -968,7 +968,7 @@ dev/printers.cma: dev/printers.mllib $(SHOW)'Testing $@' $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -thread $(SYSCMA) $(P4CMA) $(filter-out %.mllib, $^) -o test-printer @rm -f test-printer - $(SHOW)'OCAMLC -a $@' + $(SHOW)'OCAMLC -a $@' $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -thread $(SYSCMA) $(P4CMA) $(filter-out %.mllib, $^) -linkall -a -o $@ ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here @@ -1107,7 +1107,7 @@ plugins/%_mod.ml: plugins/%.mllib %.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) $(SHOW)'COQC $<' - $(HIDE)rm -f $*.glob + $(HIDE)rm -f $*.glob $(HIDE)$(BOOTCOQC) $< ifdef VALIDATE $(SHOW)'COQCHK $(call vo_to_mod,$@)' @@ -1187,7 +1187,7 @@ otags: Makefile Makefile.build Makefile.common config/Makefile : ; -# For emacs: -# Local Variables: -# mode: makefile +# For emacs: +# Local Variables: +# mode: makefile # End: diff --git a/Makefile.common b/Makefile.common index 37db66be3e..e2f67226b9 100644 --- a/Makefile.common +++ b/Makefile.common @@ -12,7 +12,7 @@ # Executables ########################################################################### -COQMKTOP:=bin/coqmktop$(EXE) +COQMKTOP:=bin/coqmktop$(EXE) COQC:=bin/coqc$(EXE) @@ -35,7 +35,7 @@ else endif INSTALLBIN:=install -INSTALLLIB:=install -m 644 +INSTALLLIB:=install -m 644 INSTALLSH:=./install.sh MKDIR:=install -d @@ -119,7 +119,7 @@ HTMLSTYLE:=simple export TEXINPUTS:=$(HEVEALIB): COQTEXOPTS:=-boot -n 72 -sl -small -DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex +DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-gal.v.tex RefMan-ext.v.tex \ @@ -149,7 +149,7 @@ REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png) ########################################################################### -# Object and Source files +# Object and Source files ########################################################################### COQRUN := coqrun @@ -394,7 +394,7 @@ GTKBIN=$(shell pkg-config --variable=prefix gtk+-2.0)/bin GTKLIBS=$(shell pkg-config --variable=libdir gtk+-2.0) -# For emacs: -# Local Variables: -# mode: makefile +# For emacs: +# Local Variables: +# mode: makefile # End: @@ -44,7 +44,7 @@ end module Tag : sig - type t + type t type 'a key val create : string -> 'a key val inj : 'a -> 'a key -> t diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 4f7c029686..ab61c8abba 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -995,7 +995,7 @@ let interp_bindings ist env sigma = function | NoBindings -> sigma, NoBindings | ImplicitBindings l -> - let sigma, l = interp_open_constr_list ist env sigma l in + let sigma, l = interp_open_constr_list ist env sigma l in sigma, ImplicitBindings l | ExplicitBindings l -> let sigma, l = List.fold_map (interp_binding ist env) sigma l in @@ -1171,7 +1171,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti in Tactic_debug.debug_prompt lev tac eval | _ -> value_interp ist >>= fun v -> return (name_vfun appl v) - + and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacAtom (loc,t) -> @@ -1644,7 +1644,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let env = Proofview.Goal.env gl in let sigma = project gl in let sigma,l' = interp_intro_pattern_list_as_list ist env sigma l in - Tacticals.New.tclWITHHOLES false + Tacticals.New.tclWITHHOLES false (name_atomic ~env (TacIntroPattern l) (* spiwack: print uninterpreted, not sure if it is the @@ -1659,7 +1659,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let sigma = project gl in let l = List.map (fun (k,c) -> let loc, f = interp_open_constr_with_bindings_loc ist c in - (k,(loc,f))) cb + (k,(loc,f))) cb in let sigma,tac = match cl with | None -> sigma, Tactics.apply_with_delayed_bindings_gen a ev l @@ -1672,7 +1672,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacElim (ev,(keep,cb),cbo) -> Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = project gl in + let sigma = project gl in let sigma, cb = interp_constr_with_bindings ist env sigma cb in let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in let named_tac = @@ -1726,7 +1726,7 @@ and interp_atomic ist tac : unit Proofview.tactic = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in - let (sigma,c) = + let (sigma,c) = (if Option.is_empty t then interp_constr else interp_type) ist env sigma c in let sigma, ipat' = interp_intro_pattern_option ist env sigma ipat in @@ -1836,7 +1836,7 @@ and interp_atomic ist tac : unit Proofview.tactic = in let c_interp patvars = { Sigma.run = begin fun sigma -> let lfun' = Id.Map.fold (fun id c lfun -> - Id.Map.add id (Value.of_constr c) lfun) + Id.Map.add id (Value.of_constr c) lfun) patvars ist.lfun in let sigma = Sigma.to_evar_map sigma in @@ -1862,7 +1862,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in let c_interp patvars = { Sigma.run = begin fun sigma -> let lfun' = Id.Map.fold (fun id c lfun -> - Id.Map.add id (Value.of_constr c) lfun) + Id.Map.add id (Value.of_constr c) lfun) patvars ist.lfun in let ist = { ist with lfun = lfun' } in |