diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 687bf32c62..632bf3a62d 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -183,7 +183,7 @@ let clenv_assign mv rhs clenv = else clenv else - let st = (ConvUpToEta 0,TypeNotProcessed) in + let st = (Conv,TypeNotProcessed) in {clenv with evd = meta_assign mv (rhs_fls.rebus,st) clenv.evd} with Not_found -> error "clenv_assign: undefined meta" @@ -439,7 +439,7 @@ let clenv_assign_binding clenv k c = let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in let c_typ = nf_betaiota clenv.evd (clenv_get_type_of clenv c) in let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in - { clenv' with evd = meta_assign k (c,(UserGiven,status)) clenv'.evd } + { clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd } let clenv_match_args bl clenv = if bl = [] then |