diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index f2c7d0f14c..daef422981 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -985,7 +985,7 @@ let clenv_so_resolver allow_K clause gl = let clenv_unique_resolver allow_K clenv gls = let pathd,_ = whd_stack (clenv_instance_template_type clenv) in - let glhd,_ = whd_stack (pf_concl gls)in + let glhd,_ = whd_stack (pf_concl gls) in match kind_of_term pathd, kind_of_term glhd with | IsMeta _, IsLambda _ -> (try |