diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/himsg.ml | 10 | ||||
| -rw-r--r-- | toplevel/minicoq.ml | 2 |
2 files changed, 6 insertions, 6 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 04f96a8721..419488a37b 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -273,17 +273,17 @@ 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 explain_occur_check k ctx ev rhs = let id = "?" ^ string_of_int ev in - let pt = prterm rhs in + let pt = P.pr_term k ctx 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 explain_not_clean k ctx sp t = + let c = Rel (Intset.choose (free_rels t)) in let id = string_of_id (Names.basename sp) in - let var = pTERM(c) in + let var = P.pr_term k ctx c in errorlabstrm "Trad.not_clean" [< 'sTR"Tried to define "; 'sTR id; 'sTR" with a term using variable "; var; 'sPC; diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml index 7a16930698..02620168c1 100644 --- a/toplevel/minicoq.ml +++ b/toplevel/minicoq.ml @@ -10,7 +10,7 @@ open Sign open Constant open Inductive open Type_errors -open Typing +open Safe_typing open G_minicoq let (env : environment ref) = ref empty_environment |