Fixing two typos introduced in r14217 and r14223

(due to unreverted debugging stuff):
- wrong revert of betaiota flag to false in r14223
- wrong exception raised in r14217

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14224 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 2 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index d90ea6fc93..0d2b2af003 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -223,7 +223,7 @@ let default_unify_flags = {
   use_meta_bound_pattern_unification = true;
   frozen_evars = ExistentialSet.empty;
   restrict_conv_on_strict_subterms = false;
-  modulo_betaiota = false;
+  modulo_betaiota = true;
   modulo_eta = true;
   allow_K_in_toplevel_higher_order_unification = false
       (* in fact useless when not used in w_unify_to_subterm_list *)
@@ -1162,7 +1162,7 @@ let w_unify env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
 		  try
 		    w_typed_unify_list env flags hd1 l1 hd2 l2 evd
 		  with ex' when precatchable_exception ex' ->
-		    raise ex')
+		    raise ex)
 
       (* General case: try first order *)
       | _ -> w_typed_unify env cv_pb flags ty1 ty2 evd