diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-18 11:52:10 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-18 11:52:10 +0000 |
| commit | 1c4bf87e00721d7c9eb94eff25ebdb5b69b7df4b (patch) | |
| tree | be663a4917d71d5e504bbce9a9ab7b5c405372de /tactics | |
| parent | d6be54f07b42c765f760a52c2ea06986386bcc8f (diff) | |
zeta flag added to reduce LetIns in a morphism type. Morphisms with local
definitions in their types are now accepted.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6232 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/setoid_replace.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 54c961ed3..43d25b6ea 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -753,7 +753,7 @@ let new_morphism m signature id hook = else let env = Global.env() in let typeofm = Typing.type_of env Evd.empty m in - let typ = nf_betaiota typeofm in + let typ = clos_norm_flags Closure.betaiotazeta empty_env Evd.empty typeofm in let argsrev, output = decompose_prod typ in let args_ty = List.rev argsrev in let args_ty_len = List.length (args_ty) in |