diff options
37 files changed, 340 insertions, 109 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 8d0bcd1ee6..6a6318f97a 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,27 +1,35 @@ ## Changes between Coq 8.12 and Coq 8.13 -- Tactic language: TacGeneric now takes an argument to tell if it - comes from a notation. Use `None` if not and `Some foo` to tell to - print such TacGeneric surrounded with `foo:( )`. - ### Code formatting - The automatic code formatting tool `ocamlformat` has been disabled and its git hook removed. If desired, automatic formatting can be achieved by calling the `fmt` target of the dune build system. -### Pp library +### ML API + +Abstract syntax of tactic: + +- TacGeneric now takes an argument to tell if it comes from a + notation. Use `None` if not and `Some foo` to tell to print such + TacGeneric surrounded with `foo:( )`. + +Printing functions: - `Pp.h` does not take a `int` argument anymore (the argument was not used). In general, where `h n` for `n` non zero was used, `hv n` was instead intended. If cancelling the breaking role of cuts in the box was intended, turn `h n c` into `h c`. -### Grammar entries +Grammar entries: - `Prim.pattern_identref` is deprecated, use `Prim.pattern_ident` which now returns a located identifier. +Generic arguments: + +- Generic arguments: `wit_var` is deprecated, use `wit_hyp`. + ## Changes between Coq 8.11 and Coq 8.12 ### Code formatting diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index f722ddda79..edd93f2266 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -878,6 +878,11 @@ Controlling the effect of proof editing commands proved before starting the previous proof) and Coq will switch back to the proof of the previous assertion. +.. flag:: Printing Goal Names + + When turned on, the name of the goal is printed in interactive + proof mode, which can be useful in cases of cross references + between goals. Controlling memory usage ------------------------ diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 343f85be03..70be55f843 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -40,8 +40,10 @@ let wit_int_or_var = let wit_ident = make0 "ident" -let wit_var = - make0 ~dyn:(val_tag (topwit wit_ident)) "var" +let wit_hyp = + make0 ~dyn:(val_tag (topwit wit_ident)) "hyp" + +let wit_var = wit_hyp let wit_ref = make0 "ref" diff --git a/interp/stdarg.mli b/interp/stdarg.mli index 3ae8b7d73f..bd34af5543 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -37,7 +37,10 @@ val wit_int_or_var : (int or_var, int or_var, int) genarg_type val wit_ident : Id.t uniform_genarg_type +val wit_hyp : (lident, lident, Id.t) genarg_type + val wit_var : (lident, lident, Id.t) genarg_type +[@@ocaml.deprecated "Use Stdarg.wit_hyp"] val wit_ref : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg index 8069f049fd..1701830cd2 100644 --- a/parsing/g_prim.mlg +++ b/parsing/g_prim.mlg @@ -45,7 +45,7 @@ let test_minus_nat = GRAMMAR EXTEND Gram GLOBAL: - bignat bigint natural integer identref name ident var preident + bignat bigint natural integer identref name ident hyp preident fullyqualid qualid reference dirpath ne_lstring ne_string string lstring pattern_ident by_notation smart_global bar_cbrace strategy_level; @@ -58,12 +58,12 @@ GRAMMAR EXTEND Gram pattern_ident: [ [ LEFTQMARK; id = ident -> { CAst.make ~loc id } ] ] ; - var: (* as identref, but interpret as a term identifier in ltac *) - [ [ id = ident -> { CAst.make ~loc id } ] ] - ; identref: [ [ id = ident -> { CAst.make ~loc id } ] ] ; + hyp: (* as identref, but interpreted as an hypothesis in tactic notations *) + [ [ id = identref -> { id } ] ] + ; field: [ [ s = FIELD -> { Id.of_string s } ] ] ; diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index fa7de40a30..996aa0925c 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -279,7 +279,8 @@ module Prim = let strategy_level = Entry.create "strategy_level" (* parsed like ident but interpreted as a term *) - let var = Entry.create "var" + let hyp = Entry.create "hyp" + let var = hyp let name = Entry.create "name" let identref = Entry.create "identref" @@ -504,7 +505,7 @@ let () = Grammar.register0 wit_string (Prim.string); Grammar.register0 wit_pre_ident (Prim.preident); Grammar.register0 wit_ident (Prim.ident); - Grammar.register0 wit_var (Prim.var); + Grammar.register0 wit_hyp (Prim.hyp); Grammar.register0 wit_ref (Prim.reference); Grammar.register0 wit_smart_global (Prim.smart_global); Grammar.register0 wit_sort_family (Constr.sort_family); diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index fa223367f7..8e60bbf504 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -173,7 +173,8 @@ module Prim : val dirpath : DirPath.t Entry.t val ne_string : string Entry.t val ne_lstring : lstring Entry.t - val var : lident Entry.t + val hyp : lident Entry.t + val var : lident Entry.t [@@ocaml.deprecated "Use Prim.hyp"] val bar_cbrace : unit Entry.t val strategy_level : Conv_oracle.level Entry.t end diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg index f1f538ab39..b7ac71181a 100644 --- a/plugins/ltac/coretactics.mlg +++ b/plugins/ltac/coretactics.mlg @@ -20,8 +20,6 @@ open Tacarg open Names open Logic -let wit_hyp = wit_var - } DECLARE PLUGIN "ltac_plugin" diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index 863c4d37d8..ad4374dba3 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -47,7 +47,7 @@ let () = let () = let register name entry = Tacentries.register_tactic_notation_entry name entry in - register "hyp" wit_var; + register "hyp" wit_hyp; register "simple_intropattern" wit_simple_intropattern; register "integer" wit_integer; register "reference" wit_ref; @@ -140,7 +140,7 @@ ARGUMENT EXTEND occurrences GLOB_PRINTED BY { pr_occurrences } | [ ne_integer_list(l) ] -> { ArgArg l } -| [ var(id) ] -> { ArgVar id } +| [ hyp(id) ] -> { ArgVar id } END { diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 4f20e5a800..a2a47c0bf4 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -33,8 +33,6 @@ open Proofview.Notations open Attributes open Vernacextend -let wit_hyp = wit_var - } DECLARE PLUGIN "ltac_plugin" @@ -450,7 +448,7 @@ END (* Subst *) TACTIC EXTEND subst -| [ "subst" ne_var_list(l) ] -> { subst l } +| [ "subst" ne_hyp_list(l) ] -> { subst l } | [ "subst" ] -> { subst_all () } END diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 2e72ceae5a..44472a1995 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -18,8 +18,6 @@ open Pcoq.Constr open Pltac open Hints -let wit_hyp = wit_var - } DECLARE PLUGIN "ltac_plugin" diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg index 0dd8939211..a86045b0a4 100644 --- a/plugins/ltac/g_class.mlg +++ b/plugins/ltac/g_class.mlg @@ -77,7 +77,7 @@ END (* true = All transparent, false = Opaque if possible *) VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF - | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) integer_opt(depth) ] -> { + | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) natural_opt(depth) ] -> { set_typeclasses_debug d; Option.iter set_typeclasses_strategy s; set_typeclasses_depth depth diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 8331927cda..ee94fd565a 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -29,8 +29,6 @@ open Pvernac.Vernac_ open Pltac open Vernacextend -let wit_hyp = wit_var - } DECLARE PLUGIN "ltac_plugin" diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index cbb53497d3..fe896f9351 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1323,7 +1323,7 @@ let () = register_basic_print0 wit_smart_global (pr_or_by_notation pr_qualid) (pr_or_var (pr_located pr_global)) pr_global; register_basic_print0 wit_ident pr_id pr_id pr_id; - register_basic_print0 wit_var pr_lident pr_lident pr_id; + register_basic_print0 wit_hyp pr_lident pr_lident pr_id; register_print0 wit_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env [@warning "-3"]; register_print0 wit_simple_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env; Genprint.register_print0 diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index f7037176d2..ee28229cb7 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -161,8 +161,8 @@ let coerce_var_to_ident fresh env sigma v = match out_gen (topwit wit_intro_pattern) v with | { CAst.v=IntroNaming (IntroIdentifier id)} -> id | _ -> fail () - else if has_type v (topwit wit_var) then - out_gen (topwit wit_var) v + else if has_type v (topwit wit_hyp) then + out_gen (topwit wit_hyp) v else match Value.to_constr v with | None -> fail () | Some c -> @@ -184,8 +184,8 @@ let id_of_name = function | Some (IntroNaming (IntroIdentifier id)) -> id | Some _ -> fail () | None -> - if has_type v (topwit wit_var) then - out_gen (topwit wit_var) v + if has_type v (topwit wit_hyp) then + out_gen (topwit wit_hyp) v else match Value.to_constr v with | None -> fail () @@ -222,8 +222,8 @@ let coerce_to_intro_pattern sigma v = match is_intro_pattern v with | Some pat -> pat | None -> - if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in + if has_type v (topwit wit_hyp) then + let id = out_gen (topwit wit_hyp) v in IntroNaming (IntroIdentifier id) else match Value.to_constr v with | Some c when isVar sigma c -> @@ -259,8 +259,8 @@ let coerce_to_constr env v = ([], c) else if has_type v (topwit wit_constr_under_binders) then out_gen (topwit wit_constr_under_binders) v - else if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in + else if has_type v (topwit wit_hyp) then + let id = out_gen (topwit wit_hyp) v in (try [], constr_of_id env id with Not_found -> fail ()) else fail () @@ -282,8 +282,8 @@ let coerce_to_evaluable_ref env sigma v = | Some (IntroNaming (IntroIdentifier id)) when is_variable env id -> EvalVarRef id | Some _ -> fail () | None -> - if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in + if has_type v (topwit wit_hyp) then + let id = out_gen (topwit wit_hyp) v in if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id else fail () else if has_type v (topwit wit_ref) then @@ -328,8 +328,8 @@ let coerce_to_hyp env sigma v = | Some (IntroNaming (IntroIdentifier id)) when is_variable env id -> id | Some _ -> fail () | None -> - if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in + if has_type v (topwit wit_hyp) then + let id = out_gen (topwit wit_hyp) v in if is_variable env id then id else fail () else match Value.to_constr v with | Some c when isVar sigma c -> destVar sigma c @@ -360,8 +360,8 @@ let coerce_to_quantified_hypothesis sigma v = | Some (IntroNaming (IntroIdentifier id)) -> NamedHyp id | Some _ -> raise (CannotCoerceTo "a quantified hypothesis") | None -> - if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in + if has_type v (topwit wit_hyp) then + let id = out_gen (topwit wit_hyp) v in NamedHyp id else if has_type v (topwit wit_int) then AnonHyp (out_gen (topwit wit_int) v) diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index f0ca813b08..d58a76fe13 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -219,7 +219,9 @@ let interp_prod_item = function | None -> if String.Map.mem s !entry_names then String.Map.find s !entry_names else begin match ArgT.name s with - | None -> user_err Pp.(str ("Unknown entry "^s^".")) + | None -> + if s = "var" then user_err Pp.(str ("var is deprecated, use hyp.")) (* to remove in 8.14 *) + else user_err Pp.(str ("Unknown entry "^s^".")) | Some arg -> arg end | Some n -> diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index dea216045e..9c3b05fdf1 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -835,7 +835,7 @@ let () = Genintern.register_intern0 wit_ref (lift intern_global_reference); Genintern.register_intern0 wit_pre_ident (fun ist c -> (ist,c)); Genintern.register_intern0 wit_ident intern_ident'; - Genintern.register_intern0 wit_var (lift intern_hyp); + Genintern.register_intern0 wit_hyp (lift intern_hyp); Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg); Genintern.register_intern0 wit_ltac (lift intern_ltac); Genintern.register_intern0 wit_quant_hyp (lift intern_quantified_hypothesis); diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index eaeae50254..12bfb4d09e 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -971,8 +971,8 @@ let interp_destruction_arg ist gl arg = match v with | {v=IntroNaming (IntroIdentifier id)} -> try_cast_id id | _ -> error () - else if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in + else if has_type v (topwit wit_hyp) then + let id = out_gen (topwit wit_hyp) v in try_cast_id id else if has_type v (topwit wit_int) then keep,ElimOnAnonHyp (out_gen (topwit wit_int) v) @@ -1238,7 +1238,7 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t = | ArgVar {loc;v=id} -> let v = try Id.Map.find id ist.lfun - with Not_found -> in_gen (topwit wit_var) id + with Not_found -> in_gen (topwit wit_hyp) id in let open Ftactic in force_vrec ist v >>= begin fun v -> @@ -1529,7 +1529,7 @@ and interp_genarg ist x : Val.t Ftactic.t = let open Ftactic.Notations in (* Ad-hoc handling of some types. *) let tag = genarg_tag x in - if argument_type_eq tag (unquote (topwit (wit_list wit_var))) then + if argument_type_eq tag (unquote (topwit (wit_list wit_hyp))) then interp_genarg_var_list ist x else if argument_type_eq tag (unquote (topwit (wit_list wit_constr))) then interp_genarg_constr_list ist x @@ -1573,9 +1573,9 @@ and interp_genarg_var_list ist x = Ftactic.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let lc = Genarg.out_gen (glbwit (wit_list wit_var)) x in + let lc = Genarg.out_gen (glbwit (wit_list wit_hyp)) x in let lc = interp_hyp_list ist env sigma lc in - let lc = in_list (val_tag wit_var) lc in + let lc = in_list (val_tag wit_hyp) lc in Ftactic.return lc end @@ -2096,7 +2096,7 @@ let () = register_interp0 wit_ref (lift interp_reference); register_interp0 wit_pre_ident (lift interp_pre_ident); register_interp0 wit_ident (lift interp_ident); - register_interp0 wit_var (lift interp_hyp); + register_interp0 wit_hyp (lift interp_hyp); register_interp0 wit_intropattern (lifts interp_intro_pattern) [@warning "-3"]; register_interp0 wit_simple_intropattern (lifts interp_intro_pattern); register_interp0 wit_clause_dft_concl (lift interp_clause); diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index fd869b225f..ec44ae4698 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -282,7 +282,7 @@ let () = Genintern.register_subst0 wit_smart_global subst_global_reference; Genintern.register_subst0 wit_pre_ident (fun _ v -> v); Genintern.register_subst0 wit_ident (fun _ v -> v); - Genintern.register_subst0 wit_var (fun _ v -> v); + Genintern.register_subst0 wit_hyp (fun _ v -> v); Genintern.register_subst0 wit_intropattern subst_intro_pattern [@warning "-3"]; Genintern.register_subst0 wit_simple_intropattern subst_intro_pattern; Genintern.register_subst0 wit_tactic subst_tactic; diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index d859fe51ab..cb58b9bcb8 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -280,7 +280,7 @@ let interp_wit wit ist gl x = sigma, Tacinterp.Value.cast (topwit wit) arg let interp_hyp ist gl (SsrHyp (loc, id)) = - let s, id' = interp_wit wit_var ist gl CAst.(make ?loc id) in + let s, id' = interp_wit wit_hyp ist gl CAst.(make ?loc id) in if not_section_id id' then s, SsrHyp (loc, id') else hyp_err ?loc "Can't clear section hypothesis " id' diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 89e0c9fcbe..7b584b5159 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -155,7 +155,7 @@ let pr_ssrhyp _ _ _ = pr_hyp let wit_ssrhyprep = add_genarg "ssrhyprep" (fun env sigma -> pr_hyp) let intern_hyp ist (SsrHyp (loc, id) as hyp) = - let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_var) CAst.(make ?loc id)) in + let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_hyp) CAst.(make ?loc id)) in if not_section_id id then hyp else hyp_err ?loc "Can't clear section hypothesis " id diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 1e8441dd8a..1dddc5622d 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -48,7 +48,7 @@ type pretype_error = | CannotUnifyBindingType of constr * constr | CannotGeneralize of constr | NoOccurrenceFound of constr * Id.t option - | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option + | CannotFindWellTypedAbstraction of constr * constr list * (env * pretype_error) option | WrongAbstractionType of Name.t * constr * types * types | AbstractionOverMeta of Name.t * Name.t | NonLinearUnification of Name.t * constr diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 45997e9a66..714d68165e 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -54,7 +54,7 @@ type pretype_error = | CannotUnifyBindingType of constr * constr | CannotGeneralize of constr | NoOccurrenceFound of constr * Id.t option - | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option + | CannotFindWellTypedAbstraction of constr * constr list * (env * pretype_error) option | WrongAbstractionType of Name.t * constr * types * types | AbstractionOverMeta of Name.t * Name.t | NonLinearUnification of Name.t * constr @@ -132,7 +132,7 @@ val error_cannot_unify : ?loc:Loc.t -> env -> Evd.evar_map -> val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -> 'b val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map -> - constr -> constr list -> (env * type_error) option -> 'b + constr -> constr list -> (env * pretype_error) option -> 'b val error_wrong_abstraction_type : env -> Evd.evar_map -> Name.t -> constr -> types -> types -> 'b diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 756ccd3438..40d3faa98c 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -220,14 +220,15 @@ let check_allowed_sort env sigma ind c p = else Sorts.relevance_of_sort_family ksort +let check_actual_type env sigma cj t = + try Evarconv.unify_leq_delay env sigma cj.uj_type t + with Evarconv.UnableToUnify (sigma,e) -> error_actual_type env sigma cj t e + let judge_of_cast env sigma cj k tj = let expected_type = tj.utj_val in - match Evarconv.unify_leq_delay env sigma cj.uj_type expected_type with - | exception Evarconv.UnableToUnify _ -> - error_actual_type_core env sigma cj expected_type; - | sigma -> - sigma, { uj_val = mkCast (cj.uj_val, k, expected_type); - uj_type = expected_type } + let sigma = check_actual_type env sigma cj expected_type in + sigma, { uj_val = mkCast (cj.uj_val, k, expected_type); + uj_type = expected_type } let check_fix env sigma pfix = let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in @@ -340,7 +341,7 @@ let judge_of_array env sigma u tj defj tyj = let sigma = Evd.set_leq_sort env sigma tyj.utj_type (Sorts.sort_of_univ (Univ.Universe.make ulev)) in - let check_one sigma j = Evarconv.unify_leq_delay env sigma j.uj_type tyj.utj_val in + let check_one sigma j = check_actual_type env sigma j tyj.utj_val in let sigma = check_one sigma defj in let sigma = Array.fold_left check_one sigma tj in let arr = EConstr.of_constr @@ type_of_array env u in @@ -391,7 +392,7 @@ let rec execute env sigma cstr = let t = mkApp (mkIndU (ci.ci_ind,univs), args) in let sigma, tj = execute env sigma t in let sigma, tj = type_judgment env sigma tj in - let sigma = Evarconv.unify_leq_delay env sigma cj.uj_type tj.utj_val in + let sigma = check_actual_type env sigma cj tj.utj_val in sigma in judge_of_case env sigma ci pj iv cj lfj @@ -492,10 +493,7 @@ and execute_array env = Array.fold_left_map (execute env) let check env sigma c t = let sigma, j = execute env sigma c in - match Evarconv.unify_leq_delay env sigma j.uj_type t with - | exception Evarconv.UnableToUnify _ -> - error_actual_type_core env sigma j t - | sigma -> sigma + check_actual_type env sigma j t (* Type of a constr *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 207a03d80f..ccfb508964 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -134,8 +134,8 @@ let abstract_list_all env evd typ c l = | Type_errors.TypeError (env',x) -> (* FIXME: plug back the typing information *) error_cannot_find_well_typed_abstraction env evd p l None - | Pretype_errors.PretypeError (env',evd,TypingError x) -> - error_cannot_find_well_typed_abstraction env evd p l (Some (env',x)) in + | Pretype_errors.PretypeError (env',evd,e) -> + error_cannot_find_well_typed_abstraction env evd p l (Some (env',e)) in evd,(p,typp) let set_occurrences_of_last_arg n = diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 4200268acc..8da1d636f0 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -234,6 +234,42 @@ let tag_var = tag Tag.variable let f (id,c) = pr_lident id ++ str ":=" ++ pr ltop c in str"@{" ++ hov 0 (prlist_with_sep pr_semicolon f (List.rev l)) ++ str"}")) + (* Assuming "{" and "}" brackets, prints + - if there is enough room + { a; b; c } + - otherwise + { + a; + b; + c + } + Alternatively, replace outer hv with h to get instead: + { a; + b; + c } + Replace the inner hv with hov to respectively get instead (if enough room): + { + a; b; + c + } + or + { a; b; + c } + *) + let pr_record left right pr = function + | [] -> str left ++ str " " ++ str right + | l -> + hv 0 ( + str left ++ + brk (1,String.length left) ++ + hv 0 (prlist_with_sep pr_semicolon pr l) ++ + brk (1,0) ++ + str right) + + let pr_record_body left right pr l = + let pr_defined_field (id, c) = hov 2 (pr_reference id ++ str" :=" ++ pr c) in + pr_record left right pr_defined_field l + let las = lapp let lpator = 0 let lpatrec = 0 @@ -242,11 +278,7 @@ let tag_var = tag Tag.variable let rec pr_patt sep inh p = let (strm,prec) = match CAst.(p.v) with | CPatRecord l -> - let pp (c, p) = - pr_reference c ++ spc() ++ str ":=" ++ pr_patt spc lpattop p - in - (if l = [] then str "{| |}" - else str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}"), lpatrec + pr_record_body "{|" "|}" (pr_patt spc lpattop) l, lpatrec | CPatAlias (p, na) -> pr_patt mt (LevelLe las) p ++ str " as " ++ pr_lname na, las @@ -287,6 +319,7 @@ let tag_var = tag Tag.variable | CPatDelimiters (k,p) -> pr_delimiters k (pr_patt mt lsimplepatt p), 1 + | CPatCast _ -> assert false in @@ -464,11 +497,6 @@ let tag_var = tag Tag.variable pr (LevelLt lapp) a ++ prlist (fun a -> spc () ++ pr_expl_args pr a) l) - let pr_record_body_gen pr l = - spc () ++ - prlist_with_sep pr_semicolon - (fun (id, c) -> pr_reference id ++ str" :=" ++ pr ltop c) l - let pr_forall n = keyword "forall" ++ pr_com_at n ++ spc () let pr_fun n = keyword "fun" ++ pr_com_at n ++ spc () @@ -568,10 +596,7 @@ let tag_var = tag Tag.variable | CApp ((None,a),l) -> return (pr_app (pr mt) a l, lapp) | CRecord l -> - return ( - hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"), - latom - ) + return (pr_record_body "{|" "|}" (pr spc ltop) l, latom) | CCases (Constr.LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[{v=([[p]],b)}]) -> return ( hv 0 ( @@ -717,7 +742,5 @@ let tag_var = tag Tag.variable let pr_cases_pattern_expr = pr_patt ltop - let pr_record_body = pr_record_body_gen pr - let pr_binders env sigma = pr_undelimited_binders spc (pr_expr env sigma ltop) diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 2850e4bfa0..02e04573f8 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -41,7 +41,8 @@ val pr_guard_annot -> recursion_order_expr option -> Pp.t -val pr_record_body : (qualid * constr_expr) list -> Pp.t +val pr_record : string -> string -> ('a -> Pp.t) -> 'a list -> Pp.t +val pr_record_body : string -> string -> ('a -> Pp.t) -> (Libnames.qualid * 'a) list -> Pp.t val pr_binders : Environ.env -> Evd.evar_map -> local_binder_expr list -> Pp.t val pr_constr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr -> Pp.t val pr_lconstr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr -> Pp.t diff --git a/printing/printer.ml b/printing/printer.ml index a1a2d9ae51..bc26caefbe 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -765,9 +765,9 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map v 0 ( int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal") ++ print_extra - ++ str (if (should_gname()) then ", subgoal 1" else "") - ++ (if should_tag() then pr_goal_tag g1 else str"") - ++ pr_goal_name sigma g1 ++ cut () ++ goals + ++ str (if pr_first && (should_gname()) && ngoals > 1 then ", subgoal 1" else "") + ++ (if pr_first && should_tag() then pr_goal_tag g1 else str"") + ++ (if pr_first then pr_goal_name sigma g1 else mt()) ++ cut () ++ goals ++ (if unfocused=[] then str "" else (cut() ++ cut() ++ str "*** Unfocused goals:" ++ cut() ++ pr_rec (List.length rest + 2) unfocused)) diff --git a/test-suite/bugs/closed/bug_12895.v b/test-suite/bugs/closed/bug_12895.v new file mode 100644 index 0000000000..53adc2981c --- /dev/null +++ b/test-suite/bugs/closed/bug_12895.v @@ -0,0 +1,20 @@ +Fixpoint bug_1 (e1 : nat) {struct e1} + : nat +with bug_2 {H_imp : nat} (e2 : nat) {struct e2} + : nat. +Proof. + - exact e1. + - exact e2. +Admitted. + +Fixpoint hbug_1 (a:bool) (e1 : nat) {struct e1} + : nat +with hbug_2 (a:nat) (e2 : nat) {struct e2} + : nat. +Proof. + - exact e1. + - exact e2. +Admitted. + +Check (hbug_1 : bool -> nat -> nat). +Check (hbug_2 : nat -> nat -> nat). diff --git a/test-suite/bugs/closed/bug_13171.v b/test-suite/bugs/closed/bug_13171.v new file mode 100644 index 0000000000..0564722729 --- /dev/null +++ b/test-suite/bugs/closed/bug_13171.v @@ -0,0 +1,10 @@ +Primitive array := #array_type. + +Goal False. +Proof. + unshelve epose (_:nat). exact_no_check true. + Fail let c := open_constr:([| n | 0 |]) in + let c := eval cbv in c in + let c := type of c in + idtac c. +Abort. diff --git a/test-suite/output/Record.out b/test-suite/output/Record.out index d45343fe60..7de1e7d559 100644 --- a/test-suite/output/Record.out +++ b/test-suite/output/Record.out @@ -30,3 +30,43 @@ fun '{| U := T; a := a; q := p |} => (T, p, a) : M -> Type * True * nat fun '{| U := T; a := a; q := p |} => (T, p, a) : M -> Type * True * nat +{| a := 0; b := 0 |} + : T +fun '{| |} => 0 + : LongModuleName.test -> nat + = {| + a := + {| + LongModuleName.long_field_name0 := 0; + LongModuleName.long_field_name1 := 1; + LongModuleName.long_field_name2 := 2; + LongModuleName.long_field_name3 := 3 + |}; + b := + fun + '{| + LongModuleName.long_field_name0 := a; + LongModuleName.long_field_name1 := b; + LongModuleName.long_field_name2 := c; + LongModuleName.long_field_name3 := d + |} => (a, b, c, d) + |} + : T + = {| + a := + {| + long_field_name0 := 0; + long_field_name1 := 1; + long_field_name2 := 2; + long_field_name3 := 3 + |}; + b := + fun + '{| + long_field_name0 := a; + long_field_name1 := b; + long_field_name2 := c; + long_field_name3 := d + |} => (a, b, c, d) + |} + : T diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v index 71a8afa131..13ea37b11e 100644 --- a/test-suite/output/Record.v +++ b/test-suite/output/Record.v @@ -33,3 +33,34 @@ Check fun x:M => let 'D T _ p := x in T. Check fun x:M => let 'D T p := x in (T,p). Check fun x:M => let 'D T a p := x in (T,p,a). Check fun x:M => let '{|U:=T;a:=a;q:=p|} := x in (T,p,a). + +Module FormattingIssue13142. + +Record T {A B} := {a:A;b:B}. + +Module LongModuleName. + Record test := { long_field_name0 : nat; + long_field_name1 : nat; + long_field_name2 : nat; + long_field_name3 : nat }. +End LongModuleName. + +Definition c := + {| LongModuleName.long_field_name0 := 0; + LongModuleName.long_field_name1 := 1; + LongModuleName.long_field_name2 := 2; + LongModuleName.long_field_name3 := 3 |}. + +Definition d := + fun '{| LongModuleName.long_field_name0 := a; + LongModuleName.long_field_name1 := b; + LongModuleName.long_field_name2 := c; + LongModuleName.long_field_name3 := d |} => (a,b,c,d). + +Check {|a:=0;b:=0|}. +Check fun '{| LongModuleName.long_field_name0:=_ |} => 0. +Eval compute in {|a:=c;b:=d|}. +Import LongModuleName. +Eval compute in {|a:=c;b:=d|}. + +End FormattingIssue13142. diff --git a/test-suite/output/goal_output.out b/test-suite/output/goal_output.out index 773533a8d3..17c1aaa55b 100644 --- a/test-suite/output/goal_output.out +++ b/test-suite/output/goal_output.out @@ -2,7 +2,79 @@ Nat.t = nat : Set Nat.t = nat : Set +2 subgoals + + ============================ + True + +subgoal 2 is: + True +2 subgoals, subgoal 1 (?Goal) + + ============================ + True + +subgoal 2 (?Goal0) is: + True 1 subgoal ============================ - False + True +1 subgoal (?Goal0) + + ============================ + True +1 subgoal (?Goal0) + + ============================ + True + +*** Unfocused goals: + +subgoal 2 (?Goal1) is: + True +subgoal 3 (?Goal) is: + True +1 subgoal + + ============================ + True + +*** Unfocused goals: + +subgoal 2 is: + True +subgoal 3 is: + True +This subproof is complete, but there are some unfocused goals. +Focus next goal with bullet -. + +2 subgoals + +subgoal 1 is: + True +subgoal 2 is: + True +This subproof is complete, but there are some unfocused goals. +Focus next goal with bullet -. + +2 subgoals + +subgoal 1 (?Goal0) is: + True +subgoal 2 (?Goal) is: + True +This subproof is complete, but there are some unfocused goals. +Focus next goal with bullet -. + +1 subgoal + +subgoal 1 is: + True +This subproof is complete, but there are some unfocused goals. +Focus next goal with bullet -. + +1 subgoal + +subgoal 1 (?Goal) is: + True diff --git a/test-suite/output/goal_output.v b/test-suite/output/goal_output.v index 327b80b0aa..b1ced94054 100644 --- a/test-suite/output/goal_output.v +++ b/test-suite/output/goal_output.v @@ -6,8 +6,32 @@ Print Nat.t. Timeout 1 Print Nat.t. -Lemma toto: False. Set Printing All. +Lemma toto: True/\True. +Proof. +split. Show. +Set Printing Goal Names. +Show. +Unset Printing Goal Names. +assert True. +- idtac. +Show. +Set Printing Goal Names. +Show. +Set Printing Unfocused. +Show. +Unset Printing Goal Names. +Show. +Unset Printing Unfocused. + auto. +Show. +Set Printing Goal Names. +Show. +Unset Printing Goal Names. +- auto. +Show. +Set Printing Goal Names. +Show. +Unset Printing Goal Names. Abort. - diff --git a/vernac/declare.ml b/vernac/declare.ml index ae7878b615..5274a6da3b 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -1854,7 +1854,8 @@ module MutualEntry : sig val declare_variable : pinfo:Proof_info.t -> uctx:UState.t - -> Entries.parameter_entry + -> sec_vars:Id.Set.t option + -> univs:Entries.universes_entry -> Names.GlobRef.t list val declare_mutdef @@ -1920,10 +1921,11 @@ end = struct in List.map_i (declare_mutdef ~pinfo ~uctx pe) 0 pinfo.Proof_info.cinfo - let declare_variable ~pinfo ~uctx pe = + let declare_variable ~pinfo ~uctx ~sec_vars ~univs = let { Info.scope; hook } = pinfo.Proof_info.info in List.map_i ( fun i { CInfo.name; typ; impargs } -> + let pe = (sec_vars, (typ, univs), None) in declare_assumption ~name ~scope ~hook ~impargs ~uctx pe ) 0 pinfo.Proof_info.cinfo @@ -1953,8 +1955,8 @@ let compute_proof_using_for_admitted proof typ pproofs = Some (Environ.really_needed env (Id.Set.union ids_typ ids_def)) | _ -> None -let finish_admitted ~pm ~pinfo ~uctx pe = - let cst = MutualEntry.declare_variable ~pinfo ~uctx pe in +let finish_admitted ~pm ~pinfo ~uctx ~sec_vars ~univs = + let cst = MutualEntry.declare_variable ~pinfo ~uctx ~sec_vars ~univs in (* If the constant was an obligation we need to update the program map *) match CEphemeron.get pinfo.Proof_info.proof_ending with | Proof_ending.End_obligation oinfo -> @@ -1974,7 +1976,7 @@ let save_admitted ~pm ~proof = let sec_vars = compute_proof_using_for_admitted proof typ pproofs in let uctx = get_initial_euctx proof in let univs = UState.check_univ_decl ~poly uctx udecl in - finish_admitted ~pm ~pinfo:proof.pinfo ~uctx (sec_vars, (typ, univs), None) + finish_admitted ~pm ~pinfo:proof.pinfo ~uctx ~sec_vars ~univs (************************************************************************) (* Saving a lemma-like constant *) @@ -2097,12 +2099,9 @@ let save_lemma_admitted_delayed ~pm ~proof ~pinfo = let poly = match proof_entry_universes with | Entries.Monomorphic_entry _ -> false | Entries.Polymorphic_entry (_, _) -> true in - let typ = match proof_entry_type with - | None -> CErrors.user_err Pp.(str "Admitted requires an explicit statement"); - | Some typ -> typ in - let ctx = UState.univ_entry ~poly uctx in + let univs = UState.univ_entry ~poly uctx in let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in - finish_admitted ~pm ~uctx ~pinfo (sec_vars, (typ, ctx), None) + finish_admitted ~pm ~uctx ~pinfo ~sec_vars ~univs let save_lemma_proved_delayed ~pm ~proof ~pinfo ~idopt = (* vio2vo calls this but with invalid info, we have to workaround diff --git a/vernac/himsg.ml b/vernac/himsg.ml index a9de01bfd0..5f7eb78a40 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -866,7 +866,7 @@ let explain_unsatisfiable_constraints env sigma constr comp = let info = Evar.Map.find ev undef in explain_typeclass_resolution env sigma info k ++ fnl () ++ cstr -let explain_pretype_error env sigma err = +let rec explain_pretype_error env sigma err = let env = Evardefine.env_nf_betaiotaevar sigma env in let env = make_all_name_different env sigma in match err with @@ -893,7 +893,7 @@ let explain_pretype_error env sigma err = | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env sigma m n | CannotFindWellTypedAbstraction (p,l,e) -> explain_cannot_find_well_typed_abstraction env sigma p l - (Option.map (fun (env',e) -> explain_type_error env' sigma e) e) + (Option.map (fun (env',e) -> explain_pretype_error env' sigma e) e) | WrongAbstractionType (n,a,t,u) -> explain_wrong_abstraction_type env sigma n a t u | AbstractionOverMeta (m,n) -> explain_abstraction_over_meta env m n diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index f972e05d3b..e9cd4272e6 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -524,8 +524,7 @@ let pr_record_field (x, { rf_subclass = oc ; rf_priority = pri ; rf_notation = n prx ++ prpri ++ prlist (pr_decl_notation @@ pr_constr) ntn let pr_record_decl c fs = - pr_opt pr_lident c ++ (if c = None then str"{" else str" {") ++ - hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}") + pr_opt pr_lident c ++ pr_record "{" "}" pr_record_field fs let pr_printable = function | PrintFullContext -> @@ -966,7 +965,7 @@ let pr_vernac_expr v = str":" ++ spc () ++ pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info ++ (match props with - | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}" + | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ pr_record_body "{" "}" pr_lconstr l | Some (true,_) -> assert false | Some (false,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p | None -> mt())) |