diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/extraction.ml | 7 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 8 | ||||
| -rw-r--r-- | plugins/ltac/taccoerce.ml | 7 | ||||
| -rw-r--r-- | plugins/ltac/taccoerce.mli | 2 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml | 20 |
5 files changed, 24 insertions, 20 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 0cad192332..ca4f5429a2 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -22,7 +22,6 @@ open Reductionops open Inductive open Termops open Inductiveops -open Recordops open Namegen open Miniml open Table @@ -531,7 +530,7 @@ and extract_really_ind env kn mib = let n = nb_default_params env sg (EConstr.of_constr ty) in let check_proj kn = if Cset.mem kn !projs then add_projection n kn ip in - List.iter (Option.iter check_proj) (lookup_projections ip) + List.iter (Option.iter check_proj) (Structures.Structure.find_projections ip) with Not_found -> () end; Record field_glob @@ -1129,7 +1128,7 @@ let extract_constant env kn cb = (match cb.const_body with | Primitive _ | Undef _ -> warn_info (); mk_typ_ax () | Def c -> - (match Recordops.find_primitive_projection kn with + (match Structures.PrimitiveProjections.find_opt kn with | None -> mk_typ (get_body c) | Some p -> let body = fake_match_projection env p in @@ -1142,7 +1141,7 @@ let extract_constant env kn cb = (match cb.const_body with | Primitive _ | Undef _ -> warn_info (); mk_ax () | Def c -> - (match Recordops.find_primitive_projection kn with + (match Structures.PrimitiveProjections.find_opt kn with | None -> mk_def (get_body c) | Some p -> let body = fake_match_projection env p in diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index c7bda43465..1640bff43b 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -373,11 +373,6 @@ end) = struct end -(* let my_type_of env evars c = Typing.e_type_of env evars c *) -(* let mytypeofkey = CProfile.declare_profile "my_type_of";; *) -(* let my_type_of = CProfile.profile3 mytypeofkey my_type_of *) - - let type_app_poly env env evd f args = let evars, c = app_poly_nocheck env evd f args in let evd', t = Typing.type_of env (goalevars evars) c in @@ -2066,9 +2061,6 @@ let get_hyp gl (c,l) clause l2r = let general_rewrite_flags = { under_lambdas = false; on_morphisms = true } -(* let rewriteclaustac_key = CProfile.declare_profile "cl_rewrite_clause_tac";; *) -(* let cl_rewrite_clause_tac = CProfile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *) - (** Setoid rewriting when called with "rewrite" *) let general_s_rewrite cl l2r occs (c,l) ~new_goals = Proofview.Goal.enter begin fun gl -> diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 5e88bf7c79..f2f5fc16a6 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -91,6 +91,13 @@ let to_int v = Some (out_gen (topwit wit_int) v) else None +let of_ident id = in_gen (topwit wit_ident) id + +let to_ident v = + if has_type v (topwit wit_ident) then + Some (out_gen (topwit wit_ident) v) + else None + let to_list v = prj Val.typ_list v let to_option v = prj Val.typ_opt v diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index 8ca2510459..c748fb3d1a 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -39,6 +39,8 @@ sig val to_uconstr : t -> Ltac_pretype.closed_glob_constr option val of_int : int -> t val to_int : t -> int option + val of_ident : Id.t -> t + val to_ident : t -> Id.t option val to_list : t -> t list option val to_option : t -> t option option val to_pair : t -> (t * t) option diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 7774258fca..805be1fc87 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -22,7 +22,6 @@ open Vars open Libnames open Tactics open Termops -open Recordops open Tacmach open Glob_term open Util @@ -333,7 +332,8 @@ type tpattern = { let all_ok _ _ = true let proj_nparams c = - try 1 + Recordops.find_projection_nparams (GlobRef.ConstRef c) with _ -> 0 + try 1 + Structures.Structure.projection_nparams c + with Not_found -> 0 let isRigid c = match kind c with | Prod _ | Sort _ | Lambda _ | Case _ | Fix _ | CoFix _ -> true @@ -429,9 +429,13 @@ let ungen_upat lhs (sigma, uc, t) u = | _ -> KpatRigid in sigma, uc, {u with up_k = k; up_FO = lhs; up_f = f; up_a = a; up_t = t} -let nb_cs_proj_args pc f u = +let nb_cs_proj_args ise pc f u = + let open Structures in + let open ValuePattern in let na k = - List.length (snd (lookup_canonical_conversion (Global.env()) (GlobRef.ConstRef pc, k))).o_TCOMPS in + let open CanonicalSolution in + let _, { cvalue_arguments } = find (Global.env()) ise (GlobRef.ConstRef pc, k) in + List.length cvalue_arguments in let nargs_of_proj t = match kind t with | App(_,args) -> Array.length args | Proj _ -> 0 (* if splay_app calls expand_projection, this has to be @@ -441,7 +445,7 @@ let nb_cs_proj_args pc f u = | Prod _ -> na Prod_cs | Sort s -> na (Sort_cs (Sorts.family s)) | Const (c',_) when Constant.CanOrd.equal c' pc -> nargs_of_proj u.up_f - | Proj (c',_) when Constant.CanOrd.equal (Projection.constant c') pc -> nargs_of_proj u.up_f + | Proj (c',_) when Constant.CanOrd.equal (Names.Projection.constant c') pc -> nargs_of_proj u.up_f | Var _ | Ind _ | Construct _ | Const _ -> na (Const_cs (fst @@ destRef f)) | _ -> -1 with Not_found -> -1 @@ -467,7 +471,7 @@ let splay_app ise = | Cast _ | Evar _ -> loop c [| |] | _ -> c, [| |] -let filter_upat i0 f n u fpats = +let filter_upat ise i0 f n u fpats = let na = Array.length u.up_a in if n < na then fpats else let np = match u.up_k with @@ -479,7 +483,7 @@ let filter_upat i0 f n u fpats = | KpatRigid when isRigid f -> na | KpatFlex -> na | KpatProj pc -> - let np = na + nb_cs_proj_args pc f u in if n < np then -1 else np + let np = na + nb_cs_proj_args ise pc f u in if n < np then -1 else np | _ -> -1 in if np < na then fpats else let () = if !i0 < np then i0 := n in (u, np) :: fpats @@ -568,7 +572,7 @@ let match_upats_HO ~on_instance upats env sigma0 ise c = let failed_because_of_TC = ref false in let rec aux upats env sigma0 ise c = let f, a = splay_app ise c in let i0 = ref (-1) in - let fpats = List.fold_right (filter_upat i0 f (Array.length a)) upats [] in + let fpats = List.fold_right (filter_upat ise i0 f (Array.length a)) upats [] in while !i0 >= 0 do let i = !i0 in i0 := -1; let one_match (u, np) = |