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 /interp | |
| 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 'interp')
| -rw-r--r-- | interp/constrextern.ml | 12 | ||||
| -rw-r--r-- | interp/constrintern.ml | 4 |
2 files changed, 9 insertions, 7 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 59b8b4e5b9..bdbfd8c277 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -654,9 +654,11 @@ 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,(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,[]) + | 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,[])) | GApp (loc,f,args) -> (match f with @@ -1029,13 +1031,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,(false,n)) + | PMeta (Some n) -> GPatVar (loc,Evar_kinds.FirstOrderPatVar 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,(true,n)), + GApp (loc,GPatVar (loc,Evar_kinds.SecondOrderPatVar 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) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 94924374a8..ea1802ccfa 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1748,9 +1748,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = GHole (loc, k, naming, solve) (* Parsing pattern variables *) | CPatVar (loc, n) when pattern_mode -> - GPatVar (loc, (true,n)) + GPatVar (loc, Evar_kinds.SecondOrderPatVar n) | CEvar (loc, n, []) when pattern_mode -> - GPatVar (loc, (false,n)) + GPatVar (loc, Evar_kinds.FirstOrderPatVar n) (* end *) (* Parsing existential variables *) | CEvar (loc, n, l) -> |