diff options
| author | herbelin | 2012-11-17 03:09:23 +0000 |
|---|---|---|
| committer | herbelin | 2012-11-17 03:09:23 +0000 |
| commit | 35846ec22445e14cb044ef3beb62f5c559d94752 (patch) | |
| tree | 283e8cc0a05b3f1722dadaabc900341ee63499ed /tactics | |
| parent | beca7a2c11d6521bd9eec7bb0eb5d77a345f99ef (diff) | |
Taking into account the type of a definition (if it exists), and the
type in "cast" to activate the temporary interpretation scope.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15978 85f007b7-540e-0410-9357-904b9bb8a0f7
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 = |