diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacintern.ml | 3 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
2 files changed, 3 insertions, 2 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index c601c623de..ad62e6015f 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -347,8 +347,9 @@ let intern_binding_name ist x = let intern_constr_gen allow_patvar isarity {ltacvars=lfun; gsigma=sigma; 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.OfType None in let c' = - warn (Constrintern.intern_gen isarity ~allow_patvar ~ltacvars:(fst lfun,[]) sigma env) c + warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars:(fst lfun,[]) sigma env) c in (c',if !strict_check then None else Some c) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 3de8395258..221f2c6f4e 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -465,7 +465,7 @@ let interp_gen kind ist allow_patvar expand_evar fail_evar use_classes env sigma intros/lettac/inversion hypothesis names *) | Some c -> let ltacdata = (List.map fst ltacvars,unbndltacvars) in - intern_gen (kind = IsType) ~allow_patvar ~ltacvars:ltacdata sigma env c + intern_gen kind ~allow_patvar ~ltacvars:ltacdata sigma env c in let trace = push_trace (dloc,LtacConstrInterp (c,vars)) ist.trace in let evdc = |