diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 6 | ||||
| -rw-r--r-- | tactics/btermdn.ml | 15 | ||||
| -rw-r--r-- | tactics/eauto.ml | 3 | ||||
| -rw-r--r-- | tactics/hints.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 10 |
5 files changed, 14 insertions, 22 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 353e138599..0189e3ab04 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -500,12 +500,6 @@ let delta_auto debug mod_delta n lems dbnames = (search d n mod_delta db_list hints) end -let delta_auto = - if Flags.profile then - let key = CProfile.declare_profile "delta_auto" in - CProfile.profile5 key delta_auto - else delta_auto - let auto ?(debug=Off) n = delta_auto debug false n let new_auto ?(debug=Off) n = delta_auto debug true n diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index af0ca22868..794d2bb94f 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -32,18 +32,25 @@ let compare_term_label t1 t2 = match t1, t2 with type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything -let decomp_pat = +let decomp_pat p = let rec decrec acc = function | PApp (f,args) -> decrec (Array.to_list args @ acc) f - | PProj (p, c) -> (PRef (GlobRef.ConstRef (Projection.constant p)), c :: acc) + | PProj (p, c) -> + let hole = PMeta None in + let params = List.make (Projection.npars p) hole in + (PRef (GlobRef.ConstRef (Projection.constant p)), params @ c :: acc) | c -> (c,acc) in - decrec [] + decrec [] p let decomp sigma t = let rec decrec acc c = match EConstr.kind sigma c with | App (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f - | Proj (p, c) -> (mkConst (Projection.constant p), c :: acc) + | Proj (p, c) -> + (* Hack: fake evar to generate [Everything] in the functions below *) + let hole = mkEvar (Evar.unsafe_of_int (-1), []) in + let params = List.make (Projection.npars p) hole in + (mkConst (Projection.constant p), params @ c :: acc) | Cast (c1,_,_) -> decrec acc c1 | _ -> (c,acc) in diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 20c557b282..5df9fab236 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -359,9 +359,6 @@ let e_search_auto debug (in_depth,p) lems db_list = tclIDTAC gl end -(* let e_search_auto_key = CProfile.declare_profile "e_search_auto" *) -(* let e_search_auto = CProfile.profile5 e_search_auto_key e_search_auto *) - let eauto_with_bases ?(debug=Off) np lems db_list = Hints.wrap_hint_warning (e_search_auto debug np lems db_list) diff --git a/tactics/hints.ml b/tactics/hints.ml index 5e9c3baeb1..31b276bb3e 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -320,7 +320,7 @@ let strip_params env sigma c = | App (f, args) -> (match EConstr.kind sigma f with | Const (cst,_) -> - (match Recordops.find_primitive_projection cst with + (match Structures.PrimitiveProjections.find_opt cst with | Some p -> let p = Projection.make p false in let npars = Projection.npars p in 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)) |