diff options
| -rw-r--r-- | engine/proofview.ml | 12 | ||||
| -rw-r--r-- | interp/coqlib.mli | 2 | ||||
| -rw-r--r-- | kernel/context.mli | 10 | ||||
| -rw-r--r-- | kernel/declarations.mli | 2 | ||||
| -rw-r--r-- | kernel/names.ml | 19 | ||||
| -rw-r--r-- | kernel/pre_env.ml | 18 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 2 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 2 |
8 files changed, 21 insertions, 46 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index 9c264439b..f054038e9 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1020,11 +1020,11 @@ module Goal = struct let assume (gl : ('a, 'r) t) = (gl :> ([ `NF ], 'r) t) - let env { env=env } = env - let sigma { sigma=sigma } = Sigma.Unsafe.of_evar_map sigma - let hyps { env=env } = EConstr.named_context env - let concl { concl=concl } = concl - let extra { sigma=sigma; self=self } = goal_extra sigma self + let env {env} = env + let sigma {sigma} = Sigma.Unsafe.of_evar_map sigma + let hyps {env} = EConstr.named_context env + let concl {concl} = concl + let extra {sigma; self} = goal_extra sigma self let gmake_with info env sigma goal = { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ; @@ -1040,7 +1040,7 @@ module Goal = struct let nf_enter f = InfoL.tag (Info.Dispatch) begin iter_goal begin fun goal -> - Env.get >>= fun env -> + tclENV >>= fun env -> tclEVARMAP >>= fun sigma -> try let (gl, sigma) = nf_gmake env sigma goal in diff --git a/interp/coqlib.mli b/interp/coqlib.mli index 5ba26d828..1facb47e1 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -19,7 +19,7 @@ open Util (** [find_reference caller_message [dir;subdir;...] s] returns a global reference to the name dir.subdir.(...).s; the corresponding module must have been required or in the process of being compiled so that - it must be used lazyly; it raises an anomaly with the given message + it must be used lazily; it raises an anomaly with the given message if not found *) type message = string diff --git a/kernel/context.mli b/kernel/context.mli index 0c666a25d..24e69ebd6 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -214,7 +214,7 @@ sig val to_rel_decl : ('c, 't) pt -> ('c, 't) Rel.Declaration.pt end - (** Rel-context is represented as a list of declarations. + (** Named-context is represented as a list of declarations. Inner-most declarations are at the beginning of the list. Outer-most declarations are at the end of the list. *) type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list @@ -223,7 +223,7 @@ sig (** empty named-context *) val empty : ('c, 't) pt - (** Return a new rel-context enriched by with a given inner-most declaration. *) + (** Return a new named-context enriched by with a given inner-most declaration. *) val add : ('c, 't) Declaration.pt -> ('c, 't) pt -> ('c, 't) pt (** Return the number of {e local declarations} in a given named-context. *) @@ -233,7 +233,7 @@ sig @raise Not_found if the designated identifier is not bound in a given named-context. *) val lookup : Id.t -> ('c, 't) pt -> ('c, 't) Declaration.pt - (** Check whether given two rel-contexts are equal. *) + (** Check whether given two named-contexts are equal. *) val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool (** Map all terms in a given named-context. *) @@ -253,8 +253,8 @@ sig (** Return the set of all identifiers bound in a given named-context. *) val to_vars : ('c, 't) pt -> Id.Set.t - (** [instance_from_named_context Ω] builds an instance [args] such - that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local + (** [to_instance Ω] builds an instance [args] such + that [Ω ⊢ args:Ω] where [Ω] is a named-context and with the local definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it gives [Var id1, Var id3]. All [idj] are supposed distinct. *) val to_instance : (Id.t -> 'r) -> ('c, 't) pt -> 'r list diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 7821ea20f..71e228b19 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -77,7 +77,7 @@ type typing_flags = { } (* some contraints are in constant_constraints, some other may be in - * the OpaueDef *) + * the OpaqueDef *) type constant_body = { const_hyps : Context.Named.t; (** New: younger hyp at top *) const_body : constant_def; diff --git a/kernel/names.ml b/kernel/names.ml index ee8d838da..5c10badbe 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -162,21 +162,8 @@ module DirPath = struct type t = module_ident list - let rec compare (p1 : t) (p2 : t) = - if p1 == p2 then 0 - else begin match p1, p2 with - | [], [] -> 0 - | [], _ -> -1 - | _, [] -> 1 - | id1 :: p1, id2 :: p2 -> - let c = Id.compare id1 id2 in - if Int.equal c 0 then compare p1 p2 else c - end - - let rec equal p1 p2 = p1 == p2 || match p1, p2 with - | [], [] -> true - | id1 :: p1, id2 :: p2 -> Id.equal id1 id2 && equal p1 p2 - | _ -> false + let compare = List.compare Id.compare + let equal = List.equal Id.equal let rec hash accu = function | [] -> accu @@ -191,7 +178,7 @@ struct let empty = [] - let is_empty d = match d with [] -> true | _ -> false + let is_empty = List.is_empty let to_string = function | [] -> "<>" diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index d14a254d3..48d7ee9ec 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -68,8 +68,8 @@ type named_context_val = { } type env = { - env_globals : globals; - env_named_context : named_context_val; + env_globals : globals; (* globals = constants + inductive types + modules + module-types *) + env_named_context : named_context_val; (* section variables *) env_rel_context : Context.Rel.t; env_rel_val : lazy_val list; env_nb_rel : int; @@ -161,19 +161,7 @@ let map_named_val f ctxt = else { env_named_ctx = ctx; env_named_map = map } let push_named d env = -(* if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context); - assert (env.env_rel_context = []); *) - { env_globals = env.env_globals; - env_named_context = push_named_context_val d env.env_named_context; - env_rel_context = env.env_rel_context; - env_rel_val = env.env_rel_val; - env_nb_rel = env.env_nb_rel; - env_stratification = env.env_stratification; - env_typing_flags = env.env_typing_flags; - env_conv_oracle = env.env_conv_oracle; - retroknowledge = env.retroknowledge; - indirect_pterms = env.indirect_pterms; - } + {env with env_named_context = push_named_context_val d env.env_named_context} let lookup_named id env = fst (Id.Map.find id env.env_named_context.env_named_map) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 5af0e1d9b..e4a87739b 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1221,7 +1221,7 @@ open Decl_kinds | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl | [], [] -> [] | _ -> assert false in - hov 1 (pr_sequence (fun x -> x) (aux rl cl)) + hov 1 (pr_sequence identity (aux rl cl)) with Not_found -> hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")") diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 61b776f24..5f4a7766f 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -88,7 +88,7 @@ type proof_terminator = proof_ending -> unit type closed_proof = proof_object * proof_terminator type pstate = { - pid : Id.t; + pid : Id.t; (* the name of the theorem whose proof is being constructed *) terminator : proof_terminator CEphemeron.key; endline_tactic : Genarg.glob_generic_argument option; section_vars : Context.Named.t option; |