diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/mod_subst.ml | 9 | ||||
| -rw-r--r-- | kernel/mod_subst.mli | 8 | ||||
| -rw-r--r-- | kernel/names.ml | 10 | ||||
| -rw-r--r-- | kernel/names.mli | 8 |
4 files changed, 0 insertions, 35 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 2aeb1ea202..4778bf1121 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -340,15 +340,6 @@ let subst_retro_action subst action = let c' = subst_constant subst c in if c == c' then action else Register_type(prim, c') -(* Here the semantics is completely unclear. - What does "Hint Unfold t" means when "t" is a parameter? - Does the user mean "Unfold X.t" or does she mean "Unfold y" - where X.t is later on instantiated with y? I choose the first - interpretation (i.e. an evaluable reference is never expanded). *) -let subst_evaluable_reference subst = function - | EvalVarRef id -> EvalVarRef id - | EvalConstRef kn -> EvalConstRef (subst_constant subst kn) - let rec map_kn f f' c = let func = map_kn f f' in match kind c with diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index bc5816dafb..9cf270cff7 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -146,14 +146,6 @@ val subst_proj : substitution -> Projection.t -> Projection.t val subst_retro_action : substitution -> Retroknowledge.action -> Retroknowledge.action -(** Here the semantics is completely unclear. - What does "Hint Unfold t" means when "t" is a parameter? - Does the user mean "Unfold X.t" or does she mean "Unfold y" - where X.t is later on instantiated with y? I choose the first - interpretation (i.e. an evaluable reference is never expanded). *) -val subst_evaluable_reference : - substitution -> evaluable_global_reference -> evaluable_global_reference - (** [replace_mp_in_con mp mp' con] replaces [mp] with [mp'] in [con] *) val replace_mp_in_kn : ModPath.t -> ModPath.t -> KerName.t -> KerName.t diff --git a/kernel/names.ml b/kernel/names.ml index be65faf234..60c6c7bd67 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -1100,16 +1100,6 @@ module GlobRef = struct end -type evaluable_global_reference = - | EvalVarRef of Id.t - | EvalConstRef of Constant.t - -(* Better to have it here that in closure, since used in grammar.cma *) -let eq_egr e1 e2 = match e1, e2 with - EvalConstRef con1, EvalConstRef con2 -> Constant.equal con1 con2 - | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2 - | _, _ -> false - (** Located identifiers and objects with syntax. *) type lident = Id.t CAst.t diff --git a/kernel/names.mli b/kernel/names.mli index 747299bb12..09885396c0 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -714,14 +714,6 @@ module GlobRef : sig end -(** Better to have it here that in Closure, since required in grammar.cma *) -(* XXX: Move to a module *) -type evaluable_global_reference = - | EvalVarRef of Id.t - | EvalConstRef of Constant.t - -val eq_egr : evaluable_global_reference -> evaluable_global_reference -> bool - (** Located identifiers and objects with syntax. *) type lident = Id.t CAst.t |