From 8300ef2c07a17451f594bcbd6f0689cafb87c3fb Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Tue, 5 Feb 2019 10:40:49 -0500 Subject: Refresh patches --- debian/patches/python-scripts-libraries.patch | 2 +- debian/patches/remove-tests-that-need-coqlib.patch | 387 +++++++++++---------- debian/patches/series | 1 - debian/patches/spelling.patch | 320 ----------------- 4 files changed, 207 insertions(+), 503 deletions(-) delete mode 100644 debian/patches/spelling.patch diff --git a/debian/patches/python-scripts-libraries.patch b/debian/patches/python-scripts-libraries.patch index 66a4a9e9..c4f662a8 100644 --- a/debian/patches/python-scripts-libraries.patch +++ b/debian/patches/python-scripts-libraries.patch @@ -5,7 +5,7 @@ Forwarded: not-needed Eliminate the .py extension from executable Python scripts. --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in -@@ -91,9 +91,9 @@ +@@ -90,9 +90,9 @@ COQMKFILE ?= "$(COQBIN)coq_makefile" # Timing scripts diff --git a/debian/patches/remove-tests-that-need-coqlib.patch b/debian/patches/remove-tests-that-need-coqlib.patch index 48cd1b96..be694991 100644 --- a/debian/patches/remove-tests-that-need-coqlib.patch +++ b/debian/patches/remove-tests-that-need-coqlib.patch @@ -1,6 +1,5 @@ From: Benjamin Barenblat Subject: Disable tests which require -coqlib to be set -Bug: https://github.com/coq/coq/issues/5975 Forwarded: not-needed A number of tests (mostly for coq_makefile) assume that Coq is @@ -8,10 +7,9 @@ installed when the test runs. This isn't true in an sbuild environment, though, so disable those tests. --- a/test-suite/misc/printers.sh +++ /dev/null -@@ -1,3 +0,0 @@ --printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | egrep "Error|Unbound" --if [ $? = 0 ]; then exit 1; else exit 0; fi -- +@@ -1,2 +0,0 @@ +-#!/bin/sh +-if printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | grep -E "Error|Unbound" ; then exit 1; else exit 0; fi --- a/test-suite/coq-makefile/arg/run.sh +++ /dev/null @@ -1,7 +0,0 @@ @@ -33,9 +31,96 @@ though, so disable those tests. -cat Makefile.conf -make -exec test -f "subdir/done" +--- a/test-suite/coq-makefile/emptyprefix/run.sh ++++ /dev/null +@@ -1,17 +0,0 @@ +-#!/usr/bin/env bash +- +-set -e +- +-. ../template/init.sh +- +-mv theories/sub theories2 +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +- +-cp ../_CoqProject.sub theories2/_CoqProject +-cd theories2 +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +--- a/test-suite/coq-makefile/extend-subdirs/run.sh ++++ /dev/null +@@ -1,8 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-exec test -f "subdir/done" +--- a/test-suite/coq-makefile/latex1/run.sh ++++ /dev/null +@@ -1,13 +0,0 @@ +-#!/usr/bin/env bash +- +-if which pdflatex; then +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-exec make all.pdf +- +-fi +-exit 0 # test skipped +--- a/test-suite/coq-makefile/merlin1/run.sh ++++ /dev/null +@@ -1,13 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make .merlin +-cat > desired < actual +-exec diff -u desired actual +--- a/test-suite/coq-makefile/only/run.sh ++++ /dev/null +@@ -1,10 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make only TGTS="src/test.cmi src/test_aux.cmi" -j2 +-test -f src/test.cmi +-test -f src/test_aux.cmi +-! test -f src/test.cmo +--- a/test-suite/coq-makefile/validate1/run.sh ++++ /dev/null +@@ -1,8 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-exec make validate --- a/test-suite/coq-makefile/coqdoc1/run.sh +++ /dev/null -@@ -1,51 +0,0 @@ +@@ -1,59 +0,0 @@ -#!/usr/bin/env bash - -. ../template/init.sh @@ -47,7 +132,15 @@ though, so disable those tests. -make install DSTROOT="$PWD/tmp" -make install-doc DSTROOT="$PWD/tmp" -#make debug --(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual +- +-# to learn about <(cmd) see https://www.gnu.org/software/bash/manual/html_node/Process-Substitution.html +-( +- while IFS= read -r -d '' d +- do +- pushd "$d" >/dev/null && find . && popd >/dev/null +- done < <(find tmp -name user-contrib -print0) +-) | sort -u > actual +- -sort -u > desired </dev/null && find . && popd >/dev/null; done) | sort -u > actual +-( +- while IFS= read -r -d '' d +- do +- pushd "$d" >/dev/null && find . && popd >/dev/null +- done < <(find tmp -name user-contrib -print0) +-) | sort -u > actual +- -sort -u > desired </dev/null; then - # the only way I found to pass OCAMLPATH on win is to have it contain - # only one entry -- export OCAMLPATH=`cygpath -w $PWD/findlib` +- OCAMLPATH=$(cygpath -w "$PWD"/findlib) +- export OCAMLPATH -fi -make -C findlib/foo clean -coq_makefile -f _CoqProject -o Makefile @@ -193,38 +262,6 @@ though, so disable those tests. -make -C findlib/foo -make -make byte ---- a/test-suite/coq-makefile/latex1/run.sh -+++ /dev/null -@@ -1,13 +0,0 @@ --#!/usr/bin/env bash -- --if which pdflatex; then -- --. ../template/init.sh -- --coq_makefile -f _CoqProject -o Makefile --cat Makefile.conf --make --exec make all.pdf -- --fi --exit 0 # test skipped ---- a/test-suite/coq-makefile/merlin1/run.sh -+++ /dev/null -@@ -1,13 +0,0 @@ --#!/usr/bin/env bash -- --. ../template/init.sh -- --coq_makefile -f _CoqProject -o Makefile --cat Makefile.conf --make .merlin --cat > desired < actual --exec diff -u desired actual --- a/test-suite/coq-makefile/mlpack1/run.sh +++ /dev/null @@ -1,23 +0,0 @@ @@ -238,7 +275,7 @@ though, so disable those tests. -make html mlihtml -make install DSTROOT="$PWD/tmp" -#make debug --(cd `find tmp -name user-contrib` && find .) | sort > actual +-(cd "$(find tmp -name user-contrib)" && find .) | sort > actual -sort > desired < actual +-(cd "$(find tmp -name user-contrib)" && find .) | sort > actual -sort > desired </dev/null && find . && popd >/dev/null; done) | sort -u > actual +-( +- while IFS= read -r -d '' d +- do +- pushd "$d" >/dev/null && find . && popd >/dev/null +- done < <(find tmp -name user-contrib -print0) +-) | sort -u > actual -sort > desired < actual +-(cd "$(find tmp -name user-contrib)" && find .) | sort > actual -sort > desired < actual +-(cd "$(find tmp -name user-contrib)" && find .) | sort > actual -sort > desired < actual +-(cd "$(find tmp -name user-contrib)" && find .) | sort > actual -sort > desired </dev/null && find . && popd >/dev/null; done) | sort -u > actual --sort -u > desired </dev/null && find . && popd >/dev/null; done) | sort -u > actual --sort -u > desired < ${file}${ext}.processed -- done --done -for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do -- echo "cat $file" -- cat "$file" -- echo -- diff -u $file.desired.processed $file.processed || exit $? +- for ext in "" .desired; do +- grep -v 'warning: undefined variable' < ${file}${ext} | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_FILE[@]}" > ${file}${ext}.processed +- done +- echo "cat $file" +- cat "$file" +- echo +- diff -u $file.desired.processed $file.processed || exit $? -done - -cd ../per-file-before @@ -621,13 +579,80 @@ though, so disable those tests. -cat A.v.timing.diff -echo - +-file=A.v.timing.diff +- -for ext in "" .desired; do -- for file in A.v.timing.diff; do -- cat ${file}${ext} | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_LINE[@]}" | sort > ${file}${ext}.processed -- done --done --for file in A.v.timing.diff; do -- diff -u $file.desired.processed $file.processed || exit $? +- sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_LINE[@]}" < "${file}${ext}" | sort > "${file}${ext}.processed" -done - +-diff -u "$file.desired.processed" "$file.processed" || exit $? +- -exit 0 +--- a/test-suite/coq-makefile/uninstall1/run.sh ++++ /dev/null +@@ -1,23 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-make html mlihtml +-make install DSTROOT="$PWD/tmp" +-make install-doc DSTROOT="$PWD/tmp" +-make uninstall DSTROOT="$PWD/tmp" +-make uninstall-doc DSTROOT="$PWD/tmp" +-#make debug +-( +- while IFS= read -r -d '' d +- do +- pushd "$d" >/dev/null && find . && popd >/dev/null +- done < <(find tmp -name user-contrib -print0) +-) | sort -u > actual +-sort -u > desired </dev/null && find . && popd >/dev/null +- done < <(find tmp -name user-contrib -print0) +-) | sort -u > actual +-sort -u > desired < -Subject: Correct some spelling errors -Origin: backport, https://github.com/coq/coq/commit/06cd051d140a183229cd43f0bbae152d6ad8d6ca -Reviewed-by: Benjamin Barenblat - -Lintian found some spelling errors in the Debian packaging for coq. Fix -them most places they appear in the current source. (Don't change -documentation anchor names, as that would invalidate external -deeplinks.) - -This also fixes a bug in coqdoc: prior to this commit, coqdoc would -highlight `instanciate` but not `instantiate`. ---- a/ide/nanoPG.ml -+++ b/ide/nanoPG.ml -@@ -189,7 +189,7 @@ - run "Edit" "Cut"; - { s with kill = Some(txt,false); sel = false } - else s)); -- mkE _k "k" "Kill untill the end of line" (Edit(fun s b i _ -> -+ mkE _k "k" "Kill until the end of line" (Edit(fun s b i _ -> - let already_killed = match s.kill with Some (k,true) -> k | _ -> "" in - let k = - if i#ends_line then begin ---- a/kernel/clambda.ml -+++ b/kernel/clambda.ml -@@ -767,7 +767,7 @@ - and such, which can't be done at this time. - for instance, for int31: if one of the digit is - not closed, it's not impossible that the number -- gets fully instanciated at run-time, thus to ensure -+ gets fully instantiated at run-time, thus to ensure - uniqueness of the representation in the vm - it is necessary to try and build a caml integer - during the execution *) ---- a/lib/future.ml -+++ b/lib/future.ml -@@ -49,7 +49,7 @@ - module UUIDMap = Map.Make(UUID) - module UUIDSet = Set.Make(UUID) - --type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] -+type 'a assignment = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] - - (* Val is not necessarily a final state, so the - computation restarts from the state stocked into Val *) -@@ -103,7 +103,7 @@ - let fix_exn_of ck = let _, _, fix_exn, _ = get ck in fix_exn - - let create_delegate ?(blocking=true) ~name fix_exn = -- let assignement signal ck = fun v -> -+ let assignment signal ck = fun v -> - let _, _, fix_exn, c = get ck in - assert (match !c with Delegated _ -> true | _ -> false); - begin match v with -@@ -118,7 +118,7 @@ - (fun () -> Mutex.lock lock; Condition.wait cond lock; Mutex.unlock lock), - (fun () -> Mutex.lock lock; Condition.broadcast cond; Mutex.unlock lock) in - let ck = create ~name fix_exn (Delegated wait) in -- ck, assignement signal ck -+ ck, assignment signal ck - - (* TODO: get rid of try/catch to be stackless *) - let rec compute ck : 'a value = ---- a/lib/future.mli -+++ b/lib/future.mli -@@ -70,10 +70,10 @@ - (* Run remotely, returns the function to assign. - If not blocking (the default) it raises NotReady if forced before the - delegate assigns it. *) --type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] -+type 'a assignment = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] - val create_delegate : - ?blocking:bool -> name:string -> -- fix_exn -> 'a computation * ('a assignement -> unit) -+ fix_exn -> 'a computation * ('a assignment -> unit) - - (* Given a computation that is_exn, replace it by another one *) - val replace : 'a computation -> 'a computation -> unit ---- a/plugins/funind/functional_principles_proofs.ml -+++ b/plugins/funind/functional_principles_proofs.ml -@@ -638,11 +638,11 @@ - (* observe (str "using snd tac since : " ++ CErrors.print e); *) - tac2 g - --let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = -+let instantiate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = - let args = Array.of_list (List.map mkVar args_id) in -- let instanciate_one_hyp hid = -+ let instantiate_one_hyp hid = - my_orelse -- ( (* we instanciate the hyp if possible *) -+ ( (* we instantiate the hyp if possible *) - fun g -> - let prov_hid = pf_get_new_id hid g in - let c = mkApp(mkVar hid,args) in -@@ -678,7 +678,7 @@ - tclTHENLIST - [ - tclMAP (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) hyps; -- tclMAP instanciate_one_hyp hyps; -+ tclMAP instantiate_one_hyp hyps; - (fun g -> - let all_g_hyps_id = - List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty -@@ -722,11 +722,11 @@ - tclTHENLIST [Proofview.V82.of_tactic (Simple.case t); - (fun g' -> - let g'_nb_prod = nb_prod (project g') (pf_concl g') in -- let nb_instanciate_partial = g'_nb_prod - g_nb_prod in -+ let nb_instantiate_partial = g'_nb_prod - g_nb_prod in - observe_tac "treat_new_case" - (treat_new_case - ptes_infos -- nb_instanciate_partial -+ nb_instantiate_partial - (build_proof do_finalize) - t - dyn_infos) -@@ -760,7 +760,7 @@ - nb_rec_hyps = List.length new_hyps - } - in --(* observe_tac "Lambda" *) (instanciate_hyps_with_args do_prove new_infos.rec_hyps [id]) g' -+(* observe_tac "Lambda" *) (instantiate_hyps_with_args do_prove new_infos.rec_hyps [id]) g' - (* build_proof do_finalize new_infos g' *) - ) g - | _ -> -@@ -1118,7 +1118,7 @@ - in - (full_params, (* real params *) - princ_params, (* the params of the principle which are not params of the function *) -- substl (* function instanciated with real params *) -+ substl (* function instantiated with real params *) - (List.map var_of_decl full_params) - f_body - ) -@@ -1128,7 +1128,7 @@ - let f_body = compose_lam f_ctxt_other f_body in - (princ_info.params, (* real params *) - [],(* all params are full params *) -- substl (* function instanciated with real params *) -+ substl (* function instantiated with real params *) - (List.map var_of_decl princ_info.params) - f_body - ) -@@ -1319,7 +1319,7 @@ - (* str "args := " ++ prlist_with_sep spc Ppconstr.pr_id args_id *) - - (* ); *) -- (* observe_tac "instancing" *) (instanciate_hyps_with_args prove_tac -+ (* observe_tac "instancing" *) (instantiate_hyps_with_args prove_tac - (List.rev_map id_of_decl princ_info.branches) - (List.rev args_id)) - ] -@@ -1369,7 +1369,7 @@ - do_prove - dyn_infos - in -- instanciate_hyps_with_args prove_tac -+ instantiate_hyps_with_args prove_tac - (List.rev_map id_of_decl princ_info.branches) - (List.rev args_id) - ] -@@ -1726,8 +1726,8 @@ - ptes_info - (body_info rec_hyps) - in -- (* observe_tac "instanciate_hyps_with_args" *) -- (instanciate_hyps_with_args -+ (* observe_tac "instantiate_hyps_with_args" *) -+ (instantiate_hyps_with_args - make_proof - (List.map (get_name %> Nameops.Name.get_id) princ_info.branches) - (List.rev args_ids) ---- a/plugins/funind/recdef.ml -+++ b/plugins/funind/recdef.ml -@@ -1318,7 +1318,7 @@ - | None -> - try add_suffix current_proof_name "_subproof" - with e when CErrors.noncritical e -> -- anomaly (Pp.str "open_new_goal with an unamed theorem.") -+ anomaly (Pp.str "open_new_goal with an unnamed theorem.") - in - let na = next_global_ident_away name Id.Set.empty in - if Termops.occur_existential sigma gls_type then ---- a/plugins/omega/PreOmega.v -+++ b/plugins/omega/PreOmega.v -@@ -181,7 +181,7 @@ - let t := eval compute in (Z.of_nat (S a)) in - change (Z.of_nat (S a)) with t in H - | _ => rewrite (Nat2Z.inj_succ a) in H -- | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]), -+ | _ => (* if the [rewrite] fails (most likely a dependent occurrence of [Z.of_nat (S a)]), - hide [Z.of_nat (S a)] in this one hypothesis *) - change (Z.of_nat (S a)) with (Z_of_nat' (S a)) in H - end -@@ -192,7 +192,7 @@ - let t := eval compute in (Z.of_nat (S a)) in - change (Z.of_nat (S a)) with t - | _ => rewrite (Nat2Z.inj_succ a) -- | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]), -+ | _ => (* if the [rewrite] fails (most likely a dependent occurrence of [Z.of_nat (S a)]), - hide [Z.of_nat (S a)] in the goal *) - change (Z.of_nat (S a)) with (Z_of_nat' (S a)) - end ---- a/plugins/omega/omega.ml -+++ b/plugins/omega/omega.ml -@@ -178,7 +178,7 @@ - | DIVIDE_AND_APPROX (e1,e2,k,d) -> - Printf.printf - "Inequation E%d is divided by %s and the constant coefficient is \ -- rounded by substracting %s.\n" e1.id (sbi k) (sbi d) -+ rounded by subtracting %s.\n" e1.id (sbi k) (sbi d) - | NOT_EXACT_DIVIDE (e,k) -> - Printf.printf - "Constant in equation E%d is not divisible by the pgcd \ ---- a/stm/stm.ml -+++ b/stm/stm.ml -@@ -1343,7 +1343,7 @@ - t_stop : Stateid.t; - t_drop : bool; - t_states : competence; -- t_assign : Proof_global.closed_proof_output Future.assignement -> unit; -+ t_assign : Proof_global.closed_proof_output Future.assignment -> unit; - t_loc : Loc.t option; - t_uuid : Future.UUID.t; - t_name : string } -@@ -1381,7 +1381,7 @@ - t_stop : Stateid.t; - t_drop : bool; - t_states : competence; -- t_assign : Proof_global.closed_proof_output Future.assignement -> unit; -+ t_assign : Proof_global.closed_proof_output Future.assignment -> unit; - t_loc : Loc.t option; - t_uuid : Future.UUID.t; - t_name : string } -@@ -1819,7 +1819,7 @@ - type task = { - t_state : Stateid.t; - t_state_fb : Stateid.t; -- t_assign : output Future.assignement -> unit; -+ t_assign : output Future.assignment -> unit; - t_ast : int * aast; - t_goal : Goal.goal; - t_kill : unit -> unit; -@@ -1836,7 +1836,7 @@ - type task = { - t_state : Stateid.t; - t_state_fb : Stateid.t; -- t_assign : output Future.assignement -> unit; -+ t_assign : output Future.assignment -> unit; - t_ast : int * aast; - t_goal : Goal.goal; - t_kill : unit -> unit; ---- a/test-suite/success/univers.v -+++ b/test-suite/success/univers.v -@@ -60,7 +60,7 @@ - - Record U : Type := { A:=Type; a:A }. - --(** Check assignement of sorts to inductives and records. *) -+(** Check assignment of sorts to inductives and records. *) - - Variable sh : list nat. - ---- a/tools/coq_makefile.ml -+++ b/tools/coq_makefile.ml -@@ -59,7 +59,7 @@ - \n _-extra-phony foo bar \"\"_ is a regular way to add the target \"bar\" as\ - \n as a dependencies of an already defined target \"foo\".\ - \n[-I dir]: look for Objective Caml dependencies in \"dir\"\ --\n[-R physicalpath logicalpath]: look for Coq dependencies resursively\ -+\n[-R physicalpath logicalpath]: look for Coq dependencies recursively\ - \n starting from \"physicalpath\". The logical path associated to the\ - \n physical path is \"logicalpath\".\ - \n[-Q physicalpath logicalpath]: look for Coq dependencies starting from\ ---- a/tools/coqdoc/output.ml -+++ b/tools/coqdoc/output.ml -@@ -76,7 +76,7 @@ - [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection"; - "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor"; - "econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct"; -- "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate"; "info_auto"; "info_eauto"; -+ "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instantiate"; "info_auto"; "info_eauto"; - "quote"; "eexact"; "autorewrite"; - "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality"; - "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega"; ---- a/tools/coqworkmgr.ml -+++ b/tools/coqworkmgr.ml -@@ -169,7 +169,7 @@ - "-j",Arg.Set_int max_tokens, "max number of concurrent jobs"; - "-d",Arg.Set debug, "do not detach (debug)"] in - let usage = -- "Prints on stdout an env variable assignement to be picked up by coq\n"^ -+ "Prints on stdout an env variable assignment to be picked up by coq\n"^ - "instances in order to limit the maximum number of concurrent workers.\n"^ - "The default value is 2.\n"^ - "Usage:" in ---- a/vernac/comProgramFixpoint.ml -+++ b/vernac/comProgramFixpoint.ml -@@ -254,7 +254,7 @@ - interp_recursive ~cofix ~program_mode:true fixl ntns - in - (* Program-specific code *) -- (* Get the interesting evars, those that were not instanciated *) -+ (* Get the interesting evars, those that were not instantiated *) - let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in - (* Solve remaining evars *) - let evd = nf_evar_map_undefined evd in ---- a/vernac/obligations.ml -+++ b/vernac/obligations.ml -@@ -338,7 +338,7 @@ - let _ = - declare_bool_option - { optdepr = false; -- optname = "Hidding of Program obligations"; -+ optname = "Hiding of Program obligations"; - optkey = ["Hide";"Obligations"]; - optread = get_hide_obligations; - optwrite = set_hide_obligations; } -- cgit v1.2.3