Correction du bug #1273 (problème avec les paramètres non récursivement uniformes dans le cas de types mutuellement inductifs)

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

2 files changed, 203 insertions, 202 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 4187b8bd66..11264a9e38 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -411,34 +411,34 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i indlc =
   (* check the inductive types occur positively in [c] *)
   let rec check_pos (env, n, ntypes, ra_env as ienv) nmr c = 
     let x,largs = decompose_app (whd_betadeltaiota env c) in
-    match kind_of_term x with
-      | Prod (na,b,d) ->
-	  assert (largs = []);
-          (match weaker_noccur_between env n ntypes b with
-              None -> failwith_non_pos_list n ntypes [b]
-            | Some b ->
-	        check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d)
-      | Rel k ->
-           (try let (ra,rarg) = List.nth ra_env (k-1) in 
-		let nmr1 =
-	       (match ra with
-                 Mrec _ -> compute_rec_par ienv hyps nmr largs
-		  |  _ -> nmr)
-		in 
-		  if not (List.for_all (noccur_between n ntypes) largs)
-	          then failwith_non_pos_list n ntypes largs
-		  else (nmr1,rarg)
-            with Failure _ | Invalid_argument _ -> (nmr,mk_norec))
-      | Ind ind_kn ->
-          (* If the inductive type being defined appears in a
-             parameter, then we have an imbricated type *)
-          if List.for_all (noccur_between n ntypes) largs then (nmr,mk_norec)
-          else check_positive_imbr ienv nmr (ind_kn, largs)
-      | err -> 
-	  if noccur_between n ntypes x &&
-             List.for_all (noccur_between n ntypes) largs 
-	  then (nmr,mk_norec)
-	  else failwith_non_pos_list n ntypes (x::largs)
+      match kind_of_term x with
+	| Prod (na,b,d) ->
+	    assert (largs = []);
+            (match weaker_noccur_between env n ntypes b with
+		None -> failwith_non_pos_list n ntypes [b]
+              | Some b ->
+	          check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d)
+	| Rel k ->
+            (try let (ra,rarg) = List.nth ra_env (k-1) in 
+	    let nmr1 =
+	      (match ra with
+                  Mrec _ -> compute_rec_par ienv hyps nmr largs
+		|  _ -> nmr)
+	    in 
+	      if not (List.for_all (noccur_between n ntypes) largs)
+	      then failwith_non_pos_list n ntypes largs
+	      else (nmr1,rarg)
+              with Failure _ | Invalid_argument _ -> (nmr,mk_norec))
+	| Ind ind_kn ->
+            (* If the inductive type being defined appears in a
+               parameter, then we have an imbricated type *)
+            if List.for_all (noccur_between n ntypes) largs then (nmr,mk_norec)
+            else check_positive_imbr ienv nmr (ind_kn, largs)
+	| err -> 
+	    if noccur_between n ntypes x &&
+              List.for_all (noccur_between n ntypes) largs 
+	    then (nmr,mk_norec)
+	    else failwith_non_pos_list n ntypes (x::largs)
 
   (* accesses to the environment are not factorised, but is it worth? *)
   and check_positive_imbr (env,n,ntypes,ra_env as ienv) nmr (mi, largs) =
@@ -447,69 +447,69 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i indlc =
     let (lpar,auxlargs) =
       try list_chop auxnpar largs 
       with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in 
-    (* If the inductive appears in the args (non params) then the
-       definition is not positive. *)
-    if not (List.for_all (noccur_between n ntypes) auxlargs) then
-      raise (IllFormedInd (LocalNonPos n));
-    (* We do not deal with imbricated mutual inductive types *)
-    let auxntyp = mib.mind_ntypes in 
-    if auxntyp <> 1 then raise (IllFormedInd (LocalNonPos n));
-    (* The nested inductive type with parameters removed *)
-    let auxlcvect = abstract_mind_lc env auxntyp auxnpar mip.mind_nf_lc in
-    (* Extends the environment with a variable corresponding to
-       the inductive def *)
-    let (env',_,_,_ as ienv') = ienv_push_inductive ienv (mi,lpar) in
-    (* Parameters expressed in env' *)
-    let lpar' = List.map (lift auxntyp) lpar in
-    let irecargs_nmr = 
-      (* fails if the inductive type occurs non positively *)
-      (* when substituted *) 
-      Array.map 
-	(function c -> 
-	  let c' = hnf_prod_applist env' c lpar' in 
-	  check_constructors ienv' false nmr c') 
-	auxlcvect
-    in
-    let irecargs = Array.map snd irecargs_nmr
-    and nmr' = array_min nmr irecargs_nmr
-    in 
-    (nmr',(Rtree.mk_rec [|mk_paths (Imbr mi) irecargs|]).(0))
-  
+      (* If the inductive appears in the args (non params) then the
+	 definition is not positive. *)
+      if not (List.for_all (noccur_between n ntypes) auxlargs) then
+	raise (IllFormedInd (LocalNonPos n));
+      (* We do not deal with imbricated mutual inductive types *)
+      let auxntyp = mib.mind_ntypes in 
+	if auxntyp <> 1 then raise (IllFormedInd (LocalNonPos n));
+	(* The nested inductive type with parameters removed *)
+	let auxlcvect = abstract_mind_lc env auxntyp auxnpar mip.mind_nf_lc in
+	  (* Extends the environment with a variable corresponding to
+	     the inductive def *)
+	let (env',_,_,_ as ienv') = ienv_push_inductive ienv (mi,lpar) in
+	  (* Parameters expressed in env' *)
+	let lpar' = List.map (lift auxntyp) lpar in
+	let irecargs_nmr = 
+	  (* fails if the inductive type occurs non positively *)
+	  (* when substituted *) 
+	  Array.map 
+	    (function c -> 
+	      let c' = hnf_prod_applist env' c lpar' in 
+		check_constructors ienv' false nmr c') 
+	    auxlcvect
+	in
+	let irecargs = Array.map snd irecargs_nmr
+	and nmr' = array_min nmr irecargs_nmr
+	in 
+	  (nmr',(Rtree.mk_rec [|mk_paths (Imbr mi) irecargs|]).(0))
+	    
   (* check the inductive types occur positively in the products of C, if
      check_head=true, also check the head corresponds to a constructor of
      the ith type *) 
-
+	    
   and check_constructors ienv check_head nmr c = 
     let rec check_constr_rec (env,n,ntypes,ra_env as ienv) nmr lrec c = 
       let x,largs = decompose_app (whd_betadeltaiota env c) in
-      match kind_of_term x with
-
-        | Prod (na,b,d) -> 
-	    assert (largs = []);
-            let nmr',recarg = check_pos ienv nmr b in 
-            let ienv' = ienv_push_var ienv (na,b,mk_norec) in
-	    check_constr_rec ienv' nmr' (recarg::lrec) d
-
-	| hd ->
-	    if check_head then
-	      if hd = Rel (n+ntypes-i-1) then
-		check_correct_par ienv hyps (ntypes-i) largs
+	match kind_of_term x with
+
+          | Prod (na,b,d) -> 
+	      assert (largs = []);
+              let nmr',recarg = check_pos ienv nmr b in 
+              let ienv' = ienv_push_var ienv (na,b,mk_norec) in
+		check_constr_rec ienv' nmr' (recarg::lrec) d
+		  
+	  | hd ->
+	      if check_head then
+		if hd = Rel (n+ntypes-i-1) then
+		  check_correct_par ienv hyps (ntypes-i) largs
+		else
+		  raise (IllFormedInd LocalNotConstructor)
 	      else
-		raise (IllFormedInd LocalNotConstructor)
-	    else
-	      if not (List.for_all (noccur_between n ntypes) largs)
+		if not (List.for_all (noccur_between n ntypes) largs)
               then raise (IllFormedInd (LocalNonPos n));
-	    (nmr,List.rev lrec)
+	      (nmr,List.rev lrec)
     in check_constr_rec ienv nmr [] c
   in
   let irecargs_nmr =
-     Array.map
+    Array.map
       (fun c ->
         let _,rawc = mind_extract_params lparams c in
-        try
-	  check_constructors ienv true nmr rawc
-        with IllFormedInd err -> 
-	  explain_ind_err (ntypes-i) env lparams c err)
+          try
+	    check_constructors ienv true nmr rawc
+          with IllFormedInd err -> 
+	    explain_ind_err (ntypes-i) env lparams c err)
       indlc
   in
   let irecargs = Array.map snd irecargs_nmr
@@ -526,7 +526,7 @@ let check_positivity env_ar params inds =
     let ra_env =
       list_tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in
     let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
-    check_positivity_one ienv params i lc 
+      check_positivity_one ienv params i lc 
   in
   let irecargs_nmr = Array.mapi check_one inds in 
   let irecargs = Array.map snd irecargs_nmr
@@ -597,61 +597,61 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
     let consnrealargs =
       Array.map (fun (d,_) -> rel_context_length d - rel_context_length params)
 	splayed_lc in
-    (* Elimination sorts *)
+      (* Elimination sorts *)
     let arkind,kelim = match ar_kind with
-    | Inr (param_levels,lev) ->
-	Polymorphic {
-	  poly_param_levels = param_levels;
-	  poly_level = lev; 
-	}, all_sorts
-    | Inl ((issmall,isunit),ar,s) ->
-	let isunit = isunit && ntypes = 1 && not (is_recursive recargs.(0)) in
-	let kelim = allowed_sorts issmall isunit s in
-	Monomorphic {
-	  mind_user_arity = ar;
-	  mind_sort = s; 
-	}, kelim in
+      | Inr (param_levels,lev) ->
+	  Polymorphic {
+	      poly_param_levels = param_levels;
+	      poly_level = lev; 
+	    }, all_sorts
+      | Inl ((issmall,isunit),ar,s) ->
+	  let isunit = isunit && ntypes = 1 && not (is_recursive recargs.(0)) in
+	  let kelim = allowed_sorts issmall isunit s in
+	    Monomorphic {
+		mind_user_arity = ar;
+		mind_sort = s; 
+	      }, kelim in
     let nconst, nblock = ref 0, ref 0 in 
     let transf num =
       let arity = List.length (dest_subterms recarg).(num) in
-      if arity = 0 then 
-	let p  = (!nconst, 0) in
-	incr nconst; p
-      else 
-	let p = (!nblock + 1, arity) in
-	incr nblock; p
-     (* les tag des constructeur constant commence a 0,
-	les tag des constructeur non constant a 1 (0 => accumulator) *)
+	if arity = 0 then 
+	  let p  = (!nconst, 0) in
+	    incr nconst; p
+	else 
+	  let p = (!nblock + 1, arity) in
+	    incr nblock; p
+	      (* les tag des constructeur constant commence a 0,
+		 les tag des constructeur non constant a 1 (0 => accumulator) *)
     in 
     let rtbl = Array.init (List.length cnames) transf in
-    (* Build the inductive packet *)
-    { mind_typename = id;
-      mind_arity = arkind;
-      mind_arity_ctxt = ar_sign;
-      mind_nrealargs = rel_context_nhyps ar_sign - nparamargs;
-      mind_kelim = kelim;
-      mind_consnames = Array.of_list cnames;
-      mind_consnrealdecls = consnrealargs;
-      mind_user_lc = lc;
-      mind_nf_lc = nf_lc;
-      mind_recargs = recarg;
-      mind_nb_constant = !nconst;
-      mind_nb_args = !nblock;
-      mind_reloc_tbl = rtbl;
-    } in
+      (* Build the inductive packet *)
+      { mind_typename = id;
+	mind_arity = arkind;
+	mind_arity_ctxt = ar_sign;
+	mind_nrealargs = rel_context_nhyps ar_sign - nparamargs;
+	mind_kelim = kelim;
+	mind_consnames = Array.of_list cnames;
+	mind_consnrealdecls = consnrealargs;
+	mind_user_lc = lc;
+	mind_nf_lc = nf_lc;
+	mind_recargs = recarg;
+	mind_nb_constant = !nconst;
+	mind_nb_args = !nblock;
+	mind_reloc_tbl = rtbl;
+      } in
   let packets = array_map2 build_one_packet inds recargs in
-  (* Build the mutual inductive *)
-  { mind_record = isrecord;
-    mind_ntypes = ntypes;
-    mind_finite = isfinite;
-    mind_hyps = hyps;
-    mind_nparams = nparamargs;
-    mind_nparams_rec = nmr;  
-    mind_params_ctxt = params;
-    mind_packets = packets;
-    mind_constraints = cst;
-    mind_equiv = None;
-  }
+    (* Build the mutual inductive *)
+    { mind_record = isrecord;
+      mind_ntypes = ntypes;
+      mind_finite = isfinite;
+      mind_hyps = hyps;
+      mind_nparams = nparamargs;
+      mind_nparams_rec = nmr;  
+      mind_params_ctxt = params;
+      mind_packets = packets;
+      mind_constraints = cst;
+      mind_equiv = None;
+    }
 
 (************************************************************************)
 (************************************************************************)
@@ -662,5 +662,5 @@ let check_inductive env mie =
   (* Then check positivity conditions *)
   let (nmr,recargs) = check_positivity env_ar params inds in
   (* Build the inductive packets *)
-  build_inductive env env_ar params mie.mind_entry_record mie.mind_entry_finite
-    inds nmr recargs cst
+    build_inductive env env_ar params mie.mind_entry_record mie.mind_entry_finite
+      inds nmr recargs cst
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index f3e3b6d2c5..abd49ee4b7 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -275,19 +275,18 @@ let mis_make_indrec env sigma listdepkind mib =
     Array.create mib.mind_ntypes (None : (bool * constr) option) in 
   let _ = 
     let rec 
-      assign k = function 
-	| [] -> ()
-        | (indi,mibi,mipi,dep,_)::rest -> 
-            (Array.set depPvec (snd indi) (Some(dep,mkRel k));
-             assign (k-1) rest)
+	assign k = function 
+	  | [] -> ()
+          | (indi,mibi,mipi,dep,_)::rest -> 
+              (Array.set depPvec (snd indi) (Some(dep,mkRel k));
+               assign (k-1) rest)
     in 
-    assign nrec listdepkind in 
+      assign nrec listdepkind in 
   let recargsvec =
     Array.map (fun mip -> mip.mind_recargs) mib.mind_packets in
- (* recarg information for non recursive parameters *)
+  (* recarg information for non recursive parameters *)
   let rec recargparn l n = 
-    if n = 0 then l else recargparn (mk_norec::l) (n-1) 
-  in
+    if n = 0 then l else recargparn (mk_norec::l) (n-1) in
   let recargpar = recargparn [] (nparams-nparrec) in
   let make_one_rec p =
     let makefix nbconstruct =
@@ -296,97 +295,97 @@ let mis_make_indrec env sigma listdepkind mib =
 	    let tyi = snd indi in
 	    let nctyi =
               Array.length mipi.mind_consnames in (* nb constructeurs du type*)
-
+	      
             (* arity in the context of the fixpoint, i.e.
-                P1..P_nrec f1..f_nbconstruct *)
+               P1..P_nrec f1..f_nbconstruct *)
 	    let args = extended_rel_list (nrec+nbconstruct) lnamesparrec in
 	    let indf = make_ind_family(indi,args) in
-
+	      
 	    let arsign,_ = get_arity env indf in
 	    let depind = build_dependent_inductive env indf in
 	    let deparsign = (Anonymous,None,depind)::arsign in
-	    
+	      
 	    let nonrecpar = rel_context_length lnonparrec in
 	    let larsign = rel_context_length deparsign in
 	    let ndepar = larsign - nonrecpar in
 	    let dect = larsign+nrec+nbconstruct in
-
-              (* constructors in context of the Cases expr, i.e.
-         P1..P_nrec f1..f_nbconstruct F_1..F_nrec a_1..a_nar x:I *)
+	      
+            (* constructors in context of the Cases expr, i.e.
+               P1..P_nrec f1..f_nbconstruct F_1..F_nrec a_1..a_nar x:I *)
 	    let args' = extended_rel_list (dect+nrec) lnamesparrec in
 	    let args'' = extended_rel_list ndepar lnonparrec in
             let indf' = make_ind_family(indi,args'@args'') in
-
+	      
 	    let branches = 
 	      let constrs = get_constructors env indf' in
 	      let fi = rel_vect (dect-i-nctyi) nctyi in
 	      let vecfi = Array.map 
-			    (fun f -> appvect (f,extended_rel_vect ndepar lnonparrec))
-			    fi 
+		(fun f -> appvect (f,extended_rel_vect ndepar lnonparrec))
+		fi 
 	      in
-	      array_map3
-		(make_rec_branch_arg env sigma 
-		   (nparrec,depPvec,larsign))
-                vecfi constrs (dest_subterms recargsvec.(tyi)) 
+		array_map3
+		  (make_rec_branch_arg env sigma 
+		      (nparrec,depPvec,larsign))
+                  vecfi constrs (dest_subterms recargsvec.(tyi)) 
 	    in
-
+	      
 	    let j = (match depPvec.(tyi) with 
-		       | Some (_,c) when isRel c -> destRel c 
-		       | _ -> assert false) 
+	      | Some (_,c) when isRel c -> destRel c 
+	      | _ -> assert false) 
 	    in
-
-	      (* Predicate in the context of the case *)
-
+	      
+	    (* Predicate in the context of the case *)
+	      
 	    let depind' = build_dependent_inductive env indf' in
 	    let arsign',_ = get_arity env indf' in
 	    let deparsign' = (Anonymous,None,depind')::arsign' in
-
+	      
 	    let pargs =
 	      let nrpar = extended_rel_list (2*ndepar) lnonparrec 
 	      and nrar = if dep then extended_rel_list 0 deparsign'
-	      else extended_rel_list 1 arsign'
+		else extended_rel_list 1 arsign'
 	      in nrpar@nrar
-
+		
 	    in
 
-		(* body of i-th component of the mutual fixpoint *)
+	    (* body of i-th component of the mutual fixpoint *)
 	    let deftyi = 
 	      let ci = make_default_case_info env RegularStyle indi in
 	      let concl = applist (mkRel (dect+j+ndepar),pargs) in 
 	      let pred =
 		it_mkLambda_or_LetIn_name env 
 		  ((if dep then mkLambda_name env else mkLambda)
-		   (Anonymous,depind',concl))
+		      (Anonymous,depind',concl))
 		  arsign'
 	      in
-	      it_mkLambda_or_LetIn_name env
-		(mkCase (ci, pred, 
-		             mkRel 1,
-			     branches))
-		(lift_rel_context nrec deparsign)
+		it_mkLambda_or_LetIn_name env
+		  (mkCase (ci, pred, 
+		          mkRel 1,
+			  branches))
+		  (lift_rel_context nrec deparsign)
 	    in
-
+	      
 	    (* type of i-th component of the mutual fixpoint *)
-
+	      
 	    let typtyi =
-	    let concl = 
-	      let pargs = if dep then extended_rel_vect 0 deparsign
-	      else extended_rel_vect 1 arsign
-	      in appvect (mkRel (nbconstruct+ndepar+nonrecpar+j),pargs)
-	    in it_mkProd_or_LetIn_name env
+	      let concl = 
+		let pargs = if dep then extended_rel_vect 0 deparsign
+		  else extended_rel_vect 1 arsign
+		in appvect (mkRel (nbconstruct+ndepar+nonrecpar+j),pargs)
+	      in it_mkProd_or_LetIn_name env
 		concl
 		deparsign
 	    in
-	    mrec (i+nctyi) (rel_context_nhyps arsign ::ln) (typtyi::ltyp) 
-                 (deftyi::ldef) rest
+	      mrec (i+nctyi) (rel_context_nhyps arsign ::ln) (typtyi::ltyp) 
+                (deftyi::ldef) rest
         | [] -> 
 	    let fixn = Array.of_list (List.rev ln) in
             let fixtyi = Array.of_list (List.rev ltyp) in
             let fixdef = Array.of_list (List.rev ldef) in 
             let names = Array.create nrec (Name(id_of_string "F")) in
-	    mkFix ((fixn,p),(names,fixtyi,fixdef))
+	      mkFix ((fixn,p),(names,fixtyi,fixdef))
       in 
-	      mrec 0 [] [] [] 
+	mrec 0 [] [] [] 
     in 
     let rec make_branch env i = function 
       | (indi,mibi,mipi,dep,_)::rest ->
@@ -404,44 +403,46 @@ let mis_make_indrec env sigma listdepkind mib =
 		type_rec_branch
                   true dep env sigma (vargs,depPvec,i+j) tyi cs recarg
 	      in 
-	      mkLambda_string "f" p_0
-		(onerec (push_rel (Anonymous,None,p_0) env) (j+1))
+		mkLambda_string "f" p_0
+		  (onerec (push_rel (Anonymous,None,p_0) env) (j+1))
 	  in onerec env 0
       | [] -> 
 	  makefix i listdepkind
-    in 
+    in
     let rec put_arity env i = function 
       | (indi,_,_,dep,kinds)::rest -> 
 	  let indf = make_ind_family (indi,extended_rel_list i lnamesparrec) in
 	  let typP = make_arity env dep indf (new_sort_in_family kinds) in
-	  mkLambda_string "P" typP
-	    (put_arity (push_rel (Anonymous,None,typP) env) (i+1) rest)
+	    mkLambda_string "P" typP
+	      (put_arity (push_rel (Anonymous,None,typP) env) (i+1) rest)
       | [] -> 
 	  make_branch env 0 listdepkind 
-    in 
-
-      (* Body on make_one_rec *)
+    in
+      
+    (* Body on make_one_rec *)
     let (indi,mibi,mipi,dep,kind) = List.nth listdepkind p in
-
-    if mis_is_recursive_subset
-      (List.map (fun (indi,_,_,_,_) -> snd indi) listdepkind)
-      mipi.mind_recargs
-    then 
-    let env' = push_rel_context lnamesparrec env in
-      it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind) 
-	lnamesparrec
-    else 
-      mis_make_case_com (Some dep) env sigma indi (mibi,mipi) kind 
+      
+      if (mis_is_recursive_subset
+	(List.map (fun (indi,_,_,_,_) -> snd indi) listdepkind)
+	mipi.mind_recargs) 
+	(* mis_is_recursive_subset do not care about mutually recursive calls so: *)
+	|| (nparams-nparrec > 0)
+      then 
+	let env' = push_rel_context lnamesparrec env in
+	  it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind) 
+	    lnamesparrec
+      else 
+	mis_make_case_com (Some dep) env sigma indi (mibi,mipi) kind 
   in 
-      (* Body of mis_make_indrec *)
-  list_tabulate make_one_rec nrec
+    (* Body of mis_make_indrec *)
+    list_tabulate make_one_rec nrec
 
 (**********************************************************************)
 (* This builds elimination predicate for Case tactic *)
 
 let make_case_com depopt env sigma ity kind =
   let (mib,mip) = lookup_mind_specif env ity in 
-  mis_make_case_com depopt env sigma ity (mib,mip) kind
+    mis_make_case_com depopt env sigma ity (mib,mip) kind
 
 let make_case_dep env   = make_case_com (Some true) env
 let make_case_nodep env = make_case_com (Some false) env 
@@ -460,7 +461,7 @@ let change_sort_arity sort =
     | Sort _ -> mkSort sort
     | _ -> assert false
   in 
-  drec 
+    drec 
 
 (* [npar] is the number of expected arguments (then excluding letin's) *)
 let instantiate_indrec_scheme sort =
@@ -536,7 +537,7 @@ let build_indrec env sigma ind =
   let (mib,mip) = lookup_mind_specif env ind in
   let kind = inductive_sort_family mip in
   let dep = kind <> InProp in
-  List.hd (mis_make_indrec env sigma [(ind,mib,mip,dep,kind)] mib)
+    List.hd (mis_make_indrec env sigma [(ind,mib,mip,dep,kind)] mib)
 
 (**********************************************************************)
 (* To handle old Case/Match syntax in Pretyping                       *)