From 8f6aab1f4d6d60842422abc5217daac806eb0897 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 1 Nov 2016 20:53:32 +0100 Subject: Reductionops API using EConstr. --- tactics/autorewrite.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics/autorewrite.ml') diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index dae1cc9f1b..46600cdd75 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -284,7 +284,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = match find_rel ctype with | Some c -> Some c | None -> - let ctx,t' = Reductionops.splay_prod_assum env sigma ctype in (* Search for underlying eq *) + let ctx,t' = Reductionops.splay_prod_assum env sigma (EConstr.of_constr ctype) in (* Search for underlying eq *) match find_rel (it_mkProd_or_LetIn t' ctx) with | Some c -> Some c | None -> None -- cgit v1.2.3 From e27949240f5b1ee212e7d0fe3326a21a13c4abb0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Nov 2016 17:21:44 +0100 Subject: Typing API using EConstr. --- tactics/autorewrite.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tactics/autorewrite.ml') diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 46600cdd75..80b9ec06e1 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -272,7 +272,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = try let others,(c1,c2) = split_last_two args in let ty1, ty2 = - Typing.unsafe_type_of env eqclause.evd c1, Typing.unsafe_type_of env eqclause.evd c2 + Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c1), Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c2) in (* if not (evd_convertible env eqclause.evd ty1 ty2) then None *) (* else *) @@ -290,7 +290,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = | None -> None let find_applied_relation metas loc env sigma c left2right = - let ctype = Typing.unsafe_type_of env sigma c in + let ctype = Typing.unsafe_type_of env sigma (EConstr.of_constr c) in match decompose_applied_relation metas env sigma c ctype left2right with | Some c -> c | None -> -- cgit v1.2.3 From 0489e8b56d7e10f7111c0171960e25d32201b963 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 11 Nov 2016 21:55:33 +0100 Subject: Clenv API using EConstr. --- tactics/autorewrite.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'tactics/autorewrite.ml') diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 80b9ec06e1..b567344c99 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -257,12 +257,12 @@ type hypinfo = { let decompose_applied_relation metas env sigma c ctype left2right = let find_rel ty = - let eqclause = Clenv.mk_clenv_from_env env sigma None (c,ty) in + let eqclause = Clenv.mk_clenv_from_env env sigma None (EConstr.of_constr c,EConstr.of_constr ty) in let eqclause = if metas then eqclause else clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd) in - let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in + let (equiv, args) = decompose_app (EConstr.Unsafe.to_constr (Clenv.clenv_type eqclause)) in let rec split_last_two = function | [c1;c2] -> [],(c1, c2) | x::y::z -> @@ -276,7 +276,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = in (* if not (evd_convertible env eqclause.evd ty1 ty2) then None *) (* else *) - Some { hyp_cl=eqclause; hyp_prf=(Clenv.clenv_value eqclause); hyp_ty = ty; + Some { hyp_cl=eqclause; hyp_prf=EConstr.Unsafe.to_constr (Clenv.clenv_value eqclause); hyp_ty = ty; hyp_car=ty1; hyp_rel=mkApp (equiv, Array.of_list others); hyp_l2r=left2right; hyp_left=c1; hyp_right=c2; } with Not_found -> None -- cgit v1.2.3 From 3f9e56fcbf479999325a86bbdaeefd6a0be13c65 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 18 Nov 2016 20:35:01 +0100 Subject: Equality API using EConstr. --- tactics/autorewrite.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tactics/autorewrite.ml') diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index b567344c99..d656206d65 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -122,7 +122,7 @@ let autorewrite ?(conds=Naive) tac_main lbas = Tacticals.New.tclTHEN tac (one_base (fun dir c tac -> let tac = (tac, conds) in - general_rewrite dir AllOccurrences true false ~tac c) + general_rewrite dir AllOccurrences true false ~tac (EConstr.of_constr c)) tac_main bas)) (Proofview.tclUNIT()) lbas)) @@ -165,7 +165,7 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas = | _ -> assert false) (* there must be at least an hypothesis *) | _ -> assert false (* rewriting cannot complete a proof *) in - let general_rewrite_in x y z w = Proofview.V82.tactic (general_rewrite_in x y z w) in + let general_rewrite_in x y z w = Proofview.V82.tactic (general_rewrite_in x y (EConstr.of_constr z) w) in Tacticals.New.tclMAP (fun id -> Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS (List.fold_left (fun tac bas -> -- cgit v1.2.3 From 0cdb7e42f64674e246d4e24e3c725e23ceeec6bd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 21 Nov 2016 12:13:05 +0100 Subject: Reductionops now return EConstrs. --- tactics/autorewrite.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'tactics/autorewrite.ml') diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index d656206d65..0293842975 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -285,6 +285,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = | Some c -> Some c | None -> let ctx,t' = Reductionops.splay_prod_assum env sigma (EConstr.of_constr ctype) in (* Search for underlying eq *) + let t' = EConstr.Unsafe.to_constr t' in match find_rel (it_mkProd_or_LetIn t' ctx) with | Some c -> Some c | None -> None -- cgit v1.2.3 From b36adb2124d3ba8a5547605e7f89bb0835d0ab10 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Nov 2016 15:50:17 +0100 Subject: Removing some return type compatibility layers in Termops. --- tactics/autorewrite.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics/autorewrite.ml') diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 0293842975..f2e98ee011 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -286,7 +286,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = | None -> let ctx,t' = Reductionops.splay_prod_assum env sigma (EConstr.of_constr ctype) in (* Search for underlying eq *) let t' = EConstr.Unsafe.to_constr t' in - match find_rel (it_mkProd_or_LetIn t' ctx) with + match find_rel (Term.it_mkProd_or_LetIn t' ctx) with | Some c -> Some c | None -> None -- cgit v1.2.3 From 02dd160233adc784eac732d97a88356d1f0eaf9b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 25 Nov 2016 18:34:53 +0100 Subject: Removing various compatibility layers of tactics. --- tactics/autorewrite.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'tactics/autorewrite.ml') diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index f2e98ee011..f43f4b2502 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -257,7 +257,7 @@ type hypinfo = { let decompose_applied_relation metas env sigma c ctype left2right = let find_rel ty = - let eqclause = Clenv.mk_clenv_from_env env sigma None (EConstr.of_constr c,EConstr.of_constr ty) in + let eqclause = Clenv.mk_clenv_from_env env sigma None (EConstr.of_constr c,ty) in let eqclause = if metas then eqclause else clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd) @@ -274,6 +274,8 @@ let decompose_applied_relation metas env sigma c ctype left2right = let ty1, ty2 = Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c1), Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c2) in + let ty = EConstr.Unsafe.to_constr ty in + let ty1 = EConstr.Unsafe.to_constr ty1 in (* if not (evd_convertible env eqclause.evd ty1 ty2) then None *) (* else *) Some { hyp_cl=eqclause; hyp_prf=EConstr.Unsafe.to_constr (Clenv.clenv_value eqclause); hyp_ty = ty; @@ -284,9 +286,8 @@ let decompose_applied_relation metas env sigma c ctype left2right = match find_rel ctype with | Some c -> Some c | None -> - let ctx,t' = Reductionops.splay_prod_assum env sigma (EConstr.of_constr ctype) in (* Search for underlying eq *) - let t' = EConstr.Unsafe.to_constr t' in - match find_rel (Term.it_mkProd_or_LetIn t' ctx) with + let ctx,t' = Reductionops.splay_prod_assum env sigma ctype in (* Search for underlying eq *) + match find_rel (it_mkProd_or_LetIn t' ctx) with | Some c -> Some c | None -> None @@ -296,7 +297,7 @@ let find_applied_relation metas loc env sigma c left2right = | Some c -> c | None -> user_err ~loc ~hdr:"decompose_applied_relation" - (str"The type" ++ spc () ++ Printer.pr_constr_env env sigma ctype ++ + (str"The type" ++ spc () ++ Printer.pr_econstr_env env sigma ctype ++ spc () ++ str"of this term does not end with an applied relation.") (* To add rewriting rules to a base *) -- cgit v1.2.3 From 3c1cd2338fcddc4a6c0e97b0af53eb2b2f238c4a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 15 Dec 2016 10:45:19 +0100 Subject: Removing most nf_enter in tactics. Now they are useless because all of the primitives are (should?) be evar-insensitive. --- tactics/autorewrite.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics/autorewrite.ml') diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index f43f4b2502..e58ec5a31f 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -92,7 +92,7 @@ type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * Genarg. let one_base general_rewrite_maybe_in tac_main bas = let lrul = find_rewrites bas in let try_rewrite dir ctx c tc = - Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + Proofview.Goal.s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in let c' = Vars.subst_univs_level_constr subst c in -- cgit v1.2.3