From f7c55014aabb0d607449868e2522515db0b40568 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 1 May 2019 17:00:55 +0200 Subject: Make the check flag of conversion functions mandatory. The current situation is a mess, some functions set it by default, but other no. Making it mandatory ensures that the expected value is the correct one. --- plugins/ssrmatching/ssrmatching.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/ssrmatching') diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 1deb935d5c..4e0866a0c5 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -1299,7 +1299,7 @@ let ssrpatterntac _ist arg gl = let concl_x = EConstr.of_constr concl_x in let gl, tty = pf_type_of gl t in let concl = EConstr.mkLetIn (make_annot (Name (Id.of_string "selected")) Sorts.Relevant, t, tty, concl_x) in - Proofview.V82.of_tactic (convert_concl concl DEFAULTcast) gl + Proofview.V82.of_tactic (convert_concl ~check:true concl DEFAULTcast) gl (* Register "ssrpattern" tactic *) let () = -- cgit v1.2.3 From 6211fd6e067e781a160db8765dd87067428048f2 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 1 Nov 2018 23:26:06 +0100 Subject: Moving Evd.evars_of_term from constr to econstr + consequences. This impacts a lot of code, apparently in the good, removing several conversions back and forth constr. --- plugins/ssrmatching/ssrmatching.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/ssrmatching') diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 4e0866a0c5..e421b31227 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -544,7 +544,7 @@ let dont_impact_evars_in cl = (* - w_unify expands let-in (zeta conversion) eagerly, whereas we want to *) (* match a head let rigidly. *) let match_upats_FO upats env sigma0 ise orig_c = - let dont_impact_evars = dont_impact_evars_in orig_c in + let dont_impact_evars = dont_impact_evars_in (EConstr.of_constr orig_c) in let rec loop c = let f, a = splay_app ise c in let i0 = ref (-1) in let fpats = @@ -586,7 +586,7 @@ let match_upats_FO upats env sigma0 ise orig_c = let match_upats_HO ~on_instance upats env sigma0 ise c = - let dont_impact_evars = dont_impact_evars_in c in + let dont_impact_evars = dont_impact_evars_in (EConstr.of_constr c) in let it_did_match = ref false in let failed_because_of_TC = ref false in let rec aux upats env sigma0 ise c = -- cgit v1.2.3 From 6608f64f001f8f1a50b2dc41fefdf63c0b84b270 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 2 Nov 2018 00:17:47 +0100 Subject: Passing evar_map to evars_of_term rather than expecting the term to be evar-nf. --- plugins/ssrmatching/ssrmatching.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'plugins/ssrmatching') diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index e421b31227..adbcfb8f3b 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -529,8 +529,8 @@ exception FoundUnif of (evar_map * UState.t * tpattern) (* Note: we don't update env as we descend into the term, as the primitive *) (* unification procedure always rejects subterms with bound variables. *) -let dont_impact_evars_in cl = - let evs_in_cl = Evd.evars_of_term cl in +let dont_impact_evars_in sigma0 cl = + let evs_in_cl = Evd.evars_of_term sigma0 cl in fun sigma -> Evar.Set.for_all (fun k -> try let _ = Evd.find_undefined sigma k in true with Not_found -> false) evs_in_cl @@ -544,7 +544,7 @@ let dont_impact_evars_in cl = (* - w_unify expands let-in (zeta conversion) eagerly, whereas we want to *) (* match a head let rigidly. *) let match_upats_FO upats env sigma0 ise orig_c = - let dont_impact_evars = dont_impact_evars_in (EConstr.of_constr orig_c) in + let dont_impact_evars = dont_impact_evars_in sigma0 (EConstr.of_constr orig_c) in let rec loop c = let f, a = splay_app ise c in let i0 = ref (-1) in let fpats = @@ -586,7 +586,7 @@ let match_upats_FO upats env sigma0 ise orig_c = let match_upats_HO ~on_instance upats env sigma0 ise c = - let dont_impact_evars = dont_impact_evars_in (EConstr.of_constr c) in + let dont_impact_evars = dont_impact_evars_in sigma0 (EConstr.of_constr c) in let it_did_match = ref false in let failed_because_of_TC = ref false in let rec aux upats env sigma0 ise c = -- cgit v1.2.3