From 4e84e83911c1cf7613a35b921b1e68e097f84b5a Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 20:11:47 +0200 Subject: Remove unused [open] statements --- pretyping/patternops.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'pretyping/patternops.ml') diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index b16d044956..33a68589c1 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -20,7 +20,6 @@ open Mod_subst open Misctypes open Decl_kinds open Pattern -open Evd open Environ let case_info_pattern_eq i1 i2 = -- cgit v1.2.3 From 68fb8e13c44c5ee95dbc9256b1d74c7c83303d2d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 28 Apr 2017 16:30:45 +0200 Subject: Fixing #5487 (v8.5 regression on ltac-matching expressions with evars). The fix follows an invariant enforced in proofview.ml on the kind of evars that are goals or that occur in goals. One day, evar kinds will need a little cleaning... --- pretyping/patternops.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'pretyping/patternops.ml') diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 2090aad8a0..75d3ed30ba 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -160,7 +160,9 @@ let pattern_of_constr env sigma t = let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in let () = ignore (pattern_of_constr env ty) in assert (not b); PMeta (Some id) - | Evar_kinds.GoalEvar -> + | Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ -> + (* These are the two evar kinds used for existing goals *) + (* see Proofview.mark_in_evm *) PEvar (evk,Array.map (pattern_of_constr env) ctxt) | _ -> let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in -- cgit v1.2.3 From db28e827d21658797418c320d566fb99570b44b6 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 28 Apr 2017 22:20:35 +0200 Subject: Revert "Fixing #5487 (v8.5 regression on ltac-matching expressions with evars)." One day I'll get bored of spending my nights fixing commits that were pushed without being tested, and I'll ask for removal of push rights. But for now let's pretend I haven't insisted enough: ~~~~ PLEASE TEST YOUR COMMITS BEFORE PUSHING ~~~~ Thank you! --- pretyping/patternops.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'pretyping/patternops.ml') diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 75d3ed30ba..2090aad8a0 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -160,9 +160,7 @@ let pattern_of_constr env sigma t = let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in let () = ignore (pattern_of_constr env ty) in assert (not b); PMeta (Some id) - | Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ -> - (* These are the two evar kinds used for existing goals *) - (* see Proofview.mark_in_evm *) + | Evar_kinds.GoalEvar -> PEvar (evk,Array.map (pattern_of_constr env) ctxt) | _ -> let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in -- cgit v1.2.3 From c3aec655a8a33fff676c79e12888d193cc2e237b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 1 May 2017 16:58:38 +0200 Subject: Fixing #5487 (v8.5 regression on ltac-matching expressions with evars). The fix follows an invariant enforced in proofview.ml on the kind of evars that are goals or that occur in goals. One day, evar kinds will need a little cleaning... PS: This is a second attempt, completing db28e82 which was missing the case PEvar in constr_matching.ml. Indeed the attached fix to #5487 alone made #2602 failing, revealing that the real cause for #2602 was actually not fixed and that if the test for #2602 was working it was because of #5487 hiding the real problem in #2602. --- pretyping/patternops.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'pretyping/patternops.ml') diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 2090aad8a0..75d3ed30ba 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -160,7 +160,9 @@ let pattern_of_constr env sigma t = let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in let () = ignore (pattern_of_constr env ty) in assert (not b); PMeta (Some id) - | Evar_kinds.GoalEvar -> + | Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ -> + (* These are the two evar kinds used for existing goals *) + (* see Proofview.mark_in_evm *) PEvar (evk,Array.map (pattern_of_constr env) ctxt) | _ -> let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in -- cgit v1.2.3 From 5c68b57c37c23a3b7b2afe4f6ff073568c7b8db9 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 19 May 2017 12:20:19 +0200 Subject: Fixing an extra bug with pattern_of_constr. Ensure in type constr_pattern that those preexisting existential variables of the goal which do not contribute as pattern variables are expanded: constr_pattern is not observed up to evar expansion (like EConstr does), so we need to pre-normalize defined evars in patterns to that matching against an EConstr works. --- pretyping/patternops.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'pretyping/patternops.ml') diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index a22db1407b..638e12d7c1 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -155,14 +155,15 @@ let pattern_of_constr env sigma t = | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp)) | Proj (p, c) -> pattern_of_constr env (EConstr.Unsafe.to_constr (Retyping.expand_projection env sigma p (EConstr.of_constr c) [])) - | Evar (evk,ctxt) -> + | Evar (evk,ctxt as ev) -> (match snd (Evd.evar_source evk sigma) with | Evar_kinds.MatchingVar (b,id) -> assert (not b); PMeta (Some id) | Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ -> (* These are the two evar kinds used for existing goals *) (* see Proofview.mark_in_evm *) - PEvar (evk,Array.map (pattern_of_constr env) ctxt) + if Evd.is_defined sigma evk then pattern_of_constr env (Evd.existential_value sigma ev) + else PEvar (evk,Array.map (pattern_of_constr env) ctxt) | _ -> PMeta None) | Case (ci,p,a,br) -> -- cgit v1.2.3