diff options
| author | Maxime Dénès | 2017-03-24 16:15:32 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-03-24 16:15:32 +0100 |
| commit | af291869bb7d1184d8e655906572d75937ca829b (patch) | |
| tree | 62a5ccf9ee7b115b7d1118cbc3db92c553261713 /pretyping | |
| parent | 3234a893a1b3cfd6b51f1c26cc10e9690d8a703e (diff) | |
| parent | 7535e268f7706d1dee263fdbafadf920349103db (diff) | |
Merge branch 'trunk' into pr379
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 7 | ||||
| -rw-r--r-- | pretyping/patternops.ml | 4 |
2 files changed, 8 insertions, 3 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 043616a519..85cc8762ee 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -514,8 +514,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (* Evar must be undefined since we have flushed evars *) let () = if !debug_unification then let open Pp in - Feedback.msg_notice (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ()) - ++ fnl ()) in + Feedback.msg_notice (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ())) in match (flex_kind_of_term (fst ts) env evd term1 sk1, flex_kind_of_term (fst ts) env evd term2 sk2) with | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) -> @@ -1152,6 +1151,10 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let t2 = apprec_nohdbeta ts env evd (whd_head_evar evd t2) in let (term1,l1 as appr1) = try destApp evd t1 with DestKO -> (t1, [||]) in let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in + let () = if !debug_unification then + let open Pp in + Feedback.msg_notice (v 0 (str "Heuristic:" ++ spc () ++ print_constr t1 + ++ cut () ++ print_constr t2 ++ cut ())) in let app_empty = Array.is_empty l1 && Array.is_empty l2 in match EConstr.kind evd term1, EConstr.kind evd term2 with | Evar (evk1,args1), (Rel _|Var _) when app_empty diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 823071e293..8c6b39b7e6 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -402,7 +402,9 @@ let rec pat_of_raw metas vars = function and pats_of_glob_branches loc metas vars ind brs = let get_arg = function - | PatVar(_,na) -> na + | PatVar(_,na) -> + name_iter (fun n -> metas := n::!metas) na; + na | PatCstr(loc,_,_,_) -> err ~loc (Pp.str "Non supported pattern.") in let rec get_pat indexes = function |