diff options
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 67bf8d0d29..c24520b371 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1555,7 +1555,7 @@ 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 = - match Recordops.find_primitive_projection proj with + match Structures.PrimitiveProjections.find_opt proj with | Some proj -> mkProj (Projection.make proj false, mkApp (c, args)) | None -> @@ -1585,7 +1585,7 @@ let descend_in_conjunctions avoid tac (err, info) c = let params = List.map EConstr.of_constr params in let cstr = (get_constructors env indf).(0) in let elim = - try DefinedRecord (Recordops.lookup_projections ind) + try DefinedRecord (Structures.Structure.find_projections ind) with Not_found -> let u = EInstance.kind sigma u in let (_, elim) = build_case_analysis_scheme env sigma (ind,u) false sort in @@ -1886,12 +1886,6 @@ let cut_and_apply c = (* Exact tactics *) (********************************************************************) -(* let convert_leqkey = CProfile.declare_profile "convert_leq";; *) -(* let convert_leq = CProfile.profile3 convert_leqkey convert_leq *) - -(* let refine_no_checkkey = CProfile.declare_profile "refine_no_check";; *) -(* let refine_no_check = CProfile.profile2 refine_no_checkkey refine_no_check *) - let exact_no_check c = Refine.refine ~typecheck:false (fun h -> (h,c)) |