diff options
| -rw-r--r-- | intf/tacexpr.mli | 2 | ||||
| -rw-r--r-- | ltac/tacintern.ml | 14 | ||||
| -rw-r--r-- | ltac/tacinterp.ml | 9 | ||||
| -rw-r--r-- | ltac/tacsubst.ml | 4 | ||||
| -rw-r--r-- | printing/pptactic.ml | 2 |
5 files changed, 17 insertions, 14 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 875ad3d16..e06436d8a 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -120,7 +120,7 @@ type open_constr_expr = unit * constr_expr type open_glob_constr = unit * glob_constr_and_expr type binding_bound_vars = Id.Set.t -type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern +type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * constr_pattern type 'a delayed_open = 'a Pretyping.delayed_open = { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index a75805b4f..15589d5c4 100644 --- a/ltac/tacintern.ml +++ b/ltac/tacintern.ml @@ -325,8 +325,9 @@ let intern_constr_pattern ist ~as_type ~ltacvars pc = let metas,pat = Constrintern.intern_constr_pattern ist.genv ~as_type ~ltacvars pc in - let c = intern_constr_gen true false ist pc in - metas,(c,pat) + let (glob,_ as c) = intern_constr_gen true false ist pc in + let bound_names = Glob_ops.bound_glob_vars glob in + metas,(bound_names,c,pat) let dummy_pat = PRel 0 @@ -334,7 +335,9 @@ let intern_typed_pattern ist p = (* we cannot ensure in non strict mode that the pattern is closed *) (* keeping a constr_expr copy is too complicated and we want anyway to *) (* type it, so we remember the pattern as a glob_constr only *) - (intern_constr_gen true false ist p,dummy_pat) + let (glob,_ as c) = intern_constr_gen true false ist p in + let bound_names = Glob_ops.bound_glob_vars glob in + (bound_names,c,dummy_pat) let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = let interp_ref r = @@ -358,7 +361,8 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = let r = evaluable_of_global_reference ist.genv (VarRef id) in Inl (ArgArg (r,None)) | _ -> - Inr ((c,None),dummy_pat) in + let bound_names = Glob_ops.bound_glob_vars c in + Inr (bound_names,(c,None),dummy_pat) in (l, match p with | Inl r -> interp_ref r | Inr (CAppExpl(_,(None,r,None),[])) -> @@ -577,7 +581,7 @@ and intern_tactic_seq onlytac ist = function ist.ltacvars, TacLetIn (isrec,l,intern_tactic onlytac ist' u) | TacMatchGoal (lz,lr,lmr) -> - ist.ltacvars, TacMatchGoal(lz,lr, intern_match_rule onlytac ist lmr) + ist.ltacvars, (TacMatchGoal(lz,lr, intern_match_rule onlytac ist lmr)) | TacMatch (lz,c,lmr) -> ist.ltacvars, TacMatch (lz,intern_tactic_or_tacarg ist c,intern_match_rule onlytac ist lmr) diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 02b03b72c..9b41a276b 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -678,7 +678,7 @@ let interp_open_constr ?(expected_type=WithoutTypeConstraint) ist = let interp_pure_open_constr ist = interp_gen WithoutTypeConstraint ist false pure_open_constr_flags -let interp_typed_pattern ist env sigma (c,_) = +let interp_typed_pattern ist env sigma (_,c,_) = let sigma, c = interp_gen WithoutTypeConstraint ist true pure_open_constr_flags env sigma c in pattern_of_constr env sigma c @@ -1106,12 +1106,11 @@ let interp_context ctxt = in_gen (topwit wit_constr_context) ctxt (* Reads a pattern by substituting vars of lfun *) let use_types = false -let eval_pattern lfun ist env sigma ((glob,_),pat as c) = - let bound_names = bound_glob_vars glob in +let eval_pattern lfun ist env sigma (bvars,(glob,_),pat as c) = if use_types then - (bound_names,interp_typed_pattern ist env sigma c) + (bvars,interp_typed_pattern ist env sigma c) else - (bound_names,instantiate_pattern env sigma lfun pat) + (bvars,instantiate_pattern env sigma lfun pat) let read_pattern lfun ist env sigma = function | Subterm (b,ido,c) -> Subterm (b,ido,eval_pattern lfun ist env sigma c) diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml index 4059877b7..438219f5a 100644 --- a/ltac/tacsubst.ml +++ b/ltac/tacsubst.ml @@ -107,8 +107,8 @@ let subst_evaluable subst = let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c) -let subst_glob_constr_or_pattern subst (c,p) = - (subst_glob_constr subst c,subst_pattern subst p) +let subst_glob_constr_or_pattern subst (bvars,c,p) = + (bvars,subst_glob_constr subst c,subst_pattern subst p) let subst_redexp subst = Miscops.map_red_expr_gen diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 631cb4c57..7949bafcb 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1188,7 +1188,7 @@ module Make let pr_and_constr_expr pr (c,_) = pr c - let pr_pat_and_constr_expr pr ((c,_),_) = pr c + let pr_pat_and_constr_expr pr (_,(c,_),_) = pr c let pr_glob_tactic_level env n t = let glob_printers = |