diff options
| author | filliatr | 1999-12-01 08:03:06 +0000 |
|---|---|---|
| committer | filliatr | 1999-12-01 08:03:06 +0000 |
| commit | dda7c7bb0b6ea0c2106459d8ae208eff0dfd6738 (patch) | |
| tree | 21bd3b1535e2e9b9cfcfa0f8cab47817a1769b70 /toplevel | |
| parent | 8b882c1ab5a31eea35eec89f134238dd17b945c2 (diff) | |
- Typing -> Safe_typing
- proofs/Typing_ev -> pretyping/Typing
- env -> sign
- fonctions var_context
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@167 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |