diff options
31 files changed, 218 insertions, 72 deletions
diff --git a/.gitattributes b/.gitattributes index 00f78b4494..f2c096f2d6 100644 --- a/.gitattributes +++ b/.gitattributes @@ -1,3 +1,36 @@ .gitattributes export-ignore .gitignore export-ignore .mailmap export-ignore + +*.asciidoc whitespace=trailing-space,tab-in-indent +*.bat whitespace=cr-at-eol,trailing-space,tab-in-indent +*.bib whitespace=trailing-space,tab-in-indent +*.c whitespace=trailing-space,tab-in-indent +*.css whitespace=trailing-space,tab-in-indent +*.dtd whitespace=trailing-space,tab-in-indent +*.el whitespace=trailing-space,tab-in-indent +*.h whitespace=trailing-space,tab-in-indent +*.html whitespace=trailing-space,tab-in-indent +*.hva whitespace=trailing-space,tab-in-indent +*.js whitespace=trailing-space,tab-in-indent +*.json whitespace=trailing-space,tab-in-indent +*.lang whitespace=trailing-space,tab-in-indent +*.md whitespace=trailing-space,tab-in-indent +*.merlin whitespace=trailing-space,tab-in-indent +*.ml whitespace=trailing-space,tab-in-indent +*.ml4 whitespace=trailing-space,tab-in-indent +*.mli whitespace=trailing-space,tab-in-indent +*.mll whitespace=trailing-space,tab-in-indent +*.mllib whitespace=trailing-space,tab-in-indent +*.mlp whitespace=trailing-space,tab-in-indent +*.mlpack whitespace=trailing-space,tab-in-indent +*.nsh whitespace=trailing-space,tab-in-indent +*.nsi whitespace=trailing-space,tab-in-indent +*.py whitespace=trailing-space,tab-in-indent +*.sh whitespace=trailing-space,tab-in-indent +*.sty whitespace=trailing-space,tab-in-indent +*.tex whitespace=trailing-space,tab-in-indent +*.txt whitespace=trailing-space,tab-in-indent +*.v whitespace=trailing-space,tab-in-indent +*.xml whitespace=trailing-space,tab-in-indent +*.yml whitespace=trailing-space,tab-in-indent @@ -55,6 +55,7 @@ Tom Hutchinson <thutchin@gforge> thutchin <thutchin@85f007b7-5 Cezary Kaliszyk <cek@gforge> cek <cek@85f007b7-540e-0410-9357-904b9bb8a0f7> Florent Kirchner <fkirchne@gforge> fkirchne <fkirchne@85f007b7-540e-0410-9357-904b9bb8a0f7> Florent Kirchner <fkirchne@gforge> kirchner <kirchner@85f007b7-540e-0410-9357-904b9bb8a0f7> +Johannes Kloos <jkloos@mpi-sws.org> jkloos <jkloos@mpi-sws.org> Matej Košík <matej.kosik@inria.fr> Matej Kosik <m4tej.kosik@gmail.com> Matej Košík <matej.kosik@inria.fr> Matej Kosik <matej.kosik@inria.fr> Marc Lasson <marc.lasson@gmail.com> mlasson <marc.lasson@gmail.com> diff --git a/.travis.yml b/.travis.yml index b71f4cc851..3b90f7cf47 100644 --- a/.travis.yml +++ b/.travis.yml @@ -66,6 +66,17 @@ env: matrix: include: + - env: + - TEST_TARGET="lint" + install: [] + before_script: [] + addons: + apt: + sources: [] + packages: [] + script: + - dev/lint-repository.sh + # Full Coq test-suite with two compilers - env: - TEST_TARGET="test-suite" diff --git a/API/API.mli b/API/API.mli index 589745b616..ccb71179dd 100644 --- a/API/API.mli +++ b/API/API.mli @@ -5831,7 +5831,7 @@ module Vernacinterp : sig type deprecation = bool - type vernac_command = Genarg.raw_generic_argument list -> unit -> unit + type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit val vinterp_add : deprecation -> Vernacexpr.extend_name -> vernac_command -> unit diff --git a/dev/build/windows/MakeCoq_regtest_noproxy.bat b/dev/build/windows/MakeCoq_regtest_noproxy.bat index 7b17e721b3..7140a7c619 100644 --- a/dev/build/windows/MakeCoq_regtest_noproxy.bat +++ b/dev/build/windows/MakeCoq_regtest_noproxy.bat @@ -25,5 +25,5 @@ call MakeCoq_MinGW.bat ^ -cygquiet=Y ^
-destcyg %ROOTPATH%\cygwin_coq64_85pl2_abs ^
-destcoq %ROOTPATH%\coq64_85pl2_abs
- -pause
\ No newline at end of file +
+pause
diff --git a/dev/build/windows/configure_profile.sh b/dev/build/windows/configure_profile.sh index 0b61a31e7f..16c972e80c 100644 --- a/dev/build/windows/configure_profile.sh +++ b/dev/build/windows/configure_profile.sh @@ -40,4 +40,4 @@ if [ ! -f $donefile ] ; then echo unset OCAMLLIB >> $rcfile touch $donefile -fi
\ No newline at end of file +fi diff --git a/dev/build/windows/patches_coq/ln.c b/dev/build/windows/patches_coq/ln.c index 5e02c72bb7..41f64f98b2 100644 --- a/dev/build/windows/patches_coq/ln.c +++ b/dev/build/windows/patches_coq/ln.c @@ -134,4 +134,4 @@ int WINAPI WinMain( HINSTANCE hInstance, HINSTANCE hPrevInstance, LPSTR lpCmdLin // Everything is fine return 0; -}
\ No newline at end of file +} diff --git a/dev/lint-commits.sh b/dev/lint-commits.sh new file mode 100755 index 0000000000..eb12bc2273 --- /dev/null +++ b/dev/lint-commits.sh @@ -0,0 +1,32 @@ +#!/usr/bin/env bash + +# A script to check prettyness for a range of commits + +CALLNAME="$0" + +function usage +{ + >&2 echo "usage: $CALLNAME <commit> <commit>" + >&2 echo "The order of commits is as given to 'git diff'" +} + +if [ "$#" != 2 ]; +then + usage + exit 1 +fi + +BASE_COMMIT="$1" +HEAD_COMMIT="$2" + +# git diff --check +# uses .gitattributes to know what to check +if git diff --check "$BASE_COMMIT" "$HEAD_COMMIT"; +then + : +else + >&2 echo "Whitespace errors!" + >&2 echo "Running 'git diff --check $BASE_COMMIT $HEAD_COMMIT'." + >&2 echo "If you use emacs, you can prevent this kind of error from reocurring by installing ws-butler and enabling ws-butler-convert-leading-tabs-or-spaces." + exit 1 +fi diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh new file mode 100755 index 0000000000..ecf7880e20 --- /dev/null +++ b/dev/lint-repository.sh @@ -0,0 +1,28 @@ +#!/usr/bin/env bash + +# A script to check prettyness over the repository. + +# lint-commits.sh seeks to prevent the worsening of already present +# problems, such as tab indentation in ml files. lint-repository.sh +# seeks to prevent the (re-)introduction of solved problems, such as +# newlines at the end of .v files. + +CODE=0 + +if [ "(" "-n" "${TRAVIS_PULL_REQUEST}" ")" "-a" "(" "${TRAVIS_PULL_REQUEST}" "!=" "false" ")" ]; +then + # Some problems are too widespread to fix in one commit, but we + # can still check that they don't worsen. + CUR_HEAD=${TRAVIS_COMMIT_RANGE%%...*} + PR_HEAD=${TRAVIS_COMMIT_RANGE##*...} + MERGE_BASE=$(git merge-base $CUR_HEAD $PR_HEAD) + dev/lint-commits.sh $MERGE_BASE $PR_HEAD || CODE=1 +fi + +# Check that the files with 'whitespace' gitattribute end in a newline. +# xargs exit status is 123 if any file failed the test +find . "(" -path ./.git -prune ")" -type f \ +-o "(" -exec dev/tools/should-check-whitespace.sh '{}' ';' ")" \ +-print0 | xargs -0 -L 1 dev/tools/check-eof-newline.sh || CODE=1 + +exit $CODE diff --git a/dev/nsis/FileAssociation.nsh b/dev/nsis/FileAssociation.nsh index b8c1e5ee78..71a9162efc 100644 --- a/dev/nsis/FileAssociation.nsh +++ b/dev/nsis/FileAssociation.nsh @@ -187,4 +187,4 @@ NoOwn: !verbose pop !macroend -!endif # !FileAssociation_INCLUDED
\ No newline at end of file +!endif # !FileAssociation_INCLUDED diff --git a/dev/tools/check-eof-newline.sh b/dev/tools/check-eof-newline.sh new file mode 100755 index 0000000000..1c578c05ce --- /dev/null +++ b/dev/tools/check-eof-newline.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash + +if [ -z "$(tail -c 1 "$1")" ] +then + exit 0 +else + echo "No newline at end of file $1!" + exit 1 +fi diff --git a/dev/tools/should-check-whitespace.sh b/dev/tools/should-check-whitespace.sh new file mode 100755 index 0000000000..8159506b41 --- /dev/null +++ b/dev/tools/should-check-whitespace.sh @@ -0,0 +1,5 @@ +#!/usr/bin/env bash + +# determine if a file has whitespace checking enabled in .gitattributes + +git check-attr whitespace -- "$1" | grep -q -v 'unspecified$' diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 70f7c4283f..35956477df 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -503,7 +503,7 @@ let _ = (function [c] when genarg_tag c = unquote (topwit wit_constr) && true -> let c = out_gen (rawwit wit_constr) c in - (fun () -> in_current_context constr_display c) + (fun _ -> in_current_context constr_display c) | _ -> failwith "Vernac extension: cannot occur") with e -> pp (CErrors.print e) @@ -519,7 +519,7 @@ let _ = (function [c] when genarg_tag c = unquote (topwit wit_constr) && true -> let c = out_gen (rawwit wit_constr) c in - (fun () -> in_current_context print_pure_constr c) + (fun _ -> in_current_context print_pure_constr c) | _ -> failwith "Vernac extension: cannot occur") with e -> pp (CErrors.print e) diff --git a/doc/common/styles/html/simple/style.css b/doc/common/styles/html/simple/style.css index 0b1e640b38..d1b2ce1112 100644 --- a/doc/common/styles/html/simple/style.css +++ b/doc/common/styles/html/simple/style.css @@ -10,4 +10,4 @@ margin: 0pt; padding: .5ex 1em; list-style: none -}
\ No newline at end of file +} diff --git a/doc/refman/index.html b/doc/refman/index.html index 9b5250abcb..b937350e6e 100644 --- a/doc/refman/index.html +++ b/doc/refman/index.html @@ -11,4 +11,4 @@ <FRAME SRC="menu.html"> </FRAMESET> -</HTML>
\ No newline at end of file +</HTML> diff --git a/engine/namegen.ml b/engine/namegen.ml index a38c73ed0b..c548fc4ac9 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -132,8 +132,8 @@ let hdchar env sigma c = | Cast (c,_,_) | App (c,_) -> hdrec k c | Proj (kn,_) -> lowercase_first_char (Label.to_id (con_label (Projection.constant kn))) | Const (kn,_) -> lowercase_first_char (Label.to_id (con_label kn)) - | Ind (x,_) -> lowercase_first_char (basename_of_global (IndRef x)) - | Construct (x,_) -> lowercase_first_char (basename_of_global (ConstructRef x)) + | Ind (x,_) -> (try lowercase_first_char (basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz") + | Construct (x,_) -> (try lowercase_first_char (basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz") | Var id -> lowercase_first_char id | Sort s -> sort_hdchar (ESorts.kind sigma s) | Rel n -> diff --git a/engine/termops.ml b/engine/termops.ml index b7fa2dc4a4..76f707f945 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -327,11 +327,11 @@ let pr_evar_constraints sigma pbs = Namegen.make_all_name_different env sigma in print_env_short env ++ spc () ++ str "|-" ++ spc () ++ - print_constr_env env sigma (EConstr.of_constr t1) ++ spc () ++ + protect (print_constr_env env sigma) (EConstr.of_constr t1) ++ spc () ++ str (match pbty with | Reduction.CONV -> "==" | Reduction.CUMUL -> "<=") ++ - spc () ++ print_constr_env env Evd.empty (EConstr.of_constr t2) + spc () ++ protect (print_constr_env env Evd.empty) (EConstr.of_constr t2) in prlist_with_sep fnl pr_evconstr pbs @@ -358,37 +358,37 @@ let pr_evar_list sigma l = h 0 (str (string_of_existential ev) ++ str "==" ++ pr_evar_info evi ++ (if evi.evar_body == Evar_empty - then str " {" ++ pr_existential_key sigma ev ++ str "}" + then str " {" ++ pr_existential_key sigma ev ++ str "}" else mt ())) in h 0 (prlist_with_sep fnl pr l) -let pr_evar_by_depth depth sigma = match depth with -| None -> - (* Print all evars *) - let to_list d = - let open Evd in - (* Workaround for change in Map.fold behavior in ocaml 3.08.4 *) - let l = ref [] in - let fold_def evk evi () = match evi.evar_body with +let to_list d = + let open Evd in + (* Workaround for change in Map.fold behavior in ocaml 3.08.4 *) + let l = ref [] in + let fold_def evk evi () = match evi.evar_body with | Evar_defined _ -> l := (evk, evi) :: !l | Evar_empty -> () - in - let fold_undef evk evi () = match evi.evar_body with + in + let fold_undef evk evi () = match evi.evar_body with | Evar_empty -> l := (evk, evi) :: !l | Evar_defined _ -> () - in - Evd.fold fold_def d (); - Evd.fold fold_undef d (); - !l in - str"EVARS:"++brk(0,1)++pr_evar_list sigma (to_list sigma)++fnl() -| Some n -> + Evd.fold fold_def d (); + Evd.fold fold_undef d (); + !l + +let pr_evar_by_depth depth sigma = match depth with +| None -> (* Print all evars *) + str"EVARS:" ++ brk(0,1) ++ pr_evar_list sigma (to_list sigma) ++ fnl() +| Some n -> + (* Print closure of undefined evars *) str"UNDEFINED EVARS:"++ (if Int.equal n 0 then mt() else str" (+level "++int n++str" closure):")++ brk(0,1)++ - pr_evar_list sigma (evar_dependency_closure n sigma)++fnl() + pr_evar_list sigma (evar_dependency_closure n sigma) ++ fnl() let pr_evar_by_filter filter sigma = let open Evd in diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index a529185dd6..874712124c 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -59,7 +59,7 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } = | None, Some cg -> (make_patt pt, ploc_vala None, - <:expr< fun () -> $cg$ $str:s$ >>) + <:expr< fun loc -> $cg$ $str:s$ >>) | None, None -> prerr_endline (("Vernac entry \""^s^"\" misses a classifier. "^ "A classifier is a function that returns an expression "^ @@ -82,7 +82,7 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } = "classifiers. Only one classifier is called.") ^ "\n"); (make_patt pt, ploc_vala None, - <:expr< fun () -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>) + <:expr< fun loc -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>) let make_fun_clauses loc s l = let map c = @@ -165,16 +165,16 @@ EXTEND [ [ "["; s = STRING; l = LIST0 args; "]"; d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> let () = if s = "" then failwith "Command name is empty." in - let b = <:expr< fun () -> $e$ >> in + let b = <:expr< fun loc -> $e$ >> in { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; } | "[" ; "-" ; l = LIST1 args ; "]" ; d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> - let b = <:expr< fun () -> $e$ >> in + let b = <:expr< fun loc -> $e$ >> in { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; } ] ] ; classifier: - [ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< fun () -> $c$>> ] ] + [ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< fun loc -> $c$>> ] ] ; args: [ [ e = LIDENT; "("; s = LIDENT; ")" -> diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index ea412a7d6a..9aef4b1312 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -39,7 +39,6 @@ type goal_reference = | OpenSubgoals | NthGoal of int | GoalId of Id.t - | GoalUid of goal_identifier type printable = | PrintTables diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index e88d8f89d5..b906c3b597 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -842,12 +842,22 @@ let rec find_solution_type evarenv = function | (id,ProjectEvar _)::l -> find_solution_type evarenv l | [] -> assert false -let find_most_recent_projection evi sols = +let is_preferred_projection_over sign (id,p) (id',p') = + (* We give priority to projection of variables over instantiation of + an evar considering that the latter is a stronger decision which + may even procude an incorrect (ill-typed) solution *) + match p, p' with + | ProjectEvar _, ProjectVar -> false + | ProjectVar, ProjectEvar _ -> true + | _, _ -> + List.index Id.equal id sign < List.index Id.equal id' sign + +let choose_projection evi sols = let sign = List.map get_id (evar_filtered_context evi) in match sols with | y::l -> List.fold_right (fun (id,p as x) (id',_ as y) -> - if List.index Id.equal id sign < List.index Id.equal id' sign then x else y) + if is_preferred_projection_over sign x y then x else y) l y | _ -> assert false @@ -1439,8 +1449,11 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = | [] -> raise Not_found | [id,p] -> (mkVar id, p) | _ -> - let (id,p) = find_most_recent_projection evi sols in - if choose then (mkVar id, p) else raise (NotUniqueInType sols) + if choose then + let (id,p) = choose_projection evi sols in + (mkVar id, p) + else + raise (NotUniqueInType sols) in let ty = lazy (Retyping.get_type_of env !evdref (of_alias t)) in let evd = do_projection_effects (evar_define conv_algo ~choose) env ty !evdref p in diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index d1158b3d6f..143f9ddcc5 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -574,7 +574,7 @@ open Decl_kinds | OpenSubgoals -> mt () | NthGoal n -> spc () ++ int n | GoalId id -> spc () ++ pr_id id - | GoalUid n -> spc () ++ str n in + in let pr_showable = function | ShowGoal n -> keyword "Show" ++ pr_goal_reference n | ShowProof -> keyword "Show Proof" diff --git a/printing/printer.ml b/printing/printer.ml index c6650ea3b8..70e96722d6 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -838,17 +838,6 @@ let pr_goal_by_id id = pr_selected_subgoal (pr_id id) sigma g) with Not_found -> user_err Pp.(str "No such goal.") -let pr_goal_by_uid uid = - let p = Proof_global.give_me_the_proof () in - let g = Goal.get_by_uid uid in - let pr gs = - v 0 (str "goal / evar " ++ str uid ++ str " is:" ++ cut () - ++ pr_goal gs) - in - try - Proof.in_proof p (fun sigma -> pr {it=g;sigma=sigma;}) - with Not_found -> user_err Pp.(str "Invalid goal identifier.") - (* Elementary tactics *) let pr_prim_rule = function diff --git a/printing/printer.mli b/printing/printer.mli index 658ea6060b..f55206f0df 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -201,7 +201,6 @@ val pr_assumptionset : env -> Term.types ContextObjectMap.t -> Pp.t val pr_goal_by_id : Id.t -> Pp.t -val pr_goal_by_uid : string -> Pp.t type printer_pr = { pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t; diff --git a/proofs/goal.ml b/proofs/goal.ml index 7d830146f9..61f3e4a029 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -21,7 +21,6 @@ type goal = Evd.evar let pr_goal e = str "GOAL:" ++ Pp.int (Evar.repr e) let uid e = string_of_int (Evar.repr e) -let get_by_uid u = Evar.unsafe_of_int (int_of_string u) (* Layer to implement v8.2 tactic engine ontop of the new architecture. Types are different from what they used to be due to a change of the diff --git a/proofs/goal.mli b/proofs/goal.mli index 6d3ec8bd4e..ad968cdfb3 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -15,9 +15,6 @@ type goal = Evar.t (* Gives a unique identifier to each goal. The identifier is guaranteed to contain no space. *) val uid : goal -> string -(* Returns the goal (even if it has been partially solved) - corresponding to a unique identifier obtained by {!uid}. *) -val get_by_uid : string -> goal (* Debugging help *) val pr_goal : goal -> Pp.t diff --git a/test-suite/bugs/closed/5245.v b/test-suite/bugs/closed/5245.v index 77bf169e18..e5bca5b5e4 100644 --- a/test-suite/bugs/closed/5245.v +++ b/test-suite/bugs/closed/5245.v @@ -15,4 +15,4 @@ Undo. progress hnf; intros; exact eq_refl. Undo. unfold foo_rel. intros x. exact eq_refl. -Qed.
\ No newline at end of file +Qed. diff --git a/test-suite/bugs/closed/6070.v b/test-suite/bugs/closed/6070.v new file mode 100644 index 0000000000..49b16f6254 --- /dev/null +++ b/test-suite/bugs/closed/6070.v @@ -0,0 +1,32 @@ +(* A slight shortening of bug 6078 *) + +(* This bug exposed a different behavior of unshelve_unifiable + depending on which projection is found in the unification + heuristics *) + +Axiom flat_type : Type. +Axiom interp_flat_type : flat_type -> Type. +Inductive type := Arrow (_ _ : flat_type). +Definition interp_type (t : type) + := interp_flat_type (match t with Arrow s d => s end) + -> interp_flat_type (match t with Arrow s d => d end). +Axiom Expr : type -> Type. +Axiom Interp : forall {t : type}, Expr t -> interp_type t. +Axiom Wf : forall {t}, Expr t -> Prop. +Axiom a : forall f, interp_flat_type f. + +Definition packaged_expr_functionP A := + (fun F : Expr A -> Expr A + => forall e' v, Interp (F e') v = a (let (_,f) := A in f)). +Goal forall (f f0 : flat_type) + (e : forall _ : Expr (@Arrow f f0), + Expr (@Arrow f f0)), + @packaged_expr_functionP (@Arrow f f0) e. + intros. + refine (fun (e0 : Expr (Arrow f f0)) + => (fun zHwf':True => + (fun v : interp_flat_type f => + ?[G] : ?[U] = ?[V] :> interp_flat_type ?[v])) ?[H]); + [ | ]. + (* Was: Error: Tactic failure: Incorrect number of goals (expected 3 tactics). *) +Abort. diff --git a/test-suite/success/guard.v b/test-suite/success/guard.v index 83d47dc683..3a1c6dabeb 100644 --- a/test-suite/success/guard.v +++ b/test-suite/success/guard.v @@ -25,4 +25,4 @@ match f with match e in (_ = B) return (B -> foo A) -> nat with | eq_refl => fun (g' : nat -> foo A) => bar A e (g' O) end g -end e.
\ No newline at end of file +end e. diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e08cb83871..41f63644d4 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1853,7 +1853,6 @@ let vernac_show = let open Feedback in function | OpenSubgoals -> pr_open_subgoals () | NthGoal n -> pr_nth_open_subgoal n | GoalId id -> pr_goal_by_id id - | GoalUid id -> pr_goal_by_uid id in msg_notice info | ShowProof -> show_proof () @@ -2070,7 +2069,7 @@ let interp ?proof ?loc locality poly c = | VernacProofMode mn -> Proof_global.set_proof_mode mn [@ocaml.warning "-3"] (* Extensions *) - | VernacExtend (opn,args) -> Vernacinterp.call ?locality (opn,args) + | VernacExtend (opn,args) -> Vernacinterp.call ?locality ?loc (opn,args) (* Vernaculars that take a locality flag *) let check_vernac_supports_locality c l = diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 2d9c0fa362..41fee6bd08 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -11,7 +11,7 @@ open Pp open CErrors type deprecation = bool -type vernac_command = Genarg.raw_generic_argument list -> unit -> unit +type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit (* Table of vernac entries *) let vernac_tab = @@ -49,8 +49,8 @@ let warn_deprecated_command = (* Interpretation of a vernac command *) -let call ?locality (opn,converted_args) = - let loc = ref "Looking up command" in +let call ?locality ?loc (opn,converted_args) = + let phase = ref "Looking up command" in try let depr, callback = vinterp_map opn in let () = if depr then @@ -62,16 +62,16 @@ let call ?locality (opn,converted_args) = let pr = pr_sequence pr_gram rules in warn_deprecated_command pr; in - loc:= "Checking arguments"; + phase := "Checking arguments"; let hunk = callback converted_args in - loc:= "Executing command"; + phase := "Executing command"; Locality.LocalityFixme.set locality; - hunk(); + hunk loc; Locality.LocalityFixme.assert_consumed() with | Drop -> raise Drop | reraise -> let reraise = CErrors.push reraise in if !Flags.debug then - Feedback.msg_debug (str"Vernac Interpreter " ++ str !loc); + Feedback.msg_debug (str"Vernac Interpreter " ++ str !phase); iraise reraise diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli index f58d070864..84370fdc29 100644 --- a/vernac/vernacinterp.mli +++ b/vernac/vernacinterp.mli @@ -9,7 +9,7 @@ (** Interpretation of extended vernac phrases. *) type deprecation = bool -type vernac_command = Genarg.raw_generic_argument list -> unit -> unit +type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit val vinterp_add : deprecation -> Vernacexpr.extend_name -> vernac_command -> unit @@ -17,4 +17,4 @@ val overwriting_vinterp_add : Vernacexpr.extend_name -> vernac_command -> unit val vinterp_init : unit -> unit -val call : ?locality:bool -> Vernacexpr.extend_name * Genarg.raw_generic_argument list -> unit +val call : ?locality:bool -> ?loc:Loc.t -> Vernacexpr.extend_name * Genarg.raw_generic_argument list -> unit |