diff options
| author | Hugo Herbelin | 2017-04-28 16:15:10 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-05-31 02:04:10 +0200 |
| commit | bf3b52f6a950490ad99b032cb0b41d32cff64824 (patch) | |
| tree | f880e1ce1989cd67c06c8a29284f35fc123bec09 /interp | |
| parent | 5dd98189c6554733fe4e22401e1637330cc8a30a (diff) | |
Using a more explicit algebraic type for evars of kind "MatchingVar".
A priori considered to be a good programming style.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 10 | ||||
| -rw-r--r-- | interp/constrintern.ml | 4 |
2 files changed, 8 insertions, 6 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 4c29fc8097..5dd0783424 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -663,9 +663,11 @@ let rec extern inctx scopes vars r = | GEvar (n,l) -> extern_evar n (List.map (on_snd (extern false scopes vars)) l) - | GPatVar (b,n) -> + | GPatVar kind -> if !print_meta_as_hole then CHole (None, Misctypes.IntroAnonymous, None) else - if b then CPatVar n else CEvar (n,[]) + (match kind with + | Evar_kinds.SecondOrderPatVar n -> CPatVar n + | Evar_kinds.FirstOrderPatVar n -> CEvar (n,[])) | GApp (f,args) -> (match f with @@ -1037,13 +1039,13 @@ let rec glob_of_pat env sigma pat = CAst.make @@ match pat with with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in GVar id | PMeta None -> GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None) - | PMeta (Some n) -> GPatVar (false,n) + | PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n) | PProj (p,c) -> GApp (CAst.make @@ GRef (ConstRef (Projection.constant p),None), [glob_of_pat env sigma c]) | PApp (f,args) -> GApp (glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args) | PSoApp (n,args) -> - GApp (CAst.make @@ GPatVar (true,n), + GApp (CAst.make @@ GPatVar (Evar_kinds.SecondOrderPatVar n), List.map (glob_of_pat env sigma) args) | PProd (na,t,c) -> GProd (na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d4d8299701..4034f145ac 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1751,10 +1751,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (* Parsing pattern variables *) | CPatVar n when pattern_mode -> CAst.make ?loc @@ - GPatVar (true,n) + GPatVar (Evar_kinds.SecondOrderPatVar n) | CEvar (n, []) when pattern_mode -> CAst.make ?loc @@ - GPatVar (false,n) + GPatVar (Evar_kinds.FirstOrderPatVar n) (* end *) (* Parsing existential variables *) | CEvar (n, l) -> |