portage modules Evarconv et Evarutil

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

1 files changed, 16 insertions, 0 deletions

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 53b35ff6d..04f96a872 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -273,4 +273,20 @@ let explain_refiner_cannot_applt k ctx t harg =
        P.pr_term k ctx t; 'sPC; 'sTR"could not be applied to"; 'bRK(1,1);
        P.pr_term k ctx harg >]
 
+let error_occur_check ev rhs =
+  let id = "?" ^ string_of_int ev in
+  let pt = prterm rhs in
+  errorlabstrm "Trad.occur_check"
+    [< 'sTR"Occur check failed: tried to define "; 'sTR id;
+      'sTR" with term"; 'bRK(1,1); pt >]
+
+let error_not_clean sp t =
+  let c = Rel (List.hd (Listset.elements(free_rels t))) in
+  let id = string_of_id (Names.basename sp) in
+  let var = pTERM(c) in
+  errorlabstrm "Trad.not_clean"
+    [< 'sTR"Tried to define "; 'sTR id;
+       'sTR" with a term using variable "; var; 'sPC;
+       'sTR"which is not in its scope." >]
+
 end