diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-05 11:22:51 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-05 12:22:45 +0100 |
| commit | 11919074c08a64e78e5a5581d744332a093850f0 (patch) | |
| tree | 4bbdfb1607844b1cf691638a7d33e1f8c760a3e9 /pretyping | |
| parent | 4e6d36c5977a874dc5adcdfb041c0a40c340e0b7 (diff) | |
Fix debugger Tactic Unification.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/unification.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 3748c7a12..a53240a1c 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -996,6 +996,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb if !debug_unification then msg_debug (str "Starting unification"); let opt = { at_top = conv_at_top; with_types = false; with_cs = true } in + try let res = if occur_meta_or_undefined_evar sigma m || occur_meta_or_undefined_evar sigma n || subterm_restriction opt flags then None @@ -1011,7 +1012,6 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb Id.Pred.is_empty dl_id && Cpred.is_empty dl_k) then error_cannot_unify env sigma (m, n) else None in - try let a = match res with | Some sigma -> sigma, ms, es | None -> unirec_rec (env,0) cv_pb opt subst m n in |