diff options
| author | Maxime Dénès | 2017-04-28 22:14:09 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-28 22:14:09 +0200 |
| commit | 4f742e14441581ece247d33020055f15732f126b (patch) | |
| tree | f28b3e927cf7715f97f3f31285e4903e426ec362 /pretyping/patternops.ml | |
| parent | 7943b1fade775af48917d54878e65b80217be038 (diff) | |
Revert "Using a more explicit algebraic type for evars of kind "MatchingVar"."
I'm sure this was pushed by accident, since testing shows immediately
that it breaks the compilation of the ssreflect plugin, hence all
developments relying on it in Travis.
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index b310da9a37..b16d044956 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 (Evar_kinds.SecondOrderPatVar id) -> Some id + Evar_kinds.MatchingVar (true,id) -> Some id | _ -> None) | _ -> None with @@ -158,11 +158,10 @@ 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 (Evar_kinds.FirstOrderPatVar id) -> - PMeta (Some id) + | Evar_kinds.MatchingVar (b,id) -> + assert (not b); 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) -> @@ -329,12 +328,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 (_,Evar_kinds.FirstOrderPatVar n) -> + | GPatVar (_,(false,n)) -> metas := n::!metas; PMeta (Some n) | GRef (_,gr,_) -> PRef (canonical_gr gr) (* Hack to avoid rewriting a complete interpretation of patterns *) - | GApp (_, GPatVar (_,Evar_kinds.SecondOrderPatVar n), cl) -> + | GApp (_, GPatVar (_,(true,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, |