Suppression de Abst

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

5 files changed, 53 insertions, 5 deletions

diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml
index c37aa6ff1a..bee6f074a9 100644
--- a/toplevel/fhimsg.ml
+++ b/toplevel/fhimsg.ml
@@ -190,7 +190,43 @@ 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 str lna i vdefs =
+let explain_ill_formed_rec_body k ctx err lna i vdefs =
+  let str = match err with
+
+  (* Fixpoint guard errors *)
+  | NotEnoughAbstractionInFixBody ->
+      [< 'sTR "Not enough abstractions in the definition" >]
+  | RecursionNotOnInductiveType ->
+      [< 'sTR "Recursive definition on a non inductive type" >]
+  | RecursionOnIllegalTerm ->
+      [< 'sTR "Recursive call applied to an illegal term" >]
+  | NotEnoughArgumentsForFixCall ->
+      [< 'sTR "Not enough arguments for the recursive call" >]
+
+  (* CoFixpoint guard errors *)
+  (* TODO : récupérer le contexte des termes pour pouvoir les afficher *)
+  | CodomainNotInductiveType c ->
+      [< 'sTR "The codomain is"; 'sPC; P.pr_term k ctx c; 'sPC;
+	 'sTR "which should be a coinductive type" >]
+  | NestedRecursiveOccurrences ->
+      [< 'sTR "Nested recursive occurrences" >]
+  | UnguardedRecursiveCall c ->
+      [< 'sTR "Unguarded recursive call" >]
+  | RecCallInTypeOfAbstraction c ->
+      [< 'sTR "Not allowed recursive call in the domain of an abstraction" >]
+  | RecCallInNonRecArgOfConstructor c ->
+      [< 'sTR "Not allowed recursive call in a non-recursive argument of constructor" >]
+  | RecCallInTypeOfDef c ->
+      [< 'sTR "Not allowed recursive call in the type of a recursive definition" >]
+  | RecCallInCaseFun c ->
+      [< 'sTR "Not allowed recursive call in a branch of cases" >]
+  | RecCallInCaseArg c -> 
+      [< 'sTR "Not allowed recursive call in the argument of cases" >]
+  | RecCallInCasePred c ->
+      [< 'sTR "Not allowed recursive call in the type of cases in" >]
+  | NotGuardedForm ->
+      [< 'sTR "Definition not in guarded form" >]
+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
diff --git a/toplevel/fhimsg.mli b/toplevel/fhimsg.mli
index ad0e7e6646..0ba0e73a70 100644
--- a/toplevel/fhimsg.mli
+++ b/toplevel/fhimsg.mli
@@ -57,7 +57,7 @@ val explain_actual_type :
   path_kind -> env -> constr -> constr -> constr -> std_ppcmds
 
 val explain_ill_formed_rec_body :
-  path_kind -> env -> std_ppcmds -> 
+  path_kind -> env -> guard_error -> 
     name list -> int -> constr array -> std_ppcmds
 
 val explain_ill_typed_rec_body  :
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index f33633517a..a6e63497d0 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -335,8 +335,8 @@ let explain_type_error k ctx = function
       explain_cant_apply_not_functional k ctx rator randl
   | IllFormedRecBody (i, lna, vdefj, vargs) ->
       explain_ill_formed_rec_body k ctx i lna vdefj vargs
-  | IllTypedRecBody (i, lna, vdefj, vargs) ->
-      explain_ill_typed_rec_body k ctx i lna vdefj vargs
+  | IllTypedRecBody (i, lna, vdefj, vargs) -> 
+     explain_ill_typed_rec_body k ctx i lna vdefj vargs
   | NotInductive c ->
       explain_not_inductive k ctx c
   | MLCase (mes,c,ct,br,brt) ->
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index 0395b94d95..ab55fe549a 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -26,6 +26,17 @@ let lookup_var id =
 let args sign = 
   Array.of_list (List.map (fun id -> VAR id) (ids_of_var_context sign))
 
+let rec globalize bv c = match kind_of_term c with
+  | IsVar id -> lookup_var id bv
+  | IsConst (sp, _) ->
+      let cb = lookup_constant sp !env in mkConst (sp, args cb.const_hyps)
+  | IsMutInd (sp,_ as spi, _) ->
+      let mib = lookup_mind sp !env in mkMutInd (spi, args mib.mind_hyps)
+  | IsMutConstruct ((sp,_),_ as spc, _) ->
+      let mib = lookup_mind sp !env in mkMutConstruct (spc, args mib.mind_hyps)
+  | _ -> map_constr_with_binders (fun na l -> na::l) globalize bv c
+
+(*
 let rec globalize bv = function
   | VAR id -> lookup_var id bv
   | DOP1 (op,c) -> DOP1 (op, globalize bv c)
@@ -43,6 +54,7 @@ let rec globalize bv = function
   | CPrd(n,t,c)   -> CPrd (n, globalize bv t, globalize (n::bv) c)
   | CLet(n,b,t,c) -> CLet (n,globalize bv b,globalize bv t,globalize (n::bv) c)
   | Rel _ | DOP0 _ as c -> c
+*)
 
 let check c = 
   let c = globalize [] c in
diff --git a/toplevel/record.ml b/toplevel/record.ml
index f3169a066a..30f7dbdee8 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -134,7 +134,7 @@ let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) =
 		      (Some PrintLet) [| RegularPat |] in
 	   let proj = mk_LambdaCit newps 
 			(mkLambda (x, rp1,
-				   mkMutCaseA ci p (Rel 1) [|branch|])) in
+				   mkMutCase (ci, p, Rel 1, [|branch|]))) in
 	   let ok = 
 	     try
 	       let cie =