Retablissement de minicoq

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

2 files changed, 21 insertions, 21 deletions

diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml
index 70d830ef5..2f248885b 100644
--- a/toplevel/fhimsg.ml
+++ b/toplevel/fhimsg.ml
@@ -100,12 +100,12 @@ let msg_bad_elimination ctx k = function
   | None -> 
       [<>]
 
-let explain_elim_arity k ctx ind aritylst c p pt okinds = 
+let explain_elim_arity k ctx ind aritylst c pj okinds = 
   let pi = P.pr_term k ctx ind in
   let ppar = prlist_with_sep pr_coma (P.pr_term k ctx) aritylst in
   let pc = P.pr_term k ctx c in
-  let pp = P.pr_term k ctx p in
-  let ppt = P.pr_term k ctx pt in
+  let pp = P.pr_term k ctx pj.uj_val in
+  let ppt = P.pr_term k ctx pj.uj_type in
   [< 'sTR "Incorrect elimination of"; 'bRK(1,1); pc; 'sPC;
      'sTR "in the inductive type"; 'bRK(1,1); pi; 'fNL;
      'sTR "The elimination predicate"; 'bRK(1,1); pp; 'sPC;
@@ -113,16 +113,16 @@ let explain_elim_arity k ctx ind aritylst c p pt okinds =
      'sTR "It should be one of :"; 'bRK(1,1) ; hOV 0 ppar; 'fNL;
      msg_bad_elimination ctx k okinds >]
 
-let explain_case_not_inductive k ctx c ct =
-  let pc = P.pr_term k ctx c in
-  let pct = P.pr_term k ctx ct in
+let explain_case_not_inductive k ctx cj =
+  let pc = P.pr_term k ctx cj.uj_val in
+  let pct = P.pr_term k ctx cj.uj_type in
   [< 'sTR "In Cases expression"; 'bRK(1,1); pc; 'sPC; 
      'sTR "has type"; 'bRK(1,1); pct; 'sPC; 
      'sTR "which is not an inductive definition" >]
   
-let explain_number_branches k ctx c ct expn =
-  let pc = P.pr_term k ctx c in
-  let pct = P.pr_term k ctx ct in
+let explain_number_branches k ctx cj expn =
+  let pc = P.pr_term k ctx cj.uj_val in
+  let pct = P.pr_term k ctx cj.uj_val in
   [< 'sTR "Cases on term"; 'bRK(1,1); pc; 'sPC ;
      'sTR "of type"; 'bRK(1,1); pct; 'sPC;
      'sTR "expects ";  'iNT expn; 'sTR " branches" >]
@@ -196,7 +196,7 @@ let explain_cant_apply_not_functional k ctx rator randl =
      'sTR" "; v 0 appl; 'fNL >]
 
 (* (co)fixpoints *)
-let explain_ill_formed_rec_body k ctx err lna i vdefs =
+let explain_ill_formed_rec_body k ctx err names i vdefs =
   let str = match err with
 
   (* Fixpoint guard errors *)
@@ -235,7 +235,7 @@ let explain_ill_formed_rec_body k ctx err lna i vdefs =
 in
   let pvd = P.pr_term k ctx vdefs.(i) in
   let s =
-    match List.nth lna i with Name id -> string_of_id id | Anonymous -> "_" in
+    match names.(i) with Name id -> string_of_id id | Anonymous -> "_" in
   [< str; 'fNL; 'sTR"The ";
      if Array.length vdefs = 1 then [<>] else [<'iNT (i+1); 'sTR "-th ">];
      'sTR"recursive definition"; 'sPC; 'sTR s;
@@ -294,12 +294,12 @@ let explain_type_error k ctx = function
       explain_bad_assumption k ctx c
   | ReferenceVariables id -> 
       explain_reference_variables id
-  | ElimArity (ind, aritylst, c, p, pt, okinds) ->
-      explain_elim_arity k ctx (mkMutInd ind) aritylst c p pt okinds 
-  | CaseNotInductive (c, ct) -> 
-      explain_case_not_inductive k ctx c ct
-  | NumberBranches (c, ct, n) -> 
-      explain_number_branches k ctx c ct n
+  | ElimArity (ind, aritylst, c, pj, okinds) ->
+      explain_elim_arity k ctx (mkMutInd ind) aritylst c pj okinds 
+  | CaseNotInductive cj -> 
+      explain_case_not_inductive k ctx cj
+  | NumberBranches (cj, n) -> 
+      explain_number_branches k ctx cj n
   | IllFormedBranch (c, i, actty, expty) -> 
       explain_ill_formed_branch k ctx c i actty expty 
   | Generalization (nvar, c) ->
diff --git a/toplevel/fhimsg.mli b/toplevel/fhimsg.mli
index 33f9f4c2b..f5c72f38a 100644
--- a/toplevel/fhimsg.mli
+++ b/toplevel/fhimsg.mli
@@ -46,13 +46,13 @@ val explain_reference_variables : identifier -> std_ppcmds
 
 val explain_elim_arity : 
   path_kind -> env -> constr -> constr list -> constr 
-    -> constr -> constr -> (constr * constr * string) option -> std_ppcmds
+    -> unsafe_judgment -> (constr * constr * string) option -> std_ppcmds
 
 val explain_case_not_inductive : 
-  path_kind -> env -> constr -> constr -> std_ppcmds
+  path_kind -> env -> unsafe_judgment -> std_ppcmds
 
 val explain_number_branches : 
-  path_kind -> env -> constr -> constr -> int -> std_ppcmds
+  path_kind -> env -> unsafe_judgment -> int -> std_ppcmds
 
 val explain_ill_formed_branch :
   path_kind -> env -> constr -> int -> constr -> constr -> std_ppcmds
@@ -65,7 +65,7 @@ val explain_actual_type :
 
 val explain_ill_formed_rec_body :
   path_kind -> env -> guard_error -> 
-    name list -> int -> constr array -> std_ppcmds
+    name array -> int -> constr array -> std_ppcmds
 
 val explain_ill_typed_rec_body  :
   path_kind -> env -> int -> name list -> unsafe_judgment array