diff options
| author | Maxime Dénès | 2017-06-05 22:09:15 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-05 22:09:15 +0200 |
| commit | 9a618ee0529f7153da1e10a8099a0b691bd13251 (patch) | |
| tree | fea027f5f8a97b0f736d553bf4c21a1d62106253 /interp/constrintern.ml | |
| parent | b91f5d1adbd039809e31b5311d06b376829de1fc (diff) | |
| parent | ccd8ab4721406991ad63c1e82a880a1f42bf065f (diff) | |
Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + a flag suspectingly renamed in a clearer way
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 190369e8fa..120258b45f 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1506,7 +1506,7 @@ let extract_explicit_arg imps args = (**********************************************************************) (* Main loop *) -let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = +let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let rec intern env = CAst.with_loc_val (fun ?loc -> function | CRef (ref,us) -> let (c,imp,subscopes,l),_ = @@ -1749,12 +1749,12 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = CAst.make ?loc @@ GHole (k, naming, solve) (* Parsing pattern variables *) - | CPatVar n when allow_patvar -> + | CPatVar n when pattern_mode -> CAst.make ?loc @@ - GPatVar (true,n) - | CEvar (n, []) when allow_patvar -> + 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) -> @@ -1944,13 +1944,13 @@ let empty_ltac_sign = { } let intern_gen kind env - ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=empty_ltac_sign) + ?(impls=empty_internalization_env) ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) c = let tmp_scope = scope_of_type_kind kind in internalize env {ids = extract_ids env; unb = false; tmp_scope = tmp_scope; scopes = []; impls = impls} - allow_patvar (ltacvars, Id.Map.empty) c + pattern_mode (ltacvars, Id.Map.empty) c let intern_constr env c = intern_gen WithoutTypeConstraint env c @@ -2023,7 +2023,7 @@ let interp_type_evars env evdref ?(impls=empty_internalization_env) c = let intern_constr_pattern env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c = let c = intern_gen (if as_type then IsType else WithoutTypeConstraint) - ~allow_patvar:true ~ltacvars env c in + ~pattern_mode:true ~ltacvars env c in pattern_of_glob_constr c let interp_notation_constr ?(impls=empty_internalization_env) nenv a = |