diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-06-01 15:40:57 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-01 15:40:57 +0200 |
commit | 04756f75bf54b1ccda8c180c62b14c5eaaaabb67 (patch) | |
tree | adbf0a9beef9c5b804fdb4f3a0e7a58bb967a0e0 /tactics | |
parent | 3a36761a27487e8917e1b59b59abacc2a7e65b95 (diff) | |
parent | c7bd285555153294ec077cfa05c36bb420716f3b (diff) |
Merge PR #7234: Reduce circular dependency constants <-> projections
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/hints.ml | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index e32807f4b..a86103d57 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -294,15 +294,15 @@ let strip_params env sigma c = | App (f, args) -> (match EConstr.kind sigma f with | Const (p,_) -> - let cb = lookup_constant p env in - (match cb.Declarations.const_proj with - | Some pb -> - let n = pb.Declarations.proj_npars in - if Array.length args > n then - mkApp (mkProj (Projection.make p false, args.(n)), - Array.sub args (n+1) (Array.length args - (n + 1))) - else c - | None -> c) + let p = Projection.make p false in + (match lookup_projection p env with + | pb -> + let n = pb.Declarations.proj_npars in + if Array.length args > n then + mkApp (mkProj (p, args.(n)), + Array.sub args (n+1) (Array.length args - (n + 1))) + else c + | exception Not_found -> c) | _ -> c) | _ -> c |