diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 2 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 3 | ||||
| -rw-r--r-- | vernac/vernacinterp.ml | 14 | ||||
| -rw-r--r-- | vernac/vernacinterp.mli | 4 |
5 files changed, 12 insertions, 13 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 7af391758d..66a4a2e492 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -190,7 +190,7 @@ let build_beq_scheme mode kn = match EConstr.kind sigma c with | Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants | Var x -> - let eid = id_of_string ("eq_"^(string_of_id x)) in + let eid = Id.of_string ("eq_"^(Id.to_string x)) in let () = try ignore (Environ.lookup_named eid env) with Not_found -> raise (ParameterWithoutEquality (VarRef x)) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 9ab89c8832..dbf7fec660 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -506,7 +506,7 @@ let save_proof ?proof = function let env = Global.env () in let ids_typ = Environ.global_vars_set env typ in let ids_def = Environ.global_vars_set env pproof in - Some (Environ.keep_hyps env (Idset.union ids_typ ids_def)) + Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def)) | _ -> None in let decl = Proof_global.get_universe_decl () in let evd = Evd.from_ctx universes in 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 |