diff options
author | Matej Kosik <m4tej.kosik@gmail.com> | 2016-01-08 10:00:21 +0100 |
---|---|---|
committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-01-11 11:45:08 +0100 |
commit | 9d991d36c07efbb6428e277573bd43f6d56788fc (patch) | |
tree | 5e5578043c9a3bc1c259260e5074b228e68f6c1a /proofs | |
parent | edc16686634e0700a46b79ba340ca0aac49afb0e (diff) |
CLEANUP: kernel/context.ml{,i}
The structure of the Context module was refined in such a way that:
- Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module.
- Types and functions related to rel-context were put into the Context.Rel module.
- Types and functions related to named-context declarations were put into the Context.Named.Declaration module.
- Types and functions related to named-context were put into the Context.Named module.
- Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module.
- Types and functions related to named-list-context were put into Context.NamedList module.
Some missing comments were added to the *.mli file.
The output of ocamldoc was checked whether it looks in a reasonable way.
"TODO: cleanup" was removed
The order in which are exported functions listed in the *.mli file was changed.
(as in a mature modules, this order usually is not random)
The order of exported functions in Context.{Rel,Named} modules is now consistent.
(as there is no special reason why that order should be different)
The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file.
(as there is no special reason to define them in a different order)
The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do.
(Now they are called Context.{Rel,Named}.fold_{inside,outside})
The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated.
Thrown exceptions are now documented.
Naming of formal parameters was made more consistent across different functions.
Comments of similar functions in different modules are now consistent.
Comments from *.mli files were copied to *.ml file.
(We need that information in *.mli files because that is were ocamldoc needs it.
It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function,
we can see the comments also there and do not need to open a different file if we want to see it.)
When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1.
(UTF-8 characters are used in our ocamldoc markup)
"open Context" was removed from all *.mli and *.ml files.
(Originally, it was OK to do that. Now it is not.)
An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed.
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/goal.mli | 2 | ||||
-rw-r--r-- | proofs/logic.ml | 1 | ||||
-rw-r--r-- | proofs/logic.mli | 2 | ||||
-rw-r--r-- | proofs/pfedit.ml | 2 | ||||
-rw-r--r-- | proofs/proofview.mli | 2 | ||||
-rw-r--r-- | proofs/refiner.ml | 4 | ||||
-rw-r--r-- | proofs/refiner.mli | 3 | ||||
-rw-r--r-- | proofs/tacmach.ml | 4 | ||||
-rw-r--r-- | proofs/tacmach.mli | 11 |
9 files changed, 14 insertions, 17 deletions
diff --git a/proofs/goal.mli b/proofs/goal.mli index a00a95a2f..46318b789 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -67,7 +67,7 @@ module V82 : sig val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool (* Used for congruence closure *) - val new_goal_with : Evd.evar_map -> goal -> Context.named_context -> goal Evd.sigma + val new_goal_with : Evd.evar_map -> goal -> Context.Named.t -> goal Evd.sigma (* Used by the compatibility layer and typeclasses *) val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map diff --git a/proofs/logic.ml b/proofs/logic.ml index 1ba14e7d4..e80f5a64c 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -13,7 +13,6 @@ open Names open Nameops open Term open Vars -open Context open Termops open Environ open Reductionops diff --git a/proofs/logic.mli b/proofs/logic.mli index d034b73c5..d33f56bb7 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -53,4 +53,4 @@ exception RefinerError of refiner_error val catchable_exception : exn -> bool val convert_hyp : bool -> Environ.named_context_val -> evar_map -> - Context.named_declaration -> Environ.named_context_val + Context.Named.Declaration.t -> Environ.named_context_val diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 9f2a00135..155b2cfca 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -215,7 +215,7 @@ let solve_by_implicit_tactic env sigma evk = match (!implicit_tactic, snd (evar_source evk sigma)) with | Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _) when - Context.named_context_equal (Environ.named_context_of_val evi.evar_hyps) + Context.Named.equal (Environ.named_context_of_val evi.evar_hyps) (Environ.named_context env) -> let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []) in (try diff --git a/proofs/proofview.mli b/proofs/proofview.mli index a92abcbbf..aac56e565 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -446,7 +446,7 @@ module Goal : sig environment of [gl] (i.e. the global environment and the hypotheses) and the current evar map. *) val concl : ([ `NF ], 'r) t -> Term.constr - val hyps : ([ `NF ], 'r) t -> Context.named_context + val hyps : ([ `NF ], 'r) t -> Context.Named.t val env : ('a, 'r) t -> Environ.env val sigma : ('a, 'r) t -> 'r Sigma.t val extra : ('a, 'r) t -> Evd.Store.t diff --git a/proofs/refiner.ml b/proofs/refiner.ml index ba62b2cb2..de7025062 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -197,10 +197,10 @@ let tclNOTSAMEGOAL (tac : tactic) goal = destruct), this is not detected by this tactical. *) let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) :Proof_type.goal list Evd.sigma = - let oldhyps:Context.named_context = pf_hyps goal in + let oldhyps:Context.Named.t = pf_hyps goal in let rslt:Proof_type.goal list Evd.sigma = tac goal in let { it = gls; sigma = sigma; } = rslt in - let hyps:Context.named_context list = + let hyps:Context.Named.t list = List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in let cmp (i1, c1, t1) (i2, c2, t2) = Names.Id.equal i1 i2 in let newhyps = diff --git a/proofs/refiner.mli b/proofs/refiner.mli index a81555ff5..2959787d4 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Context open Evd open Proof_type @@ -16,7 +15,7 @@ val sig_it : 'a sigma -> 'a val project : 'a sigma -> evar_map val pf_env : goal sigma -> Environ.env -val pf_hyps : goal sigma -> named_context +val pf_hyps : goal sigma -> Context.Named.t val unpackage : 'a sigma -> evar_map ref * 'a val repackage : evar_map ref -> 'a -> 'a sigma diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 57c60cbee..dc0cf81a7 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -48,7 +48,7 @@ let pf_last_hyp gl = List.hd (pf_hyps gl) let pf_get_hyp gls id = try - Context.lookup_named id (pf_hyps gls) + Context.Named.lookup id (pf_hyps gls) with Not_found -> raise (RefinerError (NoSuchHyp id)) @@ -198,7 +198,7 @@ module New = struct let pf_get_hyp id gl = let hyps = Proofview.Goal.hyps gl in let sign = - try Context.lookup_named id hyps + try Context.Named.lookup id hyps with Not_found -> raise (RefinerError (NoSuchHyp id)) in sign diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index c45fd250c..b7915e837 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Environ open Evd open Proof_type @@ -34,18 +33,18 @@ val apply_sig_tac : val pf_concl : goal sigma -> types val pf_env : goal sigma -> env -val pf_hyps : goal sigma -> named_context +val pf_hyps : goal sigma -> Context.Named.t (*i val pf_untyped_hyps : goal sigma -> (Id.t * constr) list i*) val pf_hyps_types : goal sigma -> (Id.t * types) list val pf_nth_hyp_id : goal sigma -> int -> Id.t -val pf_last_hyp : goal sigma -> named_declaration +val pf_last_hyp : goal sigma -> Context.Named.Declaration.t val pf_ids_of_hyps : goal sigma -> Id.t list val pf_global : goal sigma -> Id.t -> constr val pf_unsafe_type_of : goal sigma -> constr -> types val pf_type_of : goal sigma -> constr -> evar_map * types val pf_hnf_type_of : goal sigma -> constr -> types -val pf_get_hyp : goal sigma -> Id.t -> named_declaration +val pf_get_hyp : goal sigma -> Id.t -> Context.Named.Declaration.t val pf_get_hyp_typ : goal sigma -> Id.t -> types val pf_get_new_id : Id.t -> goal sigma -> Id.t @@ -123,9 +122,9 @@ module New : sig val pf_ids_of_hyps : ('a, 'r) Proofview.Goal.t -> identifier list val pf_hyps_types : ('a, 'r) Proofview.Goal.t -> (identifier * types) list - val pf_get_hyp : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> named_declaration + val pf_get_hyp : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t val pf_get_hyp_typ : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> types - val pf_last_hyp : ([ `NF ], 'r) Proofview.Goal.t -> named_declaration + val pf_last_hyp : ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> pinductive * types |