diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hints.ml | 18 | ||||
| -rw-r--r-- | tactics/tactics.ml | 5 |
2 files changed, 12 insertions, 11 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 748e0362c4..09b2e59cea 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -299,16 +299,16 @@ let strip_params env sigma c = match EConstr.kind sigma c with | App (f, args) -> (match EConstr.kind sigma f with - | Const (p,_) -> - 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))) + | Const (cst,_) -> + (match Recordops.find_primitive_projection cst with + | Some p -> + let p = Projection.make p false in + let npars = Projection.npars p in + if Array.length args > npars then + mkApp (mkProj (p, args.(npars)), + Array.sub args (npars+1) (Array.length args - (npars + 1))) else c - | exception Not_found -> c) + | None -> c) | _ -> c) | _ -> c diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 928530744a..5fc34619e8 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1581,9 +1581,10 @@ let make_projection env sigma params cstr sign elim i n c u = | Some proj -> let args = Context.Rel.to_extended_vect mkRel 0 sign in let proj = - if Environ.is_projection proj env then + match Recordops.find_primitive_projection proj with + | Some proj -> mkProj (Projection.make proj false, mkApp (c, args)) - else + | None -> mkApp (mkConstU (proj,u), Array.append (Array.of_list params) [|mkApp (c, args)|]) in |