diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-26 12:15:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-28 16:39:54 +0200 |
| commit | 7bdfa1a4e46acf11d199a07bfca0bc59381874c3 (patch) | |
| tree | f28b3e927cf7715f97f3f31285e4903e426ec362 /plugins/ltac | |
| parent | 66a68a4329ce199f25184ba8b2d98b4679e7ddae (diff) | |
Renaming allow_patvar flag of intern_gen into pattern_mode.
This highlights that this is a binary mode changing the interpretation
of "?x" rather than additionally allowing patvar.
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/tacintern.ml | 4 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 3f83f104e..db47a9857 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -198,7 +198,7 @@ let intern_binding_name ist x = and if a term w/o ltac vars, check the name is indeed quantified *) x -let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env} c = +let intern_constr_gen pattern_mode isarity {ltacvars=lfun; genv=env} c = let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in let ltacvars = { @@ -206,7 +206,7 @@ let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env} c = ltac_bound = Id.Set.empty; } in let c' = - warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars env) c + warn (Constrintern.intern_gen scope ~pattern_mode ~ltacvars env) c in (c',if !strict_check then None else Some c) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 50f43931e..2d5dc5821 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -597,7 +597,7 @@ let interp_uconstr ist env sigma = function } in { closure ; term = intern_gen WithoutTypeConstraint ~ltacvars env ce } -let interp_gen kind ist allow_patvar flags env sigma (c,ce) = +let interp_gen kind ist pattern_mode flags env sigma (c,ce) = let constrvars = extract_ltac_constr_context ist env sigma in let vars = { Pretyping.ltac_constrs = constrvars.typed; @@ -624,7 +624,7 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) = } in let kind_for_intern = match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in - intern_gen kind_for_intern ~allow_patvar ~ltacvars env c + intern_gen kind_for_intern ~pattern_mode ~ltacvars env c in (* Jason Gross: To avoid unnecessary modifications to tacinterp, as suggested by Arnaud Spiwack, we run push_trace immediately. We do |