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 /tactics/hints.ml | |
| 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 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 5e9c3baeb1..31b276bb3e 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -320,7 +320,7 @@ let strip_params env sigma c = | App (f, args) -> (match EConstr.kind sigma f with | Const (cst,_) -> - (match Recordops.find_primitive_projection cst with + (match Structures.PrimitiveProjections.find_opt cst with | Some p -> let p = Projection.make p false in let npars = Projection.npars p in |