From b3ef24e5008c70801d272aa77251ab0bf4b46855 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Thu, 2 Feb 2017 10:04:16 +0100 Subject: correcting a typo in a comment --- interp/coqlib.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- cgit v1.2.3 From 7678cf243d054b620ba78926f2effb4dd97f0bdc Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Thu, 2 Feb 2017 11:17:02 +0100 Subject: refactoring "Names.DirPath.equal" function --- kernel/names.ml | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/kernel/names.ml b/kernel/names.ml index ee8d838da..da02a32a2 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -173,10 +173,7 @@ struct 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 equal = List.equal Id.equal let rec hash accu = function | [] -> accu -- cgit v1.2.3 From 2198b0b28a396377ed8f885eddf6bc752af9c580 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Thu, 2 Feb 2017 11:18:26 +0100 Subject: refactoring "Names.DirPath.compare" function --- kernel/names.ml | 12 +----------- 1 file changed, 1 insertion(+), 11 deletions(-) diff --git a/kernel/names.ml b/kernel/names.ml index da02a32a2..b91fa758f 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -162,17 +162,7 @@ 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 compare = List.compare Id.compare let equal = List.equal Id.equal let rec hash accu = function -- cgit v1.2.3 From dda06512833eea2805a8406b407494014371b2be Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Thu, 2 Feb 2017 11:20:51 +0100 Subject: refactoring "Names.DirPath.is_empty" function --- kernel/names.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/names.ml b/kernel/names.ml index b91fa758f..5c10badbe 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -178,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 | [] -> "<>" -- cgit v1.2.3 From 207ec95b8bda34e4c905e07a1ec6462c5fdefdb0 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Thu, 2 Feb 2017 14:35:51 +0100 Subject: simplifying "Environ.push_named" function --- kernel/pre_env.ml | 14 +------------- 1 file changed, 1 insertion(+), 13 deletions(-) diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index d14a254d3..6bfba2d40 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -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) -- cgit v1.2.3 From 4579e180f86923a455a5dc7edf0c1caafe583041 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 3 Feb 2017 09:02:19 +0100 Subject: reduce syntactic noise --- engine/proofview.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/engine/proofview.ml b/engine/proofview.ml index 9c264439b..1181d2bab 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 ; -- cgit v1.2.3 From bbec61be495db3de93fc17830405b6d80a271496 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 3 Feb 2017 09:02:41 +0100 Subject: "tclENV" is sexier, use it instead of "Env.get" --- engine/proofview.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/engine/proofview.ml b/engine/proofview.ml index 1181d2bab..f054038e9 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -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 -- cgit v1.2.3 From 4fc8616852438e80b10e0247550cc8968d76e9d7 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Thu, 9 Feb 2017 18:33:56 +0100 Subject: correcting comments in the "Context" module --- kernel/context.mli | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) 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 -- cgit v1.2.3 From aaf20df2f9e531f1f05fbf72de796f9761cd646b Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Thu, 2 Feb 2017 10:04:16 +0100 Subject: correcting a typo in a comment --- kernel/declarations.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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; -- cgit v1.2.3 From d13eb9c5ab01080a12e3bcb5cc54159ec365bee4 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 14 Apr 2017 14:44:04 +0200 Subject: refactoring "Ppvernac.pr_extend" --- printing/ppvernac.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index cfc2e48d1..547cb1de9 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1222,7 +1222,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 ")") -- cgit v1.2.3 From 37fbe7f08c34c834f5cadcd425c276fe6ec4b42c Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Mon, 7 Nov 2016 13:36:38 +0100 Subject: COMMENT: Proof_global.pstate.pid --- proofs/proof_global.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index e4cba6f07..3ee6fd40f 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; -- cgit v1.2.3 From 40f7eb94b653b60f79c4f6eb204960037fcffa66 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Mon, 7 Nov 2016 14:41:52 +0100 Subject: COMMENT: Pre_env.env --- kernel/pre_env.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 6bfba2d40..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; -- cgit v1.2.3