diff options
| author | Pierre-Marie Pédrot | 2021-03-30 14:02:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-03-30 14:02:16 +0200 |
| commit | f0c6a1de3eef85ab0787be7e87cb8509e8df43d5 (patch) | |
| tree | 05f3cc7ece9e0a77f841b37a12db909ff6362be0 /library | |
| parent | 303afeab9c946bdba15e1984231ae5066bf37af6 (diff) | |
| parent | d9c80dadd353bd8b0eb90ce290048a2538f1a41a (diff) | |
Merge PR #13958: [recordops] complete API rewrite; the module is now called [structures]
Reviewed-by: SkySkimmer
Reviewed-by: ejgallego
Ack-by: herbelin
Reviewed-by: ppedrot
Diffstat (limited to 'library')
| -rw-r--r-- | library/globnames.ml | 4 | ||||
| -rw-r--r-- | library/globnames.mli | 1 |
2 files changed, 0 insertions, 5 deletions
diff --git a/library/globnames.ml b/library/globnames.ml index 654349dea0..491c89e68e 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -31,10 +31,6 @@ let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef" let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef" let destConstructRef = function ConstructRef ind -> ind | _ -> failwith "destConstructRef" -let subst_constructor subst (ind,j as ref) = - let ind' = subst_ind subst ind in - if ind==ind' then ref - else (ind',j) let subst_global_reference subst ref = match ref with | VarRef var -> ref diff --git a/library/globnames.mli b/library/globnames.mli index 8acea5ef28..58e0efbc7a 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -34,7 +34,6 @@ val destConstructRef : GlobRef.t -> constructor val is_global : GlobRef.t -> constr -> bool [@@ocaml.deprecated "Use [Constr.isRefX] instead."] -val subst_constructor : substitution -> constructor -> constructor val subst_global : substitution -> GlobRef.t -> GlobRef.t * constr Univ.univ_abstracted option val subst_global_reference : substitution -> GlobRef.t -> GlobRef.t |