diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hints.ml | 18 | ||||
| -rw-r--r-- | tactics/hipattern.ml | 4 | ||||
| -rw-r--r-- | tactics/tactics.ml | 5 |
3 files changed, 15 insertions, 12 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/hipattern.ml b/tactics/hipattern.ml index f9c4bed352..7da059ae35 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -263,7 +263,9 @@ open Evar_kinds let mkPattern c = snd (Patternops.pattern_of_glob_constr c) let mkGApp f args = DAst.make @@ GApp (f, args) let mkGHole = DAst.make @@ - GHole (QuestionMark (Define false,Anonymous), Namegen.IntroAnonymous, None) + GHole (QuestionMark { + Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=Define false; + }, Namegen.IntroAnonymous, None) let mkGProd id c1 c2 = DAst.make @@ GProd (Name (Id.of_string id), Explicit, c1, c2) let mkGArrow c1 c2 = DAst.make @@ 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 |