From 08e2c28ee98c6a5d235cc9b84bc5690dd9a22666 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 1 Jun 2000 20:51:48 +0000 Subject: Mise en place d'un choix constr/typed_type en remplacement de certains Cast git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@485 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/himsg.ml | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) (limited to 'toplevel/himsg.ml') diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index b824c20ab..28df858fd 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -97,7 +97,7 @@ let explain_ill_formed_branch k ctx c i actty expty = let explain_generalization k ctx (name,var) c = let ctx = make_all_name_different ctx in let pe = pr_ne_env [< 'sTR"in environment" >] k ctx in - let pv = prterm_env ctx (body_of_type var) in + let pv = prtype_env ctx var in let pc = prterm_env (add_rel (name,var) ctx) c in [< 'sTR"Illegal generalization: "; pe; 'fNL; 'sTR"Cannot generalize"; 'bRK(1,1); pv; 'sPC; @@ -118,14 +118,12 @@ let explain_actual_type k ctx c ct pt = let explain_cant_apply_bad_type k ctx (n,exptyp,actualtyp) rator randl = let ctx = make_all_name_different ctx in let pe = pr_ne_env [< 'sTR"in environment" >] k ctx in - let pr = prterm_env ctx rator.uj_val in - let prt = prterm_env ctx rator.uj_type in + let pr,prt = prjudge_env ctx rator in let term_string = if List.length randl > 1 then "terms" else "term" in let many = match n mod 10 with 1 -> "st" | 2 -> "nd" | _ -> "th" in let appl = prlist_with_sep pr_fnl (fun c -> - let pc = prterm_env ctx c.uj_val in - let pct = prterm_env ctx c.uj_type in + let pc,pct = prjudge_env ctx c in hOV 2 [< pc; 'sPC; 'sTR": " ; pct >]) randl in [< 'sTR"Illegal application (Type Error): "; pe; 'fNL; @@ -141,12 +139,12 @@ let explain_cant_apply_not_functional k ctx rator randl = let ctx = make_all_name_different ctx in let pe = pr_ne_env [< 'sTR"in environment" >] k ctx in let pr = prterm_env ctx rator.uj_val in - let prt = prterm_env ctx rator.uj_type in + let prt = prterm_env ctx (body_of_type rator.uj_type) in let term_string = if List.length randl > 1 then "terms" else "term" in let appl = prlist_with_sep pr_fnl (fun c -> let pc = prterm_env ctx c.uj_val in - let pct = prterm_env ctx c.uj_type in + let pct = prterm_env ctx (body_of_type c.uj_type) in hOV 2 [< pc; 'sPC; 'sTR": " ; pct >]) randl in [< 'sTR"Illegal application (Non-functional construction): "; pe; 'fNL; @@ -167,8 +165,7 @@ let explain_ill_formed_rec_body k ctx str lna i vdefs = 'sTR "is not well-formed" >] let explain_ill_typed_rec_body k ctx i lna vdefj vargs = - let pvd = prterm_env ctx (vdefj.(i)).uj_val in - let pvdt = prterm_env ctx (vdefj.(i)).uj_type in + let pvd,pvdt = prjudge_env ctx (vdefj.(i)) in let pv = prterm_env ctx (body_of_type vargs.(i)) in [< 'sTR"The " ; if Array.length vdefj = 1 then [<>] else [<'iNT (i+1); 'sTR "-th">]; -- cgit v1.2.3