diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-04-28 22:14:09 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-04-28 22:14:09 +0200 |
| commit | 4f742e14441581ece247d33020055f15732f126b (patch) | |
| tree | f28b3e927cf7715f97f3f31285e4903e426ec362 /interp/constrextern.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 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index bdbfd8c27..59b8b4e5b 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -654,11 +654,9 @@ let rec extern inctx scopes vars r = | GEvar (loc,n,l) -> extern_evar loc n (List.map (on_snd (extern false scopes vars)) l) - | GPatVar (loc,kind) -> - if !print_meta_as_hole then CHole (loc, None, Misctypes.IntroAnonymous, None) else - (match kind with - | Evar_kinds.SecondOrderPatVar n -> CPatVar (loc,n) - | Evar_kinds.FirstOrderPatVar n -> CEvar (loc,n,[])) + | GPatVar (loc,(b,n)) -> + if !print_meta_as_hole then CHole (loc, None, Misctypes.IntroAnonymous, None) else + if b then CPatVar (loc,n) else CEvar (loc,n,[]) | GApp (loc,f,args) -> (match f with @@ -1031,13 +1029,13 @@ let rec glob_of_pat env sigma = function with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in GVar (loc,id) | PMeta None -> GHole (loc,Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None) - | PMeta (Some n) -> GPatVar (loc,Evar_kinds.FirstOrderPatVar n) + | PMeta (Some n) -> GPatVar (loc,(false,n)) | PProj (p,c) -> GApp (loc,GRef (loc, ConstRef (Projection.constant p),None), [glob_of_pat env sigma c]) | PApp (f,args) -> GApp (loc,glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args) | PSoApp (n,args) -> - GApp (loc,GPatVar (loc,Evar_kinds.SecondOrderPatVar n), + GApp (loc,GPatVar (loc,(true,n)), List.map (glob_of_pat env sigma) args) | PProd (na,t,c) -> GProd (loc,na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c) |