diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/classes.ml | 2 | ||||
| -rw-r--r-- | vernac/comArguments.ml | 3 | ||||
| -rw-r--r-- | vernac/declare.ml | 14 | ||||
| -rw-r--r-- | vernac/declare.mli | 8 | ||||
| -rw-r--r-- | vernac/prettyp.ml | 36 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 3 | ||||
| -rw-r--r-- | vernac/vernacinterp.ml | 7 | ||||
| -rw-r--r-- | vernac/vernacstate.ml | 6 | ||||
| -rw-r--r-- | vernac/vernacstate.mli | 3 |
9 files changed, 44 insertions, 38 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 82a1e32a14..02cb60f1cf 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -359,7 +359,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id consequence, we use the low-level primitives to code the refinement manually.*) let future_goals, sigma = Evd.pop_future_goals sigma in - let gls = List.rev_append future_goals.Evd.FutureGoals.shelf (List.rev future_goals.Evd.FutureGoals.comb) in + let gls = List.rev future_goals.Evd.FutureGoals.comb in let sigma = Evd.push_future_goals sigma in let kind = Decls.(IsDefinition Instance) in let hook = Declare.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml index be9cc059a7..adf1f42beb 100644 --- a/vernac/comArguments.ml +++ b/vernac/comArguments.ml @@ -218,9 +218,8 @@ let vernac_arguments ~section_local reference args more_implicits flags = in let implicits = implicits :: more_implicits in - let implicits = List.map (List.map snd) implicits in let implicits_specified = match implicits with - | [l] -> List.exists (function Glob_term.Explicit -> false | _ -> true) l + | [l] -> List.exists (function _, Glob_term.Explicit -> false | _ -> true) l | _ -> true in if implicits_specified && clear_implicits_flag then diff --git a/vernac/declare.ml b/vernac/declare.ml index 28e6f21d41..099a63cf8f 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -1553,11 +1553,11 @@ let set_used_variables ps l = ctx, { ps with section_vars = Some (Context.Named.to_vars ctx) } let get_open_goals ps = - let Proof.{ goals; stack; shelf } = Proof.data ps.proof in + let Proof.{ goals; stack; sigma } = Proof.data ps.proof in List.length goals + List.fold_left (+) 0 (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) + - List.length shelf + List.length (Evd.shelf sigma) type proof_object = { name : Names.Id.t @@ -1734,8 +1734,8 @@ let return_proof ps = let p, uctx = prepare_proof ~unsafe_typ:false ps in List.map (fun (((_ub, body),eff),_) -> (body,eff)) p, uctx -let update_global_env = - map ~f:(fun p -> Proof.update_sigma_env p (Global.env ())) +let update_sigma_univs ugraph p = + map ~f:(Proof.update_sigma_univs ugraph) p let next = let n = ref 0 in fun () -> incr n; !n @@ -2014,7 +2014,7 @@ let finish_derived ~f ~name ~entries = let lemma_def = Internal.map_entry_body lemma_def ~f:(fun ((b,ctx),fx) -> (substf b, ctx), fx) in let lemma_def = DefinitionEntry lemma_def in let ct = declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in - [GlobRef.ConstRef ct] + [GlobRef.ConstRef f_kn; GlobRef.ConstRef ct] let finish_proved_equations ~pm ~kind ~hook i proof_obj types sigma0 = @@ -2251,7 +2251,7 @@ let rec solve_obligation prg num tac = let scope = Locality.Global Locality.ImportNeedQualified in let kind = kind_of_obligation (snd obl.obl_status) in let evd = Evd.from_ctx (Internal.get_uctx prg) in - let evd = Evd.update_sigma_env evd (Global.env ()) in + let evd = Evd.update_sigma_univs (Global.universes ()) evd in let auto ~pm n oblset tac = auto_solve_obligations ~pm n ~oblset tac in let proof_ending = let name = Internal.get_name prg in @@ -2292,7 +2292,7 @@ and solve_obligation_by_tac prg obls i tac = | None -> !default_tactic in let uctx = Internal.get_uctx prg in - let uctx = UState.update_sigma_env uctx (Global.env ()) in + let uctx = UState.update_sigma_univs uctx (Global.universes ()) in let poly = Internal.get_poly prg in match solve_by_tac ?loc:(fst obl.obl_location) obl.obl_name (evar_of_obligation obl) tac ~poly ~uctx with | None -> None diff --git a/vernac/declare.mli b/vernac/declare.mli index 3001d0d206..1ad79928d5 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -246,10 +246,10 @@ module Proof : sig val compact : t -> t - (** Update the proofs global environment after a side-effecting command - (e.g. a sublemma definition) has been run inside it. Assumes - there_are_pending_proofs. *) - val update_global_env : t -> t + (** Update the proof's universe information typically after a + side-effecting command (e.g. a sublemma definition) has been run + inside it. *) + val update_sigma_univs : UGraph.t -> t -> t val get_open_goals : t -> int diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 2b46542287..8b00484b4a 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -75,12 +75,12 @@ let print_ref reduce ref udecl = let inst = Univ.make_abstract_instance univs in let bl = Printer.universe_binders_with_opt_names (Environ.universes_of_global env ref) udecl in let sigma = Evd.from_ctx (UState.of_binders bl) in - let typ = EConstr.of_constr typ in let typ = if reduce then - let ctx,ccl = Reductionops.splay_prod_assum env sigma typ - in EConstr.it_mkProd_or_LetIn ccl ctx + let ctx,ccl = Reductionops.splay_prod_assum env sigma (EConstr.of_constr typ) + in EConstr.to_constr sigma (EConstr.it_mkProd_or_LetIn ccl ctx) else typ in + let typ = Arguments_renaming.rename_type typ ref in let impargs = select_stronger_impargs (implicits_of_global ref) in let impargs = List.map binding_kind_of_status impargs in let variance = let open GlobRef in match ref with @@ -95,7 +95,7 @@ let print_ref reduce ref udecl = else mt () in let priv = None in (* We deliberately don't print private univs in About. *) - hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma ~impargs typ ++ + hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_ltype_env env sigma ~impargs typ ++ Printer.pr_abstract_universe_ctx sigma ?variance univs ?priv) (********************************) @@ -261,6 +261,10 @@ let implicit_kind_of_status = function | None -> Anonymous, Glob_term.Explicit | Some (pos,_,(maximal,_)) -> implicit_name_of_pos pos, if maximal then Glob_term.MaxImplicit else Glob_term.NonMaxImplicit +let extra_implicit_kind_of_status imp = + let _,imp = implicit_kind_of_status imp in + (Anonymous, imp) + let dummy = { Vernacexpr.implicit_status = Glob_term.Explicit; name = Anonymous; @@ -268,8 +272,10 @@ let dummy = { notation_scope = None; } -let is_dummy {Vernacexpr.implicit_status; name; recarg_like; notation_scope} = - name = Anonymous && not recarg_like && notation_scope = None && implicit_status = Glob_term.Explicit +let is_dummy = function + | Vernacexpr.(RealArg {implicit_status; name; recarg_like; notation_scope}) -> + name = Anonymous && not recarg_like && notation_scope = None && implicit_status = Glob_term.Explicit + | _ -> false let rec main_implicits i renames recargs scopes impls = if renames = [] && recargs = [] && scopes = [] && impls = [] then [] @@ -292,9 +298,7 @@ let rec main_implicits i renames recargs scopes impls = let tl = function [] -> [] | _::tl -> tl in (* recargs is special -> tl handled above *) let rest = main_implicits (i+1) (tl renames) recargs (tl scopes) (tl impls) in - if is_dummy status && rest = [] - then [] (* we may have a trail of dummies due to eg "clear scopes" *) - else status :: rest + status :: rest let rec insert_fake_args volatile bidi impls = let open Vernacexpr in @@ -320,11 +324,7 @@ let print_arguments ref = | Some (UnfoldWhen { nargs; recargs }) -> [], recargs, nargs | Some (UnfoldWhenNoMatch { nargs; recargs }) -> [`ReductionDontExposeCase], recargs, nargs in - let flags, renames = match Arguments_renaming.arguments_names ref with - | exception Not_found -> flags, [] - | [] -> flags, [] - | renames -> `Rename::flags, renames - in + let renames = try Arguments_renaming.arguments_names ref with Not_found -> [] in let scopes = Notation.find_arguments_scope ref in let flags = if needs_extra_scopes ref scopes then `ExtraScopes::flags else flags in let impls = Impargs.extract_impargs_data (Impargs.implicits_of_global ref) in @@ -333,15 +333,17 @@ let print_arguments ref = | [] -> assert false in let impls = main_implicits 0 renames recargs scopes impls in - let moreimpls = List.map (fun (_,i) -> List.map implicit_kind_of_status i) moreimpls in + let moreimpls = List.map (fun (_,i) -> List.map extra_implicit_kind_of_status i) moreimpls in let bidi = Pretyping.get_bidirectionality_hint ref in let impls = insert_fake_args nargs_for_red bidi impls in - if impls = [] && moreimpls = [] && flags = [] then [] + if List.for_all is_dummy impls && moreimpls = [] && flags = [] then [] else let open Constrexpr in let open Vernacexpr in [Ppvernac.pr_vernac_expr - (VernacArguments (CAst.make (AN qid), impls, moreimpls, flags))] + (VernacArguments (CAst.make (AN qid), impls, moreimpls, flags)) ++ + (if renames = [] then mt () else + fnl () ++ str " (where some original arguments have been renamed)")] let print_name_infos ref = let type_info_for_implicit = diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 540e85621a..6a4c2a626d 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -112,7 +112,8 @@ let show_proof ~pstate = let show_top_evars ~proof = (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *) - let Proof.{goals;shelf;sigma} = Proof.data proof in + let Proof.{goals; sigma} = Proof.data proof in + let shelf = Evd.shelf sigma in let given_up = Evar.Set.elements @@ Evd.given_up sigma in pr_evars_int sigma ~shelf ~given_up 1 (Evd.undefined_map sigma) diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 6be2fb0d43..edf48fef1a 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -211,8 +211,11 @@ and interp_control ~st ({ CAst.v = cmd } as vernac) = (fun ~st -> let before_univs = Global.universes () in let pstack, pm = interp_expr ~atts:cmd.attrs ~st cmd.expr in - if before_univs == Global.universes () then pstack, pm - else Option.map (Vernacstate.LemmaStack.map_top ~f:Declare.Proof.update_global_env) pstack, pm) + let after_univs = Global.universes () in + if before_univs == after_univs then pstack, pm + else + let f = Declare.Proof.update_sigma_univs after_univs in + Option.map (Vernacstate.LemmaStack.map ~f) pstack, pm) ~st (* XXX: This won't properly set the proof mode, as of today, it is diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 6d12d72408..204008997d 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -80,7 +80,7 @@ module LemmaStack = struct type t = Declare.Proof.t * Declare.Proof.t list - let map f (pf, pfl) = (f pf, List.map f pfl) + let map ~f (pf, pfl) = (f pf, List.map f pfl) let map_top ~f (pf, pfl) = (f pf, pfl) let pop (ps, p) = match p with @@ -96,7 +96,7 @@ module LemmaStack = struct let get_all_proof_names (pf : t) = let prj x = Declare.Proof.get x in - let (pn, pns) = map Proof.(function pf -> (data (prj pf)).name) pf in + let (pn, pns) = map ~f:Proof.(function pf -> (data (prj pf)).name) pf in pn :: pns let copy_info src tgt = @@ -218,7 +218,7 @@ module Declare_ = struct Declare.Proof.info pt) let discard_all () = s_lemmas := None - let update_global_env () = dd (Declare.Proof.update_global_env) + let update_sigma_univs ugraph = dd (Declare.Proof.update_sigma_univs ugraph) let get_current_context () = cc Declare.Proof.get_current_context diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index 5efdb3cc68..e1b13dcb73 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -40,6 +40,7 @@ module LemmaStack : sig val pop : t -> Declare.Proof.t * t option val push : t option -> Declare.Proof.t -> t + val map : f:(Declare.Proof.t -> Declare.Proof.t) -> t -> t val map_top : f:(Declare.Proof.t -> Declare.Proof.t) -> t -> t val with_top : t -> f:(Declare.Proof.t -> 'a ) -> 'a @@ -112,7 +113,7 @@ module Declare : sig val close_proof : opaque:Vernacexpr.opacity_flag -> keep_body_ucst_separate:bool -> closed_proof val discard_all : unit -> unit - val update_global_env : unit -> unit + val update_sigma_univs : UGraph.t -> unit val get_current_context : unit -> Evd.evar_map * Environ.env |