diff options
| -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 d5df3bc958..d3c835be43 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -629,7 +629,7 @@ let clenv_merge with_types metas evars clenv = (clenv_wtactic (mimick_evar f (Array.length cl) evn) clenv) - | _ -> error "w_Unify") + | _ -> raise ex(********* error "w_Unify" *)) end | _ -> anomaly "clenv_resrec")) |