- let (curi,metasenv,proofbo,proofty, attrs) = proof in
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let termty,_ = TC.type_of_aux' metasenv context term CicUniv.empty_ugraph in
- let termty = CicReduction.whd context termty in
- let (termty,metasenv',arguments,fresh_meta) =
- TermUtil.saturate_term
- (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in
- let term = if arguments = [] then term else Cic.Appl (term::arguments) in
- let uri,exp_named_subst,typeno,args =
- match termty with
- C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
- | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) ->
- (uri,exp_named_subst,typeno,args)
- | _ -> raise NotAnInductiveTypeToEliminate
- in
- let paramsno,itty,patterns =
- match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
- C.InductiveDefinition (tys,_,paramsno,_),_ ->
- let _,_,itty,cl = List.nth tys typeno in
- let rec aux n context t =
- match n,CicReduction.whd context t with
- 0,C.Prod (name,source,target) ->
- let fresh_name =
- mk_fresh_name_callback metasenv' context name
- (*CSC: WRONG TYPE HERE: I can get a "bad" name*)
- ~typ:source
- in
- C.Lambda (fresh_name,C.Implicit None,
- aux 0 (Some (fresh_name,C.Decl source)::context) target)
- | n,C.Prod (name,source,target) ->
- let fresh_name =
- mk_fresh_name_callback metasenv' context name
- (*CSC: WRONG TYPE HERE: I can get a "bad" name*)
- ~typ:source
- in
- aux (n-1) (Some (fresh_name,C.Decl source)::context) target
- | 0,_ -> C.Implicit None
- | _,_ -> assert false
- in
- paramsno,itty,
- List.map (function (_,cty) -> aux paramsno context cty) cl
- | _ -> assert false
- in
- let _,right_args =
- List.fold_right
- (fun x (n,acc) -> if n > 0 then (n-1,x::acc) else (n,acc))
- args (List.length args - paramsno, [])
- in
- let outtype =
- let n_lambdas = List.length right_args + 1 in
- let lifted_ty = CicSubstitution.lift n_lambdas ty in
- let replace = ProofEngineReduction.replace_lifting
- ~equality:(ProofEngineReduction.alpha_equivalence)
- in
- let captured_ty =
- let what =
- List.map (CicSubstitution.lift n_lambdas) (right_args@[term])
- in
- let with_what =
- let rec mkargs = function
- | 0 -> []
- | 1 -> [Cic.Rel 1]
- | n -> (Cic.Implicit None)::(mkargs (n-1))
- in
- mkargs n_lambdas
- in
- replace ~what ~with_what ~where:lifted_ty
+ let (curi,metasenv,proofbo,proofty, attrs) = proof in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+ let termty,_ = TC.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+ let termty = CicReduction.whd context termty in
+ let (termty,metasenv',arguments,fresh_meta) =
+ TermUtil.saturate_term
+ (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in
+ let term = if arguments = [] then term else Cic.Appl (term::arguments) in
+ let uri,exp_named_subst,typeno,args =
+ match termty with
+ | C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
+ | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) ->
+ (uri,exp_named_subst,typeno,args)
+ | _ -> raise NotAnInductiveTypeToEliminate
+ in
+ let paramsno,itty,patterns,right_args =
+ match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
+ | C.InductiveDefinition (tys,_,paramsno,_),_ ->
+ let _,left_parameters,right_args =
+ List.fold_right
+ (fun x (n,acc1,acc2) ->
+ if n > 0 then (n-1,acc1,x::acc2) else (n,x::acc1,acc2))
+ args (List.length args - paramsno, [],[])