diff options
| author | Hugo Herbelin | 2017-04-28 16:15:10 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-04-28 16:40:22 +0200 |
| commit | 7943b1fade775af48917d54878e65b80217be038 (patch) | |
| tree | 1ea76a0ca0fb5b9a1c1699842268324cae4c1488 /pretyping/patternops.ml | |
| parent | 7bdfa1a4e46acf11d199a07bfca0bc59381874c3 (diff) | |
Using a more explicit algebraic type for evars of kind "MatchingVar".
A priori considered to be a good programming style.
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index b16d044956..b310da9a37 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -145,7 +145,7 @@ let pattern_of_constr env sigma t = match kind_of_term f with | Evar (evk,args) -> (match snd (Evd.evar_source evk sigma) with - Evar_kinds.MatchingVar (true,id) -> Some id + Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar id) -> Some id | _ -> None) | _ -> None with @@ -158,10 +158,11 @@ let pattern_of_constr env sigma t = pattern_of_constr env (EConstr.Unsafe.to_constr (Retyping.expand_projection env sigma p (EConstr.of_constr c) [])) | Evar (evk,ctxt) -> (match snd (Evd.evar_source evk sigma) with - | Evar_kinds.MatchingVar (b,id) -> - assert (not b); PMeta (Some id) + | Evar_kinds.MatchingVar (Evar_kinds.FirstOrderPatVar id) -> + PMeta (Some id) | Evar_kinds.GoalEvar -> PEvar (evk,Array.map (pattern_of_constr env) ctxt) + | Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false | _ -> PMeta None) | Case (ci,p,a,br) -> @@ -328,12 +329,12 @@ let rec pat_of_raw metas vars = function | GVar (_,id) -> (try PRel (List.index Name.equal (Name id) vars) with Not_found -> PVar id) - | GPatVar (_,(false,n)) -> + | GPatVar (_,Evar_kinds.FirstOrderPatVar n) -> metas := n::!metas; PMeta (Some n) | GRef (_,gr,_) -> PRef (canonical_gr gr) (* Hack to avoid rewriting a complete interpretation of patterns *) - | GApp (_, GPatVar (_,(true,n)), cl) -> + | GApp (_, GPatVar (_,Evar_kinds.SecondOrderPatVar n), cl) -> metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl) | GApp (_,c,cl) -> PApp (pat_of_raw metas vars c, |