aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/checker.ml40
-rw-r--r--ide/coqide.ml4
-rw-r--r--ide/ideutils.ml2
-rw-r--r--interp/constrintern.ml2
-rw-r--r--plugins/extraction/haskell.ml16
-rw-r--r--plugins/micromega/sos.ml74
-rw-r--r--plugins/omega/omega.ml2
-rw-r--r--scripts/coqmktop.ml64
-rw-r--r--tactics/equality.ml2
-rw-r--r--toplevel/metasyntax.ml2
-rw-r--r--toplevel/usage.ml114
-rw-r--r--toplevel/vernacentries.ml2
12 files changed, 163 insertions, 161 deletions
diff --git a/checker/checker.ml b/checker/checker.ml
index a6324c9e5..9213eb134 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -169,26 +169,26 @@ let print_usage_channel co command =
output_string co command;
output_string co "Coq options are:\n";
output_string co
-" -I dir -as coqdir map physical dir to logical coqdir
- -I dir map directory dir to the empty logical path
- -include dir (idem)
- -R dir -as coqdir recursively map physical dir to logical coqdir
- -R dir coqdir (idem)
-
- -admit module load module and dependencies without checking
- -norec module check module but admit dependencies without checking
-
- -where print Coq's standard library location and exit
- -v print Coq version and exit
- -boot boot mode
- -o, --output-context print the list of assumptions
- -m, --memoty print the maximum heap size
- -silent disable trace of constants being checked
-
- -impredicative-set set sort Set impredicative
-
- -h, --help print this list of options
-"
+" -I dir -as coqdir map physical dir to logical coqdir\
+\n -I dir map directory dir to the empty logical path\
+\n -include dir (idem)\
+\n -R dir -as coqdir recursively map physical dir to logical coqdir\
+\n -R dir coqdir (idem)\
+\n\
+\n -admit module load module and dependencies without checking\
+\n -norec module check module but admit dependencies without checking\
+\n\
+\n -where print Coq's standard library location and exit\
+\n -v print Coq version and exit\
+\n -boot boot mode\
+\n -o, --output-context print the list of assumptions\
+\n -m, --memoty print the maximum heap size\
+\n -silent disable trace of constants being checked\
+\n\
+\n -impredicative-set set sort Set impredicative\
+\n\
+\n -h, --help print this list of options\
+\n"
(* print the usage on standard error *)
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 54e130731..a060104c3 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -2430,8 +2430,8 @@ let main files =
("_Fixpoint __", "Fixpoint ident (_ : _) {struct _} : _ :=\n.\n",
29, 5, Some GdkKeysyms._F);
add_complex_template("_Scheme __",
- "Scheme new_scheme := Induction for _ Sort _
-with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
+ "Scheme new_scheme := Induction for _ Sort _\
+\nwith _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
(* Template for match *)
let callback () =
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 0d1704e72..b8eb2754f 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -96,7 +96,7 @@ let try_convert s =
try
do_convert s
with _ ->
- "(* Fatal error: wrong encoding in input.
+ "(* Fatal error: wrong encoding in input. \
Please choose a correct encoding in the preference panel.*)";;
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 8bb240d6e..6316228e7 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1395,7 +1395,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
| (imp::impl', []) ->
if eargs <> [] then
(let (id,(loc,_)) = List.hd eargs in
- user_err_loc (loc,"",str "Not enough non implicit
+ user_err_loc (loc,"",str "Not enough non implicit \
arguments to accept the argument bound to " ++
pr_id id ++ str"."));
[]
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index f1c13d017..1d698d129 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -45,14 +45,14 @@ let preamble mod_name used_modules usf =
(if used_modules = [] then mt () else fnl ()) ++
(if not usf.magic then mt ()
else str "\
-#ifdef __GLASGOW_HASKELL__
-import qualified GHC.Base
-unsafeCoerce = GHC.Base.unsafeCoerce#
-#else
--- HUGS
-import qualified IOExts
-unsafeCoerce = IOExts.unsafeCoerce
-#endif" ++ fnl2 ())
+\n#ifdef __GLASGOW_HASKELL__\
+\nimport qualified GHC.Base\
+\nunsafeCoerce = GHC.Base.unsafeCoerce#\
+\n#else\
+\n-- HUGS\
+\nimport qualified IOExts\
+\nunsafeCoerce = IOExts.unsafeCoerce\
+\n#endif" ++ fnl2 ())
++
(if not usf.mldummy then mt ()
else str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl2 ())
diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml
index 3029496bc..6ddc48e73 100644
--- a/plugins/micromega/sos.ml
+++ b/plugins/micromega/sos.ml
@@ -526,17 +526,17 @@ let sdpa_run_succeeded =
(* ------------------------------------------------------------------------- *)
let sdpa_default_parameters =
-"100 unsigned int maxIteration;
-1.0E-7 double 0.0 < epsilonStar;
-1.0E2 double 0.0 < lambdaStar;
-2.0 double 1.0 < omegaStar;
--1.0E5 double lowerBound;
-1.0E5 double upperBound;
-0.1 double 0.0 <= betaStar < 1.0;
-0.2 double 0.0 <= betaBar < 1.0, betaStar <= betaBar;
-0.9 double 0.0 < gammaStar < 1.0;
-1.0E-7 double 0.0 < epsilonDash;
-";;
+"100 unsigned int maxIteration;\
+\n1.0E-7 double 0.0 < epsilonStar;\
+\n1.0E2 double 0.0 < lambdaStar;\
+\n2.0 double 1.0 < omegaStar;\
+\n-1.0E5 double lowerBound;\
+\n1.0E5 double upperBound;\
+\n0.1 double 0.0 <= betaStar < 1.0;\
+\n0.2 double 0.0 <= betaBar < 1.0, betaStar <= betaBar;\
+\n0.9 double 0.0 < gammaStar < 1.0;\
+\n1.0E-7 double 0.0 < epsilonDash;\
+\n";;
(* ------------------------------------------------------------------------- *)
(* These were suggested by Makoto Yamashita for problems where we are *)
@@ -544,17 +544,17 @@ let sdpa_default_parameters =
(* ------------------------------------------------------------------------- *)
let sdpa_alt_parameters =
-"1000 unsigned int maxIteration;
-1.0E-7 double 0.0 < epsilonStar;
-1.0E4 double 0.0 < lambdaStar;
-2.0 double 1.0 < omegaStar;
--1.0E5 double lowerBound;
-1.0E5 double upperBound;
-0.1 double 0.0 <= betaStar < 1.0;
-0.2 double 0.0 <= betaBar < 1.0, betaStar <= betaBar;
-0.9 double 0.0 < gammaStar < 1.0;
-1.0E-7 double 0.0 < epsilonDash;
-";;
+"1000 unsigned int maxIteration;\
+\n1.0E-7 double 0.0 < epsilonStar;\
+\n1.0E4 double 0.0 < lambdaStar;\
+\n2.0 double 1.0 < omegaStar;\
+\n-1.0E5 double lowerBound;\
+\n1.0E5 double upperBound;\
+\n0.1 double 0.0 <= betaStar < 1.0;\
+\n0.2 double 0.0 <= betaBar < 1.0, betaStar <= betaBar;\
+\n0.9 double 0.0 < gammaStar < 1.0;\
+\n1.0E-7 double 0.0 < epsilonDash;\
+\n";;
let sdpa_params = sdpa_alt_parameters;;
@@ -563,21 +563,21 @@ let sdpa_params = sdpa_alt_parameters;;
(* ------------------------------------------------------------------------- *)
let csdp_default_parameters =
-"axtol=1.0e-8
-atytol=1.0e-8
-objtol=1.0e-8
-pinftol=1.0e8
-dinftol=1.0e8
-maxiter=100
-minstepfrac=0.9
-maxstepfrac=0.97
-minstepp=1.0e-8
-minstepd=1.0e-8
-usexzgap=1
-tweakgap=0
-affine=0
-printlevel=1
-";;
+"axtol=1.0e-8\
+\natytol=1.0e-8\
+\nobjtol=1.0e-8\
+\npinftol=1.0e8\
+\ndinftol=1.0e8\
+\nmaxiter=100\
+\nminstepfrac=0.9\
+\nmaxstepfrac=0.97\
+\nminstepp=1.0e-8\
+\nminstepd=1.0e-8\
+\nusexzgap=1\
+\ntweakgap=0\
+\naffine=0\
+\nprintlevel=1\
+\n";;
let csdp_params = csdp_default_parameters;;
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
index 9ae0205a6..3a5aece76 100644
--- a/plugins/omega/omega.ml
+++ b/plugins/omega/omega.ml
@@ -214,7 +214,7 @@ let rec display_action print_var = function
constant factors.\n" e1.id e2.id
| NEGATE_CONTRADICT(e1,e2,b) ->
Printf.printf
- "Equations E%d and E%d state that their body is at the same time
+ "Equations E%d and E%d state that their body is at the same time \
equal and different\n" e1.id e2.id
| CONSTANT_NOT_NUL (e,k) ->
Printf.printf "Equation E%d states %s = 0.\n" e (sbi k)
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 894ef1266..253df86c7 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -135,20 +135,21 @@ let all_subdirs dir =
(* usage *)
let usage () =
- prerr_endline "Usage: coqmktop <options> <ocaml options> files
-Flags are:
- -coqlib dir Specify where the Coq object files are
- -camlbin dir Specify where the OCaml binaries are
- -camlp4bin dir Specify where the CAmp4/5 binaries are
- -o exec-file Specify the name of the resulting toplevel
- -boot Run in boot mode
- -echo Print calls to external commands
- -ide Build a toplevel for the Coq IDE
- -full Link high level tactics
- -opt Compile in native code
- -searchisos Build a toplevel for SearchIsos
- -top Build Coq on a OCaml toplevel (incompatible with -opt)
- -R dir Specify recursively directories for Ocaml\n";
+ prerr_endline "Usage: coqmktop <options> <ocaml options> files\
+\nFlags are:\
+\n -coqlib dir Specify where the Coq object files are\
+\n -camlbin dir Specify where the OCaml binaries are\
+\n -camlp4bin dir Specify where the CAmp4/5 binaries are\
+\n -o exec-file Specify the name of the resulting toplevel\
+\n -boot Run in boot mode\
+\n -echo Print calls to external commands\
+\n -ide Build a toplevel for the Coq IDE\
+\n -full Link high level tactics\
+\n -opt Compile in native code\
+\n -searchisos Build a toplevel for SearchIsos\
+\n -top Build Coq on a OCaml toplevel (incompatible with -opt)\
+\n -R dir Specify recursively directories for Ocaml\
+\n";
exit 1
(* parsing of the command line *)
@@ -223,23 +224,24 @@ let declare_loading_string () =
if not !top then
"Mltop.remove ();;"
else
- "begin try
- (* Enable rectypes in the toplevel if it has the directive #rectypes *)
- begin match Hashtbl.find Toploop.directive_table \"rectypes\" with
- | Toploop.Directive_none f -> f ()
- | _ -> ()
- end
- with
- | Not_found -> ()
- end;;
-
- let ppf = Format.std_formatter;;
- Mltop.set_top
- {Mltop.load_obj=
- (fun f -> if not (Topdirs.load_file ppf f) then failwith \"error\");
- Mltop.use_file=Topdirs.dir_use ppf;
- Mltop.add_dir=Topdirs.dir_directory;
- Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\n"
+ "begin try\
+\n (* Enable rectypes in the toplevel if it has the directive #rectypes *)\
+\n begin match Hashtbl.find Toploop.directive_table \"rectypes\" with\
+\n | Toploop.Directive_none f -> f ()\
+\n | _ -> ()\
+\n end\
+\n with\
+\n | Not_found -> ()\
+\n end;;\
+\n\
+\n let ppf = Format.std_formatter;;\
+\n Mltop.set_top\
+\n {Mltop.load_obj=\
+\n (fun f -> if not (Topdirs.load_file ppf f) then failwith \"error\");\
+\n Mltop.use_file=Topdirs.dir_use ppf;\
+\n Mltop.add_dir=Topdirs.dir_directory;\
+\n Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\
+\n"
(* create a temporary main file to link *)
let create_tmp_main_file modules =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 4ba91d5f0..9e716aae5 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -607,7 +607,7 @@ let construct_discriminator sigma env dirn c sort =
CP : changed assert false in a more informative error
*)
errorlabstrm "Equality.construct_discriminator"
- (str "Cannot discriminate on inductive constructors with
+ (str "Cannot discriminate on inductive constructors with \
dependent types.") in
let (ind,_) = dest_ind_family indf in
let (mib,mip) = lookup_mind_specif env ind in
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 2f89c5985..efaf7707c 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -365,7 +365,7 @@ let error_not_same_scope x y =
let error_both_bound_and_binding x y =
errorlabstrm "" (strbrk "The recursive variables " ++ pr_id x ++
- strbrk " and " ++ pr_id y ++ strbrk " cannot be used as placeholder
+ strbrk " and " ++ pr_id y ++ strbrk " cannot be used as placeholder \
for both terms and binders.")
(**********************************************************************)
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index a3dbff23c..fc4d18b57 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -18,58 +18,58 @@ let print_usage_channel co command =
output_string co command;
output_string co "Coq options are:\n";
output_string co
-" -I dir -as coqdir map physical dir to logical coqdir
- -I dir map directory dir to the empty logical path
- -include dir (idem)
- -R dir -as coqdir recursively map physical dir to logical coqdir
- -R dir coqdir (idem)
- -top coqdir set the toplevel name to be coqdir instead of Top
- -notop r set the toplevel name to be the empty logical path
- -exclude-dir f exclude subdirectories named f for option -R
-
- -inputstate f read state from file f.coq
- -is f (idem)
- -nois start with an empty state
- -outputstate f write state in file f.coq
- -compat X.Y provides compatibility support for Coq version X.Y
-
- -load-ml-object f load ML object file f
- -load-ml-source f load ML file f
- -load-vernac-source f load Coq file f.v (Load f.)
- -l f (idem)
- -load-vernac-source-verbose f load Coq file f.v (Load Verbose f.)
- -lv f (idem)
- -load-vernac-object f load Coq object file f.vo
- -require f load Coq object file f.vo and import it (Require f.)
- -compile f compile Coq file f.v (implies -batch)
- -compile-verbose f verbosely compile Coq file f.v (implies -batch)
-
- -opt run the native-code version of Coq
- -byte run the bytecode version of Coq
-
- -where print Coq's standard library location and exit
- -config print Coq's configuration information and exit
- -v print Coq version and exit
-
- -q skip loading of rcfile
- -init-file f set the rcfile to f
- -user u use the rcfile of user u
- -batch batch mode (exits just after arguments parsing)
- -boot boot mode (implies -q and -batch)
- -emacs tells Coq it is executed under Emacs
- -noglob do not dump globalizations
- -dump-glob f dump globalizations in file f (to be used by coqdoc)
- -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)
- -impredicative-set set sort Set impredicative
- -load-proofs load opaque proofs in memory (default)
- -dont-load-proofs don't load opaque proofs in memory
- -xml export XML files either to the hierarchy rooted in
- the directory $COQ_XML_LIBRARY_ROOT (if set) or to
- stdout (if unset)
- -quality improve the legibility of the proof terms produced by
- some tactics
- -h, --help print this list of options
-"
+" -I dir -as coqdir map physical dir to logical coqdir\
+\n -I dir map directory dir to the empty logical path\
+\n -include dir (idem)\
+\n -R dir -as coqdir recursively map physical dir to logical coqdir\
+\n -R dir coqdir (idem)\
+\n -top coqdir set the toplevel name to be coqdir instead of Top\
+\n -notop r set the toplevel name to be the empty logical path\
+\n -exclude-dir f exclude subdirectories named f for option -R\
+\n\
+\n -inputstate f read state from file f.coq\
+\n -is f (idem)\
+\n -nois start with an empty state\
+\n -outputstate f write state in file f.coq\
+\n -compat X.Y provides compatibility support for Coq version X.Y\
+\n\
+\n -load-ml-object f load ML object file f\
+\n -load-ml-source f load ML file f\
+\n -load-vernac-source f load Coq file f.v (Load f.)\
+\n -l f (idem)\
+\n -load-vernac-source-verbose f load Coq file f.v (Load Verbose f.)\
+\n -lv f (idem)\
+\n -load-vernac-object f load Coq object file f.vo\
+\n -require f load Coq object file f.vo and import it (Require f.)\
+\n -compile f compile Coq file f.v (implies -batch)\
+\n -compile-verbose f verbosely compile Coq file f.v (implies -batch)\
+\n\
+\n -opt run the native-code version of Coq\
+\n -byte run the bytecode version of Coq\
+\n\
+\n -where print Coq's standard library location and exit\
+\n -config print Coq's configuration information and exit\
+\n -v print Coq version and exit\
+\n\
+\n -q skip loading of rcfile\
+\n -init-file f set the rcfile to f\
+\n -user u use the rcfile of user u\
+\n -batch batch mode (exits just after arguments parsing)\
+\n -boot boot mode (implies -q and -batch)\
+\n -emacs tells Coq it is executed under Emacs\
+\n -noglob do not dump globalizations\
+\n -dump-glob f dump globalizations in file f (to be used by coqdoc)\
+\n -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)\
+\n -impredicative-set set sort Set impredicative\
+\n -load-proofs load opaque proofs in memory (default)\
+\n -dont-load-proofs don't load opaque proofs in memory\
+\n -xml export XML files either to the hierarchy rooted in\
+\n the directory $COQ_XML_LIBRARY_ROOT (if set) or to\
+\n stdout (if unset)\
+\n -quality improve the legibility of the proof terms produced by\
+\n some tactics\
+\n -h, --help print this list of options\
+\n"
(* print the usage on standard error *)
@@ -79,11 +79,11 @@ let print_usage_coqtop () =
print_usage "Usage: coqtop <options>\n\n"
let print_usage_coqc () =
- print_usage "Usage: coqc <options> <Coq options> file...\n
-options are:
- -verbose compile verbosely
- -image f specify an alternative executable for Coq
- -t keep temporary files\n\n"
+ print_usage "Usage: coqc <options> <Coq options> file...\n\
+\noptions are:\
+\n -verbose compile verbosely\
+\n -image f specify an alternative executable for Coq\
+\n -t keep temporary files\n\n"
(* Print the configuration information *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d785a8a40..c5125e9ff 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1128,7 +1128,7 @@ let interp_search_about_item = function
(fun _ -> true) s sc in
GlobSearchSubPattern (Pattern.PRef ref)
with UserError _ ->
- error ("Unable to interp \""^s^"\" either as a reference or
+ error ("Unable to interp \""^s^"\" either as a reference or \
as an identifier component")
let vernac_search s r =
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 23:51:07 +0000