Made the subterm finding function make_abstraction independent of the

proof engine. Moved it to unification.ml.

1 files changed, 19 insertions, 0 deletions

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 90e358828..d251b571c 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -637,6 +637,24 @@ let explain_type_error env sigma err =
   | UnsatisfiedConstraints cst ->
       explain_unsatisfied_constraints env cst
 
+let pr_position (cl,pos) =
+  let clpos = match cl with
+    | None -> str " of the goal"
+    | Some (id,Locus.InHyp) -> str " of hypothesis " ++ pr_id id
+    | Some (id,Locus.InHypTypeOnly) -> str " of the type of hypothesis " ++ pr_id id
+    | Some (id,Locus.InHypValueOnly) -> str " of the body of hypothesis " ++ pr_id id in
+  int pos ++ clpos
+
+let explain_cannot_unify_occurrences env nested (cl2,pos2,t2) (cl1,pos1,t1) =
+  let s = if nested then "Found nested occurrences of the pattern"
+    else "Found incompatible occurrences of the pattern" in
+  str s ++ str ":" ++
+  spc () ++ str "Matched term " ++ pr_lconstr_env env t2 ++
+  strbrk " at position " ++ pr_position (cl2,pos2) ++
+  strbrk " is not compatible with matched term " ++
+  pr_lconstr_env env t1 ++ strbrk " at position " ++ 
+  pr_position (cl1,pos1) ++ str "."
+
 let explain_pretype_error env sigma err =
   let env = Evarutil.env_nf_betaiotaevar sigma env in
   let env = make_all_name_different env in
@@ -669,6 +687,7 @@ let explain_pretype_error env sigma err =
   | AbstractionOverMeta (m,n) -> explain_abstraction_over_meta env m n
   | NonLinearUnification (m,c) -> explain_non_linear_unification env m c
   | TypingError t -> explain_type_error env sigma t
+  | CannotUnifyOccurrences (b,c1,c2) -> explain_cannot_unify_occurrences env b c1 c2
 
 (* Module errors *)