Nettoyage

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

4 files changed, 122 insertions, 168 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index b4cc547d1..1e3770ad0 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -449,25 +449,25 @@ let discriminable env sigma t1 t2 =
 
 let descend_then sigma env head dirn =
   let headj = unsafe_machine env sigma head in
-  let indspec =
+  let IndType (indf,_) as indt =
     try find_inductive env sigma headj.uj_type
     with Not_found -> assert false in
+  let mispec,params = dest_ind_family indf in
   let construct =
-    mkMutConstruct (ith_constructor_of_inductive indspec.mind dirn) in
-  let mispec = lookup_mind_specif indspec.mind env in
+    mkMutConstruct (ith_constructor_of_inductive(mis_inductive mispec) dirn) in
   let dirn_cty = 
     strong (fun _ _ -> whd_castapp) env sigma
-      (type_of env sigma (applist(construct,indspec.Inductive.params))) in
+      (type_of env sigma (applist(construct,params))) in
   let dirn_nlams = nb_prod dirn_cty in
   let (_,dirn_env) = add_prods_rel sigma (dirn_cty,env) in
   (dirn_nlams,
    dirn_env,
    (fun dirnval (dfltval,resty) ->
-      let aritysign,_ = get_arity env sigma indspec in
-      let p = lam_it (lift indspec.nrealargs resty) aritysign in
+      let aritysign,_ = get_arity env sigma indf in
+      let p = lam_it (lift (mis_nrealargs mispec) resty) aritysign in
       let nb_prodP = nb_prod p in
       let bty,_ =
-	type_case_branches env sigma indspec (type_of env sigma p) p head in
+	type_case_branches env sigma indt (type_of env sigma p) p head in
       let build_branch i =
 	let result = if i = dirn then dirnval else dfltval in
 	let nlams = nb_prod bty.(i-1) in
@@ -478,7 +478,7 @@ let descend_then sigma env head dirn =
 	branchval 
       in
       mkMutCase (make_default_case_info mispec) p head 
-	(List.map build_branch (interval 1 indspec.nconstr))))
+	(List.map build_branch (interval 1 (mis_nconstr mispec)))))
   
 (* Now we need to construct the discriminator, given a discriminable
    position.  This boils down to:
@@ -498,7 +498,7 @@ let descend_then sigma env head dirn =
    giving [True], and all the rest giving False. *)
 
 let construct_discriminator sigma env dirn c sort =
-  let indspec =
+  let (IndType(IndFamily (mispec,_) as indf,_) as indt) =
     try find_inductive env sigma (type_of env sigma c)
     with Not_found ->
        (* one can find Rel(k) in case of dependent constructors 
@@ -509,8 +509,7 @@ let construct_discriminator sigma env dirn c sort =
       errorlabstrm "Equality.construct_discriminator"
 	[< 'sTR "Cannot discriminate on inductive constructors with 
 		 dependent types" >] in
-  let mispec = lookup_mind_specif indspec.mind env in
-  let arsign,arsort = get_arity env sigma indspec in
+  let arsign,arsort = get_arity env sigma indf in
   let (true_0,false_0,sort_0) = 
     match necessary_elimination arsort (destSort sort) with
       | Type_Type ->
@@ -520,7 +519,7 @@ let construct_discriminator sigma env dirn c sort =
 	  build_True (), build_False (), (DOP0(Sort (Prop Null))) 
   in
   let p = lam_it sort_0 arsign in
-  let bty,_ = type_case_branches env sigma indspec (type_of env sigma p) p c in
+  let bty,_ = type_case_branches env sigma indt (type_of env sigma p) p c in
   let build_branch i =
     let nlams = nb_prod bty.(i-1) in
     let endpt = if i = dirn then true_0 else false_0 in
@@ -528,7 +527,7 @@ let construct_discriminator sigma env dirn c sort =
   in
   let build_match () =
     mkMutCase (make_default_case_info mispec) p c 
-      (List.map build_branch (interval 1 indspec.nconstr)) 
+      (List.map build_branch (interval 1 (mis_nconstr mispec)))
   in
   build_match()
     
@@ -536,19 +535,17 @@ let rec build_discriminator sigma env dirn c sort = function
   | [] -> construct_discriminator sigma env dirn c sort
   | (MutConstruct(sp,cnum),argnum)::l ->
       let cty = type_of env sigma c in
-      let indspec =
+      let IndType (indf,_) =
 	try find_inductive env sigma cty with Not_found -> assert false in
-      let _,arsort = get_arity env sigma indspec in
-      let nparams = indspec.Inductive.nparams in
+      let _,arsort = get_arity env sigma indf in
+      let nparams = mis_nparams (fst (dest_ind_family indf)) in
       let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in
       let newc = Rel(cnum_nlams-(argnum-nparams)) in
       let subval = build_discriminator sigma cnum_env dirn newc sort l  in
       (match necessary_elimination arsort (destSort sort) with
          | Type_Type ->
 	     kont subval (build_EmptyT (),DOP0(Sort(Type(dummy_univ))))
-	 | _ -> kont subval (build_False ()
-
-,DOP0(Sort(Prop Null))))
+	 | _ -> kont subval (build_False (),DOP0(Sort(Prop Null))))
   | _ -> assert false
 
 let find_eq_data_decompose eqn =
@@ -685,28 +682,7 @@ let h_discrConcl = hide_atomic_tactic "DiscrConcl" discrConcl
 let h_discrHyp   = hide_ident_tactic  "DiscrHyp"   discrHyp
 (**)
 
-(* [bind_ith na i T]
- *  will verify that T has no binders below [Rel i], and produce the
- *  term [na]T, binding [Rel i] in T.  The resulting term should be
- *  valid in the same environment as T, which means that we have to
- *  re-lift it. *)
-
-let bind_ith na i t = lift i (DLAM(na,lift (-(i-1)) t))
-(*
-let existS_term = put_squel mmk "existS"
-let sigS_term = put_squel mmk "sigS"
-let projS1_term = put_squel mmk "projS1"
-let projS2_term = put_squel mmk "projS2"
-let sigS_rec_term = put_squel mmk "sigS_rec"
-*)
 let existS_pattern = put_pat mmk "(existS ? ? ? ?)"
-(*
-let existT_term = put_squel mmk "existT"
-let sigT_term = put_squel mmk "sigT"
-let projT1_term = put_squel mmk "projT1"
-let projT2_term = put_squel mmk "projT2"
-let sigT_rect_term = put_squel mmk "sigT_rect"
-*)
 let existT_pattern = put_pat mmk "(existT ? ? ? ?)"
 
 let build_sigma_set () =
@@ -732,29 +708,27 @@ let find_sigma_data s =
     | Type _    -> build_sigma_type ()                   (* Type *)
     | Prop Null -> error "find_sigma_data"
 
-(* [make_tuple env na lind rterm rty]
-
-   If [rty] depends on lind, then we will fabricate the term
+(* [make_tuple env sigma lind rterm rty]
 
-          (existS A==[type_of(Rel lind)] P==(Lambda(type_of(Rel lind),
-                                            [bind_ith na lind rty]))
-                  [(Rel lind)] [rterm])
+   If [rty] depends on lind, then we will build the term
 
-   [The term (Lambda(type_of(Rel lind),[bind_ith na lind rty])) is
-    valid in [env] because [bind_ith] produces a term which does not
-    "change" environments.]
+     (existS A==[type_of(Rel lind)] P==(Lambda(na:type_of(Rel lind),
+                                        [rty{1/lind}]))
+              [(Rel lind)] [rterm])
 
    which should have type (sigS A P) - we can verify it by
    typechecking at the end.
  *)
 
-let make_tuple sigma env na lind rterm rty =
+let make_tuple env sigma (rterm,rty) lind =
   if dependent (Rel lind) rty then
     let {intro = exist_term; ex = sig_term} =
       find_sigma_data (get_sort_of env sigma rty) in
     let a = type_of env sigma (Rel lind) in
-    let p = DOP2(Lambda,a,
-                 bind_ith (fst(lookup_rel lind env)) lind rty) in
+    (* We replace (Rel lind) by (Rel 1) in rty then abstract on (na:a) *)
+    let rty' = substn_many [|make_substituend (Rel 1)|] lind rty in
+    let na = fst (lookup_rel lind env) in
+    let p = mkLambda na a rty' in
     (applist(exist_term,[a;p;(Rel lind);rterm]),
      applist(sig_term,[a;p]))
   else
@@ -858,18 +832,14 @@ let sig_clausale_forme env sigma sort_of_ty siglen ty (dFLT,dFLTty) =
 
  *)
 
-let make_iterated_tuple sigma env (dFLT,dFLTty) (c,cty) =
+let make_iterated_tuple env sigma (dFLT,dFLTty) (c,cty) =
   let (cty,rels) = minimal_free_rels env sigma (c,cty) in
   let sort_of_cty = get_sort_of env sigma cty in
   let sorted_rels = Sort.list (>=) (Intset.elements rels) in
   let (tuple,tuplety) =
-    List.fold_left (fun (rterm,rty) lind ->
-                      let na = fst(lookup_rel lind env) in 
-		      make_tuple sigma env na lind rterm rty)
-      (c,cty)
-      sorted_rels 
+    List.fold_left (make_tuple env sigma) (c,cty) sorted_rels 
   in
-  if not(closed0 tuplety) then failwith "make_iterated_tuple";
+  assert (closed0 tuplety);
   let dfltval = 
     sig_clausale_forme env sigma sort_of_cty (List.length sorted_rels) 
       tuplety (dFLT,dFLTty)
@@ -878,7 +848,7 @@ let make_iterated_tuple sigma env (dFLT,dFLTty) (c,cty) =
 
 let rec build_injrec sigma env (t1,t2) c = function
   | [] ->
-      make_iterated_tuple sigma env (t1,type_of env sigma t1)
+      make_iterated_tuple env sigma (t1,type_of env sigma t1)
         (c,type_of env sigma c)
   | (MutConstruct(sp,cnum),argnum)::l ->
       let cty = type_of env sigma c in
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 3341167d8..9e19a0c04 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -99,7 +99,7 @@ val dEq : clause -> tactic
 val dEqThen : (int -> tactic) -> clause -> tactic
 
 val make_iterated_tuple : 
-  'a evar_map -> env -> (constr * constr) -> (constr * constr) 
+  env -> 'a evar_map -> (constr * constr) -> (constr * constr) 
     -> constr * constr * constr
 
 val subst : constr -> clause -> tactic
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 0f2d188b4..cd8fa4926 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -9,6 +9,7 @@ open Term
 open Global
 open Sign
 open Environ
+open Inductive
 open Printer
 open Reduction
 open Retyping
@@ -83,19 +84,6 @@ let dest_match_eq gls eqn =
 	  errorlabstrm "dest_match_eq" 
 	    [< 'sTR "no primitive equality here" >]))
     
-let type_of_predicate_argument gls ity globargs =
-  let env = pf_env gls in
-  let sigma = project gls in 
-  let sort = sort_of_goal gls  in
-  let elim = Indrec.make_case_gen env sigma ity sort in
-  let type_elim = type_of env sigma elim in
-  let nparams = mind_nparams ity in
-  let (hyps,predicate,_) = named_push_and_liftl env nparams [] type_elim [] in
-  let (_,predicate,_) = lam_and_popl nparams hyps predicate [] in
-  let prod = whd_beta env Evd.empty (applist (predicate,globargs)) in
-  let (_,ty,_) = destProd prod in
-  ty
-
 let implicit = Sort implicit_sort
 
 let change_sign env (vars,rels) =
@@ -105,83 +93,80 @@ let change_sign env (vars,rels) =
        let tt = execute_type env Evd.empty t in push_rel (n,tt) env)
     env' rels
 
-let make_inv_predicate (ity,args) c dflt_concl dep_option gls =
-  let env = pf_env gls in
-  let sigma = project gls in
-  let sign = pf_hyps gls in
-  let concl = (pf_concl gls) in
-  let id = destVar c in 
-  let nparams = mind_nparams ity in
-  let (globargs,largs_init) = list_chop nparams args in
-  let arity = hnf_prod_applist env sigma "make_inv_predicate" 
-                (nf_betadeltaiota env sigma (mind_arity ity)) globargs in 
-  let len = List.length largs_init in
-  let hyps = [] in
-  let largs = List.map insert_lifted largs_init in
-  let (hyps,larg_var_list,concl,dephyp) =                   
-    if not dep_option (* (dependent (VAR id) concl) *) then 
-      (* We push de arity and leave concl unchanged *)
-      let hyps_ar,_,largs_ar = named_push_and_liftl env len hyps arity largs in
-      let larg_var_list =
-        list_map_i (fun i ai -> (extract_lifted ai,len-i+1)) 1 largs
-      in 
-      (hyps_ar,larg_var_list,concl,0)
-    else 
-      if not (dependent (VAR id) concl) then errorlabstrm "make_inv_predicate"
-        [< 'sTR "Current goal does not depend on "; print_id id >]
-      else   
-       (* We abstract the conclusion of goal with respect to args and c to be
-	* concl in order to rewrite and have c also rewritten when the case
-        * will be done *)
-        let p=type_of_predicate_argument gls ity globargs in
-        let c2 =
-          (match dflt_concl with
-             | None -> abstract_list_all gls p concl (largs_init@[c])  
-             | (Some concl) -> concl) 
-	in  
-        let hyps,_,largs =
-          named_push_lambda_and_liftl env (nb_lam c2) hyps c2 largs in     
-        let c3 = whd_beta env Evd.empty
-                   (applist (c2,Array.to_list
-                               (rel_vect (List.length largs)
-                                  (nb_prod arity +1)))) 
-	in
-        let larg_var_list =
-          list_map_i (fun i ai-> (extract_lifted ai,len-i+2)) 1 largs 
-        in 
-	(hyps,larg_var_list,c3,1)
+(* Environment management *)
+let push_rel_type sigma (na,t) env =
+  push_rel (na,make_typed t (get_sort_of env sigma t)) env
+
+let push_rels vars env =
+  List.fold_left (fun env nvar -> push_rel_type Evd.empty nvar env) env vars
+
+type inversion_status = Dep of constr option | NoDep
+
+let compute_eqn env sigma n i ai =
+  (ai,get_type_of env sigma ai),
+  (Rel (n-i),get_type_of env sigma (Rel (n-i)))
+
+let make_inv_predicate env sigma ind id status concl =
+  let indf,realargs = dest_ind_type ind in
+  let nrealargs = List.length realargs in
+  let (hyps,concl) =
+    match status with
+      | NoDep ->
+	  (* We push the arity and leave concl unchanged *)
+	  let hyps_arity,_ = get_arity env sigma indf in
+	  let env' = push_rels hyps_arity env in
+	  (hyps_arity,concl)
+      | Dep dflt_concl ->
+	  if not (dependent (VAR id) concl) then
+	    errorlabstrm "make_inv_predicate"
+              [< 'sTR "Current goal does not depend on "; print_id id >];
+          (* We abstract the conclusion of goal with respect to
+             realargs and c to * be concl in order to rewrite and have
+             c also rewritten when the case * will be done *)
+	  let pred =
+            match dflt_concl with
+              | Some concl -> concl (*assumed it's some [x1..xn,H:I(x1..xn)]C*)
+              | None ->
+		let sort = get_sort_of env sigma concl in
+		let p = make_arity env sigma true indf sort in
+		abstract_list_all env sigma p concl (realargs@[VAR id])
+	  in
+	  let hyps,_ = decompose_lam pred in
+	  let c3 =
+	    whd_beta env sigma
+	      (applist (pred,rel_list nrealargs (nrealargs +1))) 
+	  in
+
+
+		(hyps,c3)
   in
+  let n = List.length hyps in
+  let env' = push_rels hyps env in
+  let realargs' = List.map (lift n) realargs in
+  let pairs = list_map_i (compute_eqn env' sigma n) 0 realargs' in
+  let nhyps = List.length hyps in
   (* Now the arity is pushed, and we need to construct the pairs
    * ai,Rel(n-i+1) *)
   (* Now, we can recurse down this list, for each ai,(Rel k) whether to
      push <Ai>(Rel k)=ai (when   Ai is closed).
    In any case, we carry along the rest of larg_var_list *)
-  let rec build_concl hyps n = function
-      | [] ->
-          let neqns = (List.length hyps) - dephyp - len in
-	  let (hyps1,hyps2) = list_chop neqns hyps in
-          let hyps,concl,_ = prod_and_popl neqns hyps concl [] in
-	  (lam_it (prod_it concl hyps1) hyps2,neqns)
-      | (ai,k)::restlist ->
-	  let ai = lift n ai in
-	  let k = k+n in
-          let tk = (Typeops.relative (change_sign env (sign,hyps)) k).uj_type in
-          let (lhs,eqnty,rhs) =
-            if closed0 tk then 
-	      (Rel k,tk,ai)
-            else 
-	      make_iterated_tuple Evd.empty
-		(change_sign env (sign,hyps))
-		(ai,type_of env Evd.empty ai)
-		(Rel k,tk)
-	  in
-          let type_type_rhs = get_sort_of env sigma (type_of env sigma rhs) in
-          let sort = destSort (pf_type_of gls (pf_concl gls)) in 
-          let eq_term = find_eq_pattern type_type_rhs sort in
-          let eqn = applist (eq_term ,[eqnty;lhs;rhs]) in 
-	  build_concl ((Anonymous,eqn)::hyps) (n+1) restlist
+  let rec build_concl eqns n = function
+    | [] -> (prod_it concl eqns,n)
+    | ((ai,ati),(xi,ti))::restlist ->
+        let (lhs,eqnty,rhs) =
+          if closed0 ti then 
+	    (xi,ti,ai)
+          else 
+	    make_iterated_tuple env' sigma (ai,ati) (xi,ti)
+	in
+        let type_type_rhs = get_sort_of env sigma (type_of env sigma rhs) in
+        let sort = get_sort_of env sigma concl in 
+        let eq_term = find_eq_pattern type_type_rhs sort in
+        let eqn = applist (eq_term ,[eqnty;lhs;rhs]) in 
+	build_concl ((Anonymous,lift n eqn)::hyps) (n+1) restlist
   in
-  let (predicate,neqns) = build_concl hyps 0 larg_var_list in
+  let (newconcl,neqns) = build_concl hyps 0 pairs in
+  let predicate = it_lambda_name env newconcl hyps in
   (* OK - this predicate should now be usable by res_elimination_then to
      do elimination on the conclusion. *)
   (predicate,neqns)
@@ -366,25 +351,25 @@ let case_trailer othin neqns ba gl =
 	   rewrite_eqns)))
   gl
 
-let res_case_then gene thin indbinding c dflt_concl dep_option gl =
+let res_case_then gene thin indbinding id status gl =
+  let env = pf_env gl and sigma = project gl in
+  let c = VAR id in
   let (wc,kONT) = startWalk gl in
   let t = 
     strong_prodspine (fun _ _ -> pf_whd_betadeltaiota gl) 
-      (pf_env gl) (project gl) (pf_type_of gl c) in
+      env sigma (pf_type_of gl c) in
   let indclause = mk_clenv_from wc (c,t) in
   let indclause' = clenv_constrain_with_bindings indbinding indclause in
   let newc = clenv_instance_template indclause' in
-  let (ity,args) = decomp_app (clenv_instance_template_type indclause') in
-  let ity = destMutInd ity in
+  let (IndType (indf,realargs) as indt) =
+    find_inductive env sigma (clenv_instance_template_type indclause') in
   let (elim_predicate,neqns) =
-    make_inv_predicate (ity,args) c dflt_concl dep_option gl in
-  let nparams = mind_nparams ity in
-  let largs = snd (list_chop nparams args) in
+    make_inv_predicate env sigma indt id status (pf_concl gl) in
   let (cut_concl,case_tac) =
-    if dep_option & (dependent c (pf_concl gl)) then 
-      applist(elim_predicate,largs@[c]),case_then_using 
+    if status <> NoDep & (dependent c (pf_concl gl)) then 
+      applist(elim_predicate,realargs@[c]),case_then_using 
     else 
-      applist(elim_predicate,largs),case_nodep_then_using 
+      applist(elim_predicate,realargs),case_nodep_then_using 
   in
   let case_trailer_tac =
     if gene then case_trailer_gene thin neqns else case_trailer thin neqns
@@ -431,8 +416,8 @@ let wrap_inv_error id = function
   | Not_found  ->  errorlabstrm "Inv" (not_found_message [id]) 
   | e -> raise e
 
-let inv gene com dflt_concl dep_option id =
-  let inv_tac = res_case_then gene com [] (VAR id) dflt_concl dep_option in
+let inv gene com status id =
+  let inv_tac = res_case_then gene com [] id status in
   let tac =
     if com = Some true (* if Inversion_clear, clear the hypothesis *) then 
       tclTHEN inv_tac (tclTRY (clear_clause (Some id)))
@@ -455,7 +440,7 @@ let (half_inv_tac, inv_tac, inv_clear_tac) =
   let gentac =
     hide_tactic "Inv"
       (function
-	 | [ic; Identifier id] -> inv false (com_of_id ic) None false id
+	 | [ic; Identifier id] -> inv false (com_of_id ic) NoDep id
 	 | _ -> anomaly "Inv called with bad args")
   in
   ((fun id -> gentac [hinv_kind; Identifier id]),
@@ -467,7 +452,7 @@ let named_inv =
   let gentac =
     hide_tactic "NamedInv"
       (function
-	 | [ic; Identifier id] -> inv true (com_of_id ic) None false id
+	 | [ic; Identifier id] -> inv true (com_of_id ic) NoDep id
 	 | _ -> anomaly "NamedInv called with bad args")
   in 
   (fun ic id -> gentac [ic; Identifier id])
@@ -477,7 +462,7 @@ let (half_dinv_tac, dinv_tac, dinv_clear_tac) =
   let gentac =
     hide_tactic "DInv"
       (function
-	 | [ic; Identifier id] -> inv false (com_of_id ic) None true id
+	 | [ic; Identifier id] -> inv false (com_of_id ic) (Dep None) id
 	 | _ -> anomaly "DInv called with bad args")
   in
   ((fun id -> gentac [hinv_kind; Identifier id]),
@@ -492,7 +477,7 @@ let (half_dinv_with, dinv_with, dinv_clear_with) =
 	 | [ic; Identifier id; Command com] ->
              fun gls -> 
 	       inv false (com_of_id ic)
-		 (Some (pf_interp_constr gls com)) true id gls
+		 (Dep (Some (pf_interp_constr gls com))) id gls
 	 | _ -> anomaly "DInvWith called with bad args")
   in
   ((fun id com -> gentac [hinv_kind; Identifier id; Command com]),
@@ -516,7 +501,7 @@ let invIn com id ids gls =
   in
   try 
     (tclTHEN (bring_hyps (List.map in_some ids))
-       (tclTHEN (inv false com None false id)
+       (tclTHEN (inv false com NoDep id)
           (intros_replace_ids)))
     gls
   with e -> wrap_inv_error id e
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 5f789d7f8..273633975 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -144,19 +144,18 @@ let rec add_prods_sign env sigma t =
 *)
 
 let compute_first_inversion_scheme env sigma ind sort dep_option =
+  let indf,realargs = dest_ind_type ind in
   let allvars = ids_of_sign (var_context env) in
   let p = next_ident_away (id_of_string "P") allvars in
   let pty,goal =
     if dep_option  then
-      let arity = Instantiate.mis_arity (lookup_mind_specif ind.mind env) in
-      let arprods,_ = splay_prod env sigma arity in
-      let h = next_ident_away (id_of_string "H") allvars in
-      let i = applist (mkMutInd ind.mind,rel_list 0 (List.length arprods)) in
-      let pty = it_prod_name env (mkProd (Name h) i (mkSort sort)) arprods in
-      let goal = mkProd (Name h) i (applist(VAR p, ind.realargs@[Rel 1])) in
+      let pty = make_arity env sigma true indf sort in
+      let goal = 
+	mkProd Anonymous (mkAppliedInd ind) (applist(VAR p,realargs@[Rel 1]))
+      in
       pty,goal
     else
-      let i = applist (mkMutInd ind.mind,ind.Inductive.params@ind.realargs) in
+      let i = mkAppliedInd ind in
       let ivars = global_vars i in
       let revargs,ownsign =
 	sign_it