aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml38
-rw-r--r--plugins/funind/functional_principles_types.ml70
-rw-r--r--plugins/funind/g_indfun.ml413
-rw-r--r--plugins/funind/glob_term_to_relation.ml76
-rw-r--r--plugins/funind/glob_termops.ml9
-rw-r--r--plugins/funind/indfun.ml41
-rw-r--r--plugins/funind/indfun_common.ml13
-rw-r--r--plugins/funind/indfun_common.mli2
-rw-r--r--plugins/funind/invfun.ml69
-rw-r--r--plugins/funind/merge.ml14
-rw-r--r--plugins/funind/recdef.ml101
-rw-r--r--plugins/funind/recdef.mli6
12 files changed, 248 insertions, 204 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f06d8fa53f..a3af23dcda 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -124,11 +124,13 @@ let finish_proof dynamic_infos g =
let refine c =
- Tacmach.refine_no_check c
+ Tacmach.refine c
let thin l =
Tacmach.thin_no_check l
+let eq_constr u v = eq_constr_nounivs u v
+
let is_trivial_eq t =
let res = try
begin
@@ -205,7 +207,7 @@ let prove_trivial_eq h_id context (constructor,type_of_term,term) =
let find_rectype env c =
- let (t, l) = decompose_app (Reduction.whd_betaiotazeta c) in
+ let (t, l) = decompose_app (Reduction.whd_betaiotazeta env c) in
match kind_of_term t with
| Ind ind -> (t, l)
| Construct _ -> (t,l)
@@ -233,7 +235,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
failwith "NoChange";
end
in
- let eq_constr = Reductionops.is_conv env sigma in
+ let eq_constr = Evarconv.e_conv env (ref sigma) in
if not (noccurn 1 end_of_type)
then nochange "dependent"; (* if end_of_type depends on this term we don't touch it *)
if not (isApp t) then nochange "not an equality";
@@ -325,7 +327,8 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
let all_ids = pf_ids_of_hyps g in
let new_ids,_ = list_chop ctxt_size all_ids in
let to_refine = applist(witness_fun,List.rev_map mkVar new_ids) in
- refine to_refine g
+ let evm, _ = pf_apply Typing.e_type_of g to_refine in
+ tclTHEN (Refiner.tclEVARS evm) (refine to_refine) g
)
in
let simpl_eq_tac =
@@ -633,8 +636,11 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
( (* we instanciate the hyp if possible *)
fun g ->
let prov_hid = pf_get_new_id hid g in
+ let c = mkApp(mkVar hid,args) in
+ let evm, _ = pf_apply Typing.e_type_of g c in
tclTHENLIST[
- Proofview.V82.of_tactic (pose_proof (Name prov_hid) (mkApp(mkVar hid,args)));
+ Refiner.tclEVARS evm;
+ Proofview.V82.of_tactic (pose_proof (Name prov_hid) c);
thin [hid];
rename_hyp [prov_hid,hid]
] g
@@ -757,6 +763,7 @@ let build_proof
begin
match kind_of_term f with
| App _ -> assert false (* we have collected all the app in decompose_app *)
+ | Proj _ -> assert false (*FIXME*)
| Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ | Sort _ | Prod _ ->
let new_infos =
{ dyn_infos with
@@ -764,7 +771,7 @@ let build_proof
}
in
build_proof_args do_finalize new_infos g
- | Const c when not (List.mem_f Constant.equal c fnames) ->
+ | Const (c,_) when not (List.mem_f Constant.equal c fnames) ->
let new_infos =
{ dyn_infos with
info = (f,args)
@@ -809,6 +816,7 @@ let build_proof
| Fix _ | CoFix _ ->
error ( "Anonymous local (co)fixpoints are not handled yet")
+ | Proj _ -> error "Prod"
| Prod _ -> error "Prod"
| LetIn _ ->
let new_infos =
@@ -938,7 +946,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
(* observe (str "nb_args := " ++ str (string_of_int nb_args)); *)
(* observe (str "nb_params := " ++ str (string_of_int nb_params)); *)
(* observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *)
- let f_def = Global.lookup_constant (destConst f) in
+ let f_def = Global.lookup_constant (fst (destConst f)) in
let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in
let f_body = Option.get (body_of_constant f_def)
in
@@ -956,10 +964,10 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in
(* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *)
let type_ctxt,type_of_f = decompose_prod_n_assum (nb_params + nb_args)
- (Typeops.type_of_constant_type (Global.env()) f_def.const_type) in
+ ((*FIXME*)f_def.const_type) in
let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in
let lemma_type = it_mkProd_or_LetIn eqn type_ctxt in
- let f_id = Label.to_id (con_label (destConst f)) in
+ let f_id = Label.to_id (con_label (fst (destConst f))) in
let prove_replacement =
tclTHENSEQ
[
@@ -978,8 +986,8 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
Ensures by: obvious
i*)
(mk_equation_id f_id)
- (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
- lemma_type
+ (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem))
+ (lemma_type, (*FIXME*) Univ.ContextSet.empty)
(fun _ _ -> ());
ignore (Pfedit.by (Proofview.V82.tactic prove_replacement));
Lemmas.save_proof (Vernacexpr.Proved(false,None))
@@ -990,10 +998,10 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
let equation_lemma =
try
- let finfos = find_Function_infos (destConst f) in
+ let finfos = find_Function_infos (fst (destConst f)) (*FIXME*) in
mkConst (Option.get finfos.equation_lemma)
with (Not_found | Option.IsNone as e) ->
- let f_id = Label.to_id (con_label (destConst f)) in
+ let f_id = Label.to_id (con_label (fst (destConst f))) in
(*i The next call to mk_equation_id is valid since we will construct the lemma
Ensures by: obvious
i*)
@@ -1002,7 +1010,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
let _ =
match e with
| Option.IsNone ->
- let finfos = find_Function_infos (destConst f) in
+ let finfos = find_Function_infos (fst (destConst f)) in
update_Function
{finfos with
equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with
@@ -1306,7 +1314,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
in
let fname = destConst (fst (decompose_app (List.hd (List.rev pte_args)))) in
tclTHENSEQ
- [unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef fname)];
+ [unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst fname))];
let do_prove =
build_proof
interactive_proof
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index d6f21fb86b..2adc825056 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -106,14 +106,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
let pre_princ = substl (List.map mkVar ptes_vars) pre_princ in
let is_dom c =
match kind_of_term c with
- | Ind((u,_)) -> MutInd.equal u rel_as_kn
- | Construct((u,_),_) -> MutInd.equal u rel_as_kn
+ | Ind((u,_),_) -> MutInd.equal u rel_as_kn
+ | Construct(((u,_),_),_) -> MutInd.equal u rel_as_kn
| _ -> false
in
let get_fun_num c =
match kind_of_term c with
- | Ind(_,num) -> num
- | Construct((_,num),_) -> num
+ | Ind((_,num),_) -> num
+ | Construct(((_,num),_),_) -> num
| _ -> assert false
in
let dummy_var = mkVar (Id.of_string "________") in
@@ -251,8 +251,10 @@ let change_property_sort toSort princ princName =
let princ_info = compute_elim_sig princ in
let change_sort_in_predicate (x,v,t) =
(x,None,
- let args,_ = decompose_prod t in
- compose_prod args (mkSort toSort)
+ let args,ty = decompose_prod t in
+ let s = destSort ty in
+ Global.add_constraints (Univ.enforce_leq (univ_of_sort toSort) (univ_of_sort s) Univ.Constraint.empty);
+ compose_prod args (mkSort toSort)
)
in
let princName_as_constr = Constrintern.global_reference princName in
@@ -292,8 +294,8 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
begin
Lemmas.start_proof
new_princ_name
- (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
- new_principle_type
+ (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem))
+ (new_principle_type, (*FIXME*) Univ.ContextSet.empty)
hook
;
(* let _tim1 = System.get_time () in *)
@@ -315,7 +317,7 @@ let generate_functional_principle
try
let f = funs.(i) in
- let type_sort = Termops.new_sort_in_family InType in
+ let type_sort = Universes.new_sort_in_family InType in
let new_sorts =
match sorts with
| None -> Array.make (Array.length funs) (type_sort)
@@ -334,18 +336,23 @@ let generate_functional_principle
then
(* let id_of_f = Label.to_id (con_label f) in *)
let register_with_sort fam_sort =
- let s = Termops.new_sort_in_family fam_sort in
+ let s = Universes.new_sort_in_family fam_sort in
let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
let value = change_property_sort s new_principle_type new_princ_name in
(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
- let ce = {
- const_entry_body = Future.from_val (value,Declareops.no_seff);
- const_entry_secctx = None;
- const_entry_type = None;
- const_entry_opaque = false;
- const_entry_inline_code = false;
- const_entry_feedback = None;
- } in
+ let ce =
+ { const_entry_body =
+ Future.from_val (value,Declareops.no_seff);
+ const_entry_secctx = None;
+ const_entry_type = None;
+ const_entry_polymorphic = false;
+ const_entry_universes = Univ.UContext.empty (*FIXME*);
+ const_entry_proj = None;
+ const_entry_opaque = false;
+ const_entry_feedback = None;
+ const_entry_inline_code = false
+ }
+ in
ignore(
Declare.declare_constant
name
@@ -488,19 +495,20 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
List.map
(fun (idx) ->
let ind = first_fun_kn,idx in
- ind,true,prop_sort
+ (ind,Univ.Instance.empty)(*FIXME*),true,prop_sort
)
funs_indexes
in
+ let sigma, schemes =
+ Indrec.build_mutual_induction_scheme env sigma ind_list
+ in
let l_schemes =
- List.map
- (Typing.type_of env sigma)
- (Indrec.build_mutual_induction_scheme env sigma ind_list)
+ List.map (Typing.type_of env sigma) schemes
in
let i = ref (-1) in
let sorts =
List.rev_map (fun (_,x) ->
- Termops.new_sort_in_family (Pretyping.interp_elimination_sort x)
+ Universes.new_sort_in_family (Pretyping.interp_elimination_sort x)
)
fas
in
@@ -649,10 +657,10 @@ let build_case_scheme fa =
(* Constrintern.global_reference id *)
(* in *)
let funs = (fun (_,f,_) ->
- try Globnames.constr_of_global (Nametab.global f)
+ try Universes.constr_of_global (Nametab.global f)
with Not_found ->
Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in
- let first_fun = destConst funs in
+ let first_fun,u = destConst funs in
let funs_mp,funs_dp,_ = Names.repr_con first_fun in
let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in
@@ -664,16 +672,18 @@ let build_case_scheme fa =
let prop_sort = InProp in
let funs_indexes =
let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
- List.assoc_f Constant.equal (destConst funs) this_block_funs_indexes
+ List.assoc_f Constant.equal (fst (destConst funs)) this_block_funs_indexes
in
let ind_fun =
let ind = first_fun_kn,funs_indexes in
- ind,prop_sort
+ (ind,Univ.Instance.empty)(*FIXME*),prop_sort
in
- let scheme_type = (Typing.type_of env sigma ) ((fun (ind,sf) -> Indrec.build_case_analysis_scheme_default env sigma ind sf) ind_fun) in
+ let sigma, scheme =
+ (fun (ind,sf) -> Indrec.build_case_analysis_scheme_default env sigma ind sf) ind_fun in
+ let scheme_type = (Typing.type_of env sigma ) scheme in
let sorts =
(fun (_,_,x) ->
- Termops.new_sort_in_family (Pretyping.interp_elimination_sort x)
+ Universes.new_sort_in_family (Pretyping.interp_elimination_sort x)
)
fa
in
@@ -690,6 +700,6 @@ let build_case_scheme fa =
(Some princ_name)
this_block_funs
0
- (prove_princ_for_struct false 0 [|destConst funs|])
+ (prove_princ_for_struct false 0 [|fst (destConst funs)|])
in
()
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 2dd78d8908..3802aa3659 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -307,8 +307,11 @@ let rec hdMatchSub inu (test: constr -> bool) : fapp_info list =
max_rel = max_rel; onlyvars = List.for_all isVar args }
::subres
+let make_eq () =
+(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ())
+
let mkEq typ c1 c2 =
- mkApp (Coqlib.build_coq_eq(),[| typ; c1; c2|])
+ mkApp (make_eq(),[| typ; c1; c2|])
let poseq_unsafe idunsafe cstr gl =
@@ -463,10 +466,10 @@ VERNAC COMMAND EXTEND MergeFunind CLASSIFIED AS SIDEFF
[ "Mergeschemes" "(" ident(id1) ne_ident_list(cl1) ")"
"with" "(" ident(id2) ne_ident_list(cl2) ")" "using" ident(id) ] ->
[
- let f1 = Constrintern.interp_constr Evd.empty (Global.env())
- (CRef (Libnames.Ident (Loc.ghost,id1))) in
- let f2 = Constrintern.interp_constr Evd.empty (Global.env())
- (CRef (Libnames.Ident (Loc.ghost,id2))) in
+ let f1,ctx = Constrintern.interp_constr Evd.empty (Global.env())
+ (CRef (Libnames.Ident (Loc.ghost,id1),None)) in
+ let f2,ctx' = Constrintern.interp_constr Evd.empty (Global.env())
+ (CRef (Libnames.Ident (Loc.ghost,id2),None)) in
let f1type = Typing.type_of (Global.env()) Evd.empty f1 in
let f2type = Typing.type_of (Global.env()) Evd.empty f2 in
let ar1 = List.length (fst (decompose_prod f1type)) in
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index dd02dfe8d1..4544f736ca 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -333,8 +333,8 @@ let raw_push_named (na,raw_value,raw_typ) env =
match na with
| Anonymous -> env
| Name id ->
- let value = Option.map (Pretyping.understand Evd.empty env) raw_value in
- let typ = Pretyping.understand Evd.empty env ~expected_type:Pretyping.IsType raw_typ in
+ let value = Option.map (fun x-> fst (Pretyping.understand Evd.empty env x)) raw_value in
+ let typ,ctx = Pretyping.understand Evd.empty env ~expected_type:Pretyping.IsType raw_typ in
Environ.push_named (id,value,typ) env
@@ -350,7 +350,7 @@ let add_pat_variables pat typ env : Environ.env =
with Not_found -> assert false
in
let constructors = Inductiveops.get_constructors env indf in
- let constructor : Inductiveops.constructor_summary = List.find (fun cs -> eq_constructor c cs.Inductiveops.cs_cstr) (Array.to_list constructors) in
+ let constructor : Inductiveops.constructor_summary = List.find (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr)) (Array.to_list constructors) in
let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in
List.fold_left2 add_pat_variables env patl (List.rev cs_args_types)
in
@@ -397,7 +397,7 @@ let rec pattern_to_term_and_type env typ = function
with Not_found -> assert false
in
let constructors = Inductiveops.get_constructors env indf in
- let constructor = List.find (fun cs -> eq_constructor cs.Inductiveops.cs_cstr constr) (Array.to_list constructors) in
+ let constructor = List.find (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr) (Array.to_list constructors) in
let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in
let _,cstl = Inductiveops.dest_ind_family indf in
let csta = Array.of_list cstl in
@@ -486,7 +486,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
a pseudo value "v1 ... vn".
The "value" of this branch is then simply [res]
*)
- let rt_as_constr = Pretyping.understand Evd.empty env rt in
+ let rt_as_constr,ctx = Pretyping.understand Evd.empty env rt in
let rt_typ = Typing.type_of env Evd.empty rt_as_constr in
let res_raw_type = Detyping.detype false [] (Termops.names_of_rel_context env) rt_typ in
let res = fresh_id args_res.to_avoid "_res" in
@@ -559,6 +559,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
*)
build_entry_lc env funnames avoid (mkGApp(b,args))
| GRec _ -> error "Not handled GRec"
+ | GProj _ -> error "Not handled GProj"
| GProd _ -> error "Cannot apply a type"
end (* end of the application treatement *)
@@ -594,7 +595,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
and combine the two result
*)
let v_res = build_entry_lc env funnames avoid v in
- let v_as_constr = Pretyping.understand Evd.empty env v in
+ let v_as_constr,ctx = Pretyping.understand Evd.empty env v in
let v_type = Typing.type_of env Evd.empty v_as_constr in
let new_env =
match n with
@@ -610,7 +611,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
let make_discr = make_discr_match brl in
build_entry_lc_from_case env funnames make_discr el brl avoid
| GIf(_,b,(na,e_option),lhs,rhs) ->
- let b_as_constr = Pretyping.understand Evd.empty env b in
+ let b_as_constr,ctx = Pretyping.understand Evd.empty env b in
let b_typ = Typing.type_of env Evd.empty b_as_constr in
let (ind,_) =
try Inductiveops.find_inductive env Evd.empty b_typ
@@ -619,7 +620,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
Printer.pr_glob_constr b ++ str " in " ++
Printer.pr_glob_constr rt ++ str ". try again with a cast")
in
- let case_pats = build_constructors_of_type ind [] in
+ let case_pats = build_constructors_of_type (fst ind) [] in
assert (Int.equal (Array.length case_pats) 2);
let brl =
List.map_i
@@ -642,7 +643,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
)
nal
in
- let b_as_constr = Pretyping.understand Evd.empty env b in
+ let b_as_constr,ctx = Pretyping.understand Evd.empty env b in
let b_typ = Typing.type_of env Evd.empty b_as_constr in
let (ind,_) =
try Inductiveops.find_inductive env Evd.empty b_typ
@@ -651,7 +652,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
Printer.pr_glob_constr b ++ str " in " ++
Printer.pr_glob_constr rt ++ str ". try again with a cast")
in
- let case_pats = build_constructors_of_type ind nal_as_glob_constr in
+ let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in
assert (Int.equal (Array.length case_pats) 1);
let br =
(Loc.ghost,[],[case_pats.(0)],e)
@@ -661,6 +662,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
end
| GRec _ -> error "Not handled GRec"
+ | GProj _ -> error "Not handled GProj"
| GCast(_,b,_) ->
build_entry_lc env funnames avoid b
and build_entry_lc_from_case env funname make_discr
@@ -689,7 +691,7 @@ and build_entry_lc_from_case env funname make_discr
in
let types =
List.map (fun (case_arg,_) ->
- let case_arg_as_constr = Pretyping.understand Evd.empty env case_arg in
+ let case_arg_as_constr,ctx = Pretyping.understand Evd.empty env case_arg in
Typing.type_of env Evd.empty case_arg_as_constr
) el
in
@@ -844,7 +846,7 @@ let is_res id =
let same_raw_term rt1 rt2 =
match rt1,rt2 with
- | GRef(_,r1), GRef (_,r2) -> Globnames.eq_gr r1 r2
+ | GRef(_,r1,_), GRef (_,r2,_) -> Globnames.eq_gr r1 r2
| GHole _, GHole _ -> true
| _ -> false
let decompose_raw_eq lhs rhs =
@@ -894,7 +896,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
let new_t =
mkGApp(mkGVar(mk_rel_id this_relname),args'@[res_rt])
in
- let t' = Pretyping.understand Evd.empty env new_t in
+ let t',ctx = Pretyping.understand Evd.empty env new_t in
let new_env = Environ.push_rel (n,None,t') env in
let new_b,id_to_exclude =
rebuild_cons new_env
@@ -907,14 +909,14 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
| _ -> (* the first args is the name of the function! *)
assert false
end
- | GApp(loc1,GRef(loc2,eq_as_ref),[ty;GVar(loc3,id);rt])
+ | GApp(loc1,GRef(loc2,eq_as_ref,_),[ty;GVar(loc3,id);rt])
when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous
->
begin
try
observe (str "computing new type for eq : " ++ pr_glob_constr rt);
let t' =
- try Pretyping.understand Evd.empty env t
+ try fst (Pretyping.understand Evd.empty env t)(*FIXME*)
with e when Errors.noncritical e -> raise Continue
in
let is_in_b = is_free_in id b in
@@ -936,17 +938,17 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
in
mkGProd(n,t,new_b),id_to_exclude
with Continue ->
- let jmeq = Globnames.IndRef (destInd (jmeq ())) in
- let ty' = Pretyping.understand Evd.empty env ty in
+ let jmeq = Globnames.IndRef (fst (destInd (jmeq ()))) in
+ let ty',ctx = Pretyping.understand Evd.empty env ty in
let ind,args' = Inductive.find_inductive env ty' in
- let mib,_ = Global.lookup_inductive ind in
+ let mib,_ = Global.lookup_inductive (fst ind) in
let nparam = mib.Declarations.mind_nparams in
let params,arg' =
((Util.List.chop nparam args'))
in
let rt_typ =
GApp(Loc.ghost,
- GRef (Loc.ghost,Globnames.IndRef ind),
+ GRef (Loc.ghost,Globnames.IndRef (fst ind),None),
(List.map
(fun p -> Detyping.detype false []
(Termops.names_of_rel_context env)
@@ -956,10 +958,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
(mkGHole ()))))
in
let eq' =
- GApp(loc1,GRef(loc2,jmeq),[ty;GVar(loc3,id);rt_typ;rt])
+ GApp(loc1,GRef(loc2,jmeq,None),[ty;GVar(loc3,id);rt_typ;rt])
in
observe (str "computing new type for jmeq : " ++ pr_glob_constr eq');
- let eq'_as_constr = Pretyping.understand Evd.empty env eq' in
+ let eq'_as_constr,ctx = Pretyping.understand Evd.empty env eq' in
observe (str " computing new type for jmeq : done") ;
let new_args =
match kind_of_term eq'_as_constr with
@@ -1007,7 +1009,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
if is_in_b then b else replace_var_by_term id rt b
in
let new_env =
- let t' = Pretyping.understand Evd.empty env eq' in
+ let t',ctx = Pretyping.understand Evd.empty env eq' in
Environ.push_rel (n,None,t') env
in
let new_b,id_to_exclude =
@@ -1024,7 +1026,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
mkGProd(n,t,new_b),id_to_exclude
else new_b, Id.Set.add id id_to_exclude
*)
- | GApp(loc1,GRef(loc2,eq_as_ref),[ty;rt1;rt2])
+ | GApp(loc1,GRef(loc2,eq_as_ref,_),[ty;rt1;rt2])
when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous
->
begin
@@ -1045,7 +1047,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
else raise Continue
with Continue ->
observe (str "computing new type for prod : " ++ pr_glob_constr rt);
- let t' = Pretyping.understand Evd.empty env t in
+ let t',ctx = Pretyping.understand Evd.empty env t in
let new_env = Environ.push_rel (n,None,t') env in
let new_b,id_to_exclude =
rebuild_cons new_env
@@ -1061,7 +1063,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
end
| _ ->
observe (str "computing new type for prod : " ++ pr_glob_constr rt);
- let t' = Pretyping.understand Evd.empty env t in
+ let t',ctx = Pretyping.understand Evd.empty env t in
let new_env = Environ.push_rel (n,None,t') env in
let new_b,id_to_exclude =
rebuild_cons new_env
@@ -1080,7 +1082,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
let not_free_in_t id = not (is_free_in id t) in
let new_crossed_types = t :: crossed_types in
observe (str "computing new type for lambda : " ++ pr_glob_constr rt);
- let t' = Pretyping.understand Evd.empty env t in
+ let t',ctx = Pretyping.understand Evd.empty env t in
match n with
| Name id ->
let new_env = Environ.push_rel (n,None,t') env in
@@ -1102,7 +1104,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
| GLetIn(_,n,t,b) ->
begin
let not_free_in_t id = not (is_free_in id t) in
- let t' = Pretyping.understand Evd.empty env t in
+ let t',ctx = Pretyping.understand Evd.empty env t in
let type_t' = Typing.type_of env Evd.empty t' in
let new_env = Environ.push_rel (n,Some t',type_t') env in
let new_b,id_to_exclude =
@@ -1127,7 +1129,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
args (crossed_types)
depth t
in
- let t' = Pretyping.understand Evd.empty env new_t in
+ let t',ctx = Pretyping.understand Evd.empty env new_t in
let new_env = Environ.push_rel (na,None,t') env in
let new_b,id_to_exclude =
rebuild_cons new_env
@@ -1179,7 +1181,7 @@ let rec compute_cst_params relnames params = function
discriminitation ones *)
| GSort _ -> params
| GHole _ -> params
- | GIf _ | GRec _ | GCast _ ->
+ | GIf _ | GRec _ | GCast _ | GProj _->
raise (UserError("compute_cst_params", str "Not handled case"))
and compute_cst_params_from_app acc (params,rtl) =
match params,rtl with
@@ -1267,12 +1269,12 @@ let do_build_inductive
(fun (n,t,is_defined) acc ->
if is_defined
then
- Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),Constrextern.extern_glob_constr Id.Set.empty t,
+ Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
acc)
else
Constrexpr.CProdN
(Loc.ghost,
- [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Id.Set.empty t],
+ [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
acc
)
)
@@ -1285,7 +1287,8 @@ let do_build_inductive
*)
let rel_arities = Array.mapi rel_arity funsargs in
Util.Array.fold_left2 (fun env rel_name rel_ar ->
- Environ.push_named (rel_name,None, Constrintern.interp_constr Evd.empty env rel_ar) env) env relnames rel_arities
+ Environ.push_named (rel_name,None,
+ fst (with_full_print (Constrintern.interp_constr Evd.empty env) rel_ar)) env) env relnames rel_arities
in
(* and of the real constructors*)
let constr i res =
@@ -1333,12 +1336,12 @@ let do_build_inductive
(fun (n,t,is_defined) acc ->
if is_defined
then
- Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),Constrextern.extern_glob_constr Id.Set.empty t,
+ Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
acc)
else
Constrexpr.CProdN
(Loc.ghost,
- [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Id.Set.empty t],
+ [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
acc
)
)
@@ -1366,8 +1369,7 @@ let do_build_inductive
Array.map (List.map
(fun (id,t) ->
false,((Loc.ghost,id),
- Flags.with_option
- Flags.raw_print
+ with_full_print
(Constrextern.extern_glob_type Id.Set.empty) ((* zeta_normalize *) t)
)
))
@@ -1403,7 +1405,7 @@ let do_build_inductive
(* in *)
let _time2 = System.get_time () in
try
- with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds)) true
+ with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds false)) true
with
| UserError(s,msg) as e ->
let _time3 = System.get_time () in
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 6a7f326e6c..5efaf7954e 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -10,7 +10,7 @@ open Misctypes
Some basic functions to rebuild glob_constr
In each of them the location is Loc.ghost
*)
-let mkGRef ref = GRef(Loc.ghost,ref)
+let mkGRef ref = GRef(Loc.ghost,ref,None)
let mkGVar id = GVar(Loc.ghost,id)
let mkGApp(rt,rtl) = GApp(Loc.ghost,rt,rtl)
let mkGLambda(n,t,b) = GLambda(Loc.ghost,n,Explicit,t,b)
@@ -180,6 +180,7 @@ let change_vars =
| GRec _ -> error "Local (co)fixes are not supported"
| GSort _ -> rt
| GHole _ -> rt
+ | GProj _ -> error "Native projections are not supported" (** FIXME *)
| GCast(loc,b,c) ->
GCast(loc,change_vars mapping b,
Miscops.map_cast_type (change_vars mapping) c)
@@ -357,6 +358,7 @@ let rec alpha_rt excluded rt =
alpha_rt excluded rhs
)
| GRec _ -> error "Not handled GRec"
+ | GProj _ -> error "Native projections are not supported" (** FIXME *)
| GSort _ -> rt
| GHole _ -> rt
| GCast (loc,b,c) ->
@@ -407,6 +409,7 @@ let is_free_in id =
| GIf(_,cond,_,br1,br2) ->
is_free_in cond || is_free_in br1 || is_free_in br2
| GRec _ -> raise (UserError("",str "Not handled GRec"))
+ | GProj _ -> error "Native projections are not supported" (** FIXME *)
| GSort _ -> false
| GHole _ -> false
| GCast (_,b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t
@@ -503,6 +506,7 @@ let replace_var_by_term x_id term =
replace_var_by_pattern rhs
)
| GRec _ -> raise (UserError("",str "Not handled GRec"))
+ | GProj _ -> error "Native projections are not supported" (** FIXME *)
| GSort _ -> rt
| GHole _ -> rt
| GCast(loc,b,c) ->
@@ -598,6 +602,7 @@ let ids_of_glob_constr c =
| GCases (loc,sty,rtntypopt,tml,brchl) ->
List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_glob_constr [] c) brchl)
| GRec _ -> failwith "Fix inside a constructor branch"
+ | GProj _ -> error "Native projections are not supported" (** FIXME *)
| (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> []
in
(* build the set *)
@@ -656,6 +661,7 @@ let zeta_normalize =
zeta_normalize_term rhs
)
| GRec _ -> raise (UserError("",str "Not handled GRec"))
+ | GProj _ -> error "Native projections are not supported" (** FIXME *)
| GSort _ -> rt
| GHole _ -> rt
| GCast(loc,b,c) ->
@@ -698,6 +704,7 @@ let expand_as =
GIf(loc,expand_as map e,(na,Option.map (expand_as map) po),
expand_as map br1, expand_as map br2)
| GRec _ -> error "Not handled GRec"
+ | GProj _ -> error "Native projections are not supported" (** FIXME *)
| GCast(loc,b,c) ->
GCast(loc,expand_as map b,
Miscops.map_cast_type (expand_as map) c)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 661e5e4869..d98f824e84 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -38,7 +38,7 @@ let functional_induction with_clean c princl pat =
| None -> (* No principle is given let's find the good one *)
begin
match kind_of_term f with
- | Const c' ->
+ | Const (c',u) ->
let princ_option =
let finfo = (* we first try to find out a graph on f *)
try find_Function_infos c'
@@ -148,7 +148,7 @@ let build_newrecursive
List.fold_left
(fun (env,impls) ((_,recname),bl,arityc,_) ->
let arityc = Constrexpr_ops.prod_constr_expr arityc bl in
- let arity = Constrintern.interp_type sigma env0 arityc in
+ let arity,ctx = Constrintern.interp_type sigma env0 arityc in
let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity [] in
(Environ.push_named (recname,None,arity) env, Id.Map.add recname impl impls))
(env0,Constrintern.empty_internalization_env) lnameargsardef in
@@ -182,6 +182,7 @@ let is_rec names =
| GVar(_,id) -> check_id id names
| GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> false
| GCast(_,b,_) -> lookup names b
+ | GProj _ -> error "GProj not handled"
| GRec _ -> error "GRec not handled"
| GIf(_,b,_,lhs,rhs) ->
(lookup names b) || (lookup names lhs) || (lookup names rhs)
@@ -222,7 +223,7 @@ let derive_inversion fix_names =
try
(* we first transform the fix_names identifier into their corresponding constant *)
let fix_names_as_constant =
- List.map (fun id -> destConst (Constrintern.global_reference id)) fix_names
+ List.map (fun id -> fst (destConst (Constrintern.global_reference id))) fix_names
in
(*
Then we check that the graphs have been defined
@@ -239,7 +240,7 @@ let derive_inversion fix_names =
Ensures by : register_built
i*)
(List.map
- (fun id -> destInd (Constrintern.global_reference (mk_rel_id id)))
+ (fun id -> fst (destInd (Constrintern.global_reference (mk_rel_id id))))
fix_names
)
with e when Errors.noncritical e ->
@@ -326,9 +327,8 @@ let generate_principle on_error
let _ =
List.map_i
(fun i x ->
- let princ = destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)) in
- let princ_type = Typeops.type_of_constant (Global.env()) princ
- in
+ let princ = Indrec.lookup_eliminator (ind_kn,i) (InProp) in
+ let princ_type = Global.type_of_global_unsafe princ in
Functional_principles_types.generate_functional_principle
interactive_proof
princ_type
@@ -351,10 +351,10 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
match fixpoint_exprl with
| [((_,fname),_,bl,ret_type,body),_] when not is_rec ->
let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in
- Command.do_definition fname (Decl_kinds.Global,Decl_kinds.Definition)
+ Command.do_definition fname (Decl_kinds.Global,(*FIXME*)false,Decl_kinds.Definition)
bl None body (Some ret_type) (fun _ _ -> ())
| _ ->
- Command.do_fixpoint Global fixpoint_exprl
+ Command.do_fixpoint Global false(*FIXME*) fixpoint_exprl
let generate_correction_proof_wf f_ref tcc_lemma_ref
is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
@@ -385,7 +385,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
let f_app_args =
Constrexpr.CAppExpl
(Loc.ghost,
- (None,(Ident (Loc.ghost,fname))) ,
+ (None,(Ident (Loc.ghost,fname)),None) ,
(List.map
(function
| _,Anonymous -> assert false
@@ -399,7 +399,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
[(f_app_args,None);(body,None)])
in
let eq = Constrexpr_ops.prod_constr_expr unbounded_eq args in
- let hook f_ref tcc_lemma_ref functional_ref eq_ref rec_arg_num rec_arg_type
+ let hook (f_ref,_) tcc_lemma_ref (functional_ref,_) (eq_ref,_) rec_arg_num rec_arg_type
nb_args relation =
try
pre_hook
@@ -536,7 +536,7 @@ let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ
let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in
- let ((_,_,typel),_) = Command.interp_fixpoint fixl ntns in
+ let ((_,_,typel),_,_) = Command.interp_fixpoint fixl ntns in
let constr_expr_typel =
with_full_print (List.map (Constrextern.extern_constr false (Global.env ()))) typel in
let fixpoint_exprl_with_new_bl =
@@ -631,10 +631,10 @@ let do_generate_principle on_error register_built interactive_proof
let rec add_args id new_args b =
match b with
- | CRef r ->
+ | CRef (r,_) ->
begin match r with
| Libnames.Ident(loc,fname) when Id.equal fname id ->
- CAppExpl(Loc.ghost,(None,r),new_args)
+ CAppExpl(Loc.ghost,(None,r,None),new_args)
| _ -> b
end
| CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo")
@@ -648,12 +648,12 @@ let rec add_args id new_args b =
add_args id new_args b1)
| CLetIn(loc,na,b1,b2) ->
CLetIn(loc,na,add_args id new_args b1,add_args id new_args b2)
- | CAppExpl(loc,(pf,r),exprl) ->
+ | CAppExpl(loc,(pf,r,us),exprl) ->
begin
match r with
| Libnames.Ident(loc,fname) when Id.equal fname id ->
- CAppExpl(loc,(pf,r),new_args@(List.map (add_args id new_args) exprl))
- | _ -> CAppExpl(loc,(pf,r),List.map (add_args id new_args) exprl)
+ CAppExpl(loc,(pf,r,us),new_args@(List.map (add_args id new_args) exprl))
+ | _ -> CAppExpl(loc,(pf,r,us),List.map (add_args id new_args) exprl)
end
| CApp(loc,(pf,b),bl) ->
CApp(loc,(pf,add_args id new_args b),
@@ -767,11 +767,10 @@ let make_graph (f_ref:global_reference) =
| Some body ->
let env = Global.env () in
let extern_body,extern_type =
- with_full_print
- (fun () ->
+ with_full_print (fun () ->
(Constrextern.extern_constr false env body,
Constrextern.extern_type false env
- (Typeops.type_of_constant_type env c_body.const_type)
+ ((*FIXNE*) c_body.const_type)
)
)
()
@@ -792,7 +791,7 @@ let make_graph (f_ref:global_reference) =
| Constrexpr.LocalRawAssum (nal,_,_) ->
List.map
(fun (loc,n) ->
- CRef(Libnames.Ident(loc, Nameops.out_name n)))
+ CRef(Libnames.Ident(loc, Nameops.out_name n),None))
nal
)
nal_tas
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 5c37dcec34..8cccb0bedf 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -114,7 +114,7 @@ let const_of_id id =
let def_of_const t =
match (Term.kind_of_term t) with
Term.Const sp ->
- (try (match Declareops.body_of_constant (Global.lookup_constant sp) with
+ (try (match Environ.constant_opt_value_in (Global.env()) sp with
| Some c -> c
| _ -> assert false)
with Not_found -> assert false)
@@ -146,7 +146,7 @@ let get_locality = function
| Local -> true
| Global -> false
-let save with_clean id const (locality,kind) hook =
+let save with_clean id const (locality,_,kind) hook =
let l,r = match locality with
| Discharge when Lib.sections_are_opened () ->
let k = Kindops.logical_kind_of_goal_kind kind in
@@ -177,7 +177,8 @@ let get_proof_clean do_reduce =
let with_full_print f a =
let old_implicit_args = Impargs.is_implicit_args ()
and old_strict_implicit_args = Impargs.is_strict_implicit_args ()
- and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
+ and old_contextual_implicit_args = Impargs.is_contextual_implicit_args ()
+ in
let old_rawprint = !Flags.raw_print in
Flags.raw_print := true;
Impargs.make_implicit_args false;
@@ -259,8 +260,8 @@ let cache_Function (_,finfos) =
let load_Function _ = cache_Function
let subst_Function (subst,finfos) =
- let do_subst_con c = fst (Mod_subst.subst_con subst c)
- and do_subst_ind (kn,i) = (Mod_subst.subst_ind subst kn,i)
+ let do_subst_con c = Mod_subst.subst_constant subst c
+ and do_subst_ind i = Mod_subst.subst_ind subst i
in
let function_constant' = do_subst_con finfos.function_constant in
let graph_ind' = do_subst_ind finfos.graph_ind in
@@ -336,7 +337,7 @@ let pr_info f_info =
str "function_constant_type := " ++
(try
Printer.pr_lconstr
- (Global.type_of_global (ConstRef f_info.function_constant))
+ (Global.type_of_global_unsafe (ConstRef f_info.function_constant))
with e when Errors.noncritical e -> mt ()) ++ fnl () ++
str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++
str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 0e8b22deba..6e8b79a6be 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -58,7 +58,7 @@ val get_proof_clean : bool ->
-(* [with_full_print f a] applies [f] to [a] in full printing environment
+(* [with_full_print f a] applies [f] to [a] in full printing environment.
This function preserves the print settings
*)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 7c8f5714e6..897c8765bf 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -112,7 +112,9 @@ let id_to_constr id =
let generate_type g_to_f f graph i =
(*i we deduce the number of arguments of the function and its returned type from the graph i*)
- let graph_arity = Inductive.type_of_inductive (Global.env()) (Global.lookup_inductive (destInd graph)) in
+ let gr,u = destInd graph in
+ let graph_arity = Inductive.type_of_inductive (Global.env())
+ (Global.lookup_inductive gr, u) in
let ctxt,_ = decompose_prod_assum graph_arity in
let fun_ctxt,res_type =
match ctxt with
@@ -138,8 +140,11 @@ let generate_type g_to_f f graph i =
the hypothesis [res = fv] can then be computed
We will need to lift it by one in order to use it as a conclusion
i*)
+ let make_eq () =
+(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ())
+ in
let res_eq_f_of_args =
- mkApp(Coqlib.build_coq_eq (),[|lift 2 res_type;mkRel 1;mkRel 2|])
+ mkApp(make_eq (),[|lift 2 res_type;mkRel 1;mkRel 2|])
in
(*i
The hypothesis [graph\ x_1\ldots x_n\ res] can then be computed
@@ -166,7 +171,7 @@ let generate_type g_to_f f graph i =
WARNING: while convertible, [type_of body] and [type] can be non equal
*)
let find_induction_principle f =
- let f_as_constant = match kind_of_term f with
+ let f_as_constant,u = match kind_of_term f with
| Const c' -> c'
| _ -> error "Must be used with a function"
in
@@ -205,6 +210,11 @@ let rec generate_fresh_id x avoid i =
let id = Namegen.next_ident_away_in_goal x avoid in
id::(generate_fresh_id x (id::avoid) (pred i))
+let make_eq () =
+(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ())
+let make_eq_refl () =
+(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq_refl ())
+
(* [prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos i ]
is the tactic used to prove correctness lemma.
@@ -237,7 +247,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
\[fun (x_1:t_1)\ldots(x_n:t_n)=> fun fv => fun res => res = fv \rightarrow graph\ x_1\ldots x_n\ res\]
*)
(* we the get the definition of the graphs block *)
- let graph_ind = destInd graphs_constr.(i) in
+ let graph_ind,u = destInd graphs_constr.(i) in
let kn = fst graph_ind in
let mib,_ = Global.lookup_inductive graph_ind in
(* and the principle to use in this lemma in $\zeta$ normal form *)
@@ -267,8 +277,8 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
branches
in
(* before building the full intro pattern for the principle *)
- let eq_ind = Coqlib.build_coq_eq () in
- let eq_construct = mkConstruct((destInd eq_ind),1) in
+ let eq_ind = make_eq () in
+ let eq_construct = mkConstructUi (destInd eq_ind, 1) in
(* The next to referencies will be used to find out which constructor to apply in each branch *)
let ind_number = ref 0
and min_constr_number = ref 0 in
@@ -731,7 +741,7 @@ let rec intros_with_rewrite g =
observe_tac "intros_with_rewrite" intros_with_rewrite_aux g
and intros_with_rewrite_aux : tactic =
fun g ->
- let eq_ind = Coqlib.build_coq_eq () in
+ let eq_ind = make_eq () in
match kind_of_term (pf_concl g) with
| Prod(_,t,t') ->
begin
@@ -830,7 +840,7 @@ let rec reflexivity_with_destruct_cases g =
| _ -> Proofview.V82.of_tactic reflexivity
with e when Errors.noncritical e -> Proofview.V82.of_tactic reflexivity
in
- let eq_ind = Coqlib.build_coq_eq () in
+ let eq_ind = make_eq () in
let discr_inject =
Tacticals.onAllHypsAndConcl (
fun sc g ->
@@ -936,7 +946,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
let rewrite_tac j ids : tactic =
let graph_def = graphs.(j) in
let infos =
- try find_Function_infos (destConst funcs.(j))
+ try find_Function_infos (fst (destConst funcs.(j)))
with Not_found -> error "No graph found"
in
if infos.is_general
@@ -962,7 +972,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
thin ids
]
else
- unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (destConst f))]
+ unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst (destConst f)))]
in
(* The proof of each branche itself *)
let ind_number = ref 0 in
@@ -1026,7 +1036,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
let lemmas_types_infos =
Util.Array.map2_i
(fun i f_constr graph ->
- let const_of_f = destConst f_constr in
+ let const_of_f,u = destConst f_constr in
let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info =
generate_type false const_of_f graph i
in
@@ -1065,22 +1075,22 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
i*)
let lem_id = mk_correct_id f_id in
Lemmas.start_proof lem_id
- (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
- (fst lemmas_types_infos.(i))
+ (Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem))
+ (fst lemmas_types_infos.(i), (*FIXME*)Univ.ContextSet.empty)
(fun _ _ -> ());
ignore (Pfedit.by
(Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
(proving_tac i))));
do_save ();
let finfo = find_Function_infos f_as_constant in
- let lem_cst = destConst (Constrintern.global_reference lem_id) in
+ let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in
update_Function {finfo with correctness_lemma = Some lem_cst}
)
funs;
let lemmas_types_infos =
Util.Array.map2_i
(fun i f_constr graph ->
- let const_of_f = destConst f_constr in
+ let const_of_f = fst (destConst f_constr) in
let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info =
generate_type true const_of_f graph i
in
@@ -1092,19 +1102,21 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
funs_constr
graphs_constr
in
- let kn,_ as graph_ind = destInd graphs_constr.(0) in
+ let kn,_ as graph_ind = fst (destInd graphs_constr.(0)) in
let mib,mip = Global.lookup_inductive graph_ind in
- let schemes =
- Array.of_list
+ let sigma, scheme =
(Indrec.build_mutual_induction_scheme (Global.env ()) Evd.empty
(Array.to_list
(Array.mapi
- (fun i _ -> (kn,i),true,InType)
+ (fun i _ -> ((kn,i),Univ.Instance.empty)(*FIXME*),true,InType)
mib.Declarations.mind_packets
)
)
)
in
+ let schemes =
+ Array.of_list scheme
+ in
let proving_tac =
prove_fun_complete funs_constr mib.Declarations.mind_packets schemes lemmas_types_infos
in
@@ -1116,15 +1128,12 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
i*)
let lem_id = mk_complete_id f_id in
Lemmas.start_proof lem_id
- (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
- (fst lemmas_types_infos.(i))
+ (Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem))
+ (fst lemmas_types_infos.(i), (*FIXME*)Univ.ContextSet.empty)
(fun _ _ -> ());
- ignore (Pfedit.by
- (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
- (proving_tac i))));
do_save ();
let finfo = find_Function_infos f_as_constant in
- let lem_cst = destConst (Constrintern.global_reference lem_id) in
+ let lem_cst,u = destConst (Constrintern.global_reference lem_id) in
update_Function {finfo with completeness_lemma = Some lem_cst}
)
funs)
@@ -1142,7 +1151,7 @@ let revert_graph kn post_tac hid g =
let typ = pf_type_of g (mkVar hid) in
match kind_of_term typ with
| App(i,args) when isInd i ->
- let ((kn',num) as ind') = destInd i in
+ let ((kn',num) as ind'),u = destInd i in
if MutInd.equal kn kn'
then (* We have generated a graph hypothesis so that we must change it if we can *)
let info =
@@ -1192,7 +1201,7 @@ let functional_inversion kn hid fconst f_correct : tactic =
let old_ids = List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty in
let type_of_h = pf_type_of g (mkVar hid) in
match kind_of_term type_of_h with
- | App(eq,args) when eq_constr eq (Coqlib.build_coq_eq ()) ->
+ | App(eq,args) when eq_constr eq (make_eq ()) ->
let pre_tac,f_args,res =
match kind_of_term args.(1),kind_of_term args.(2) with
| App(f,f_args),_ when eq_constr f fconst ->
@@ -1244,12 +1253,12 @@ let invfun qhyp f g =
(fun hid -> Proofview.V82.tactic begin fun g ->
let hyp_typ = pf_type_of g (mkVar hid) in
match kind_of_term hyp_typ with
- | App(eq,args) when eq_constr eq (Coqlib.build_coq_eq ()) ->
+ | App(eq,args) when eq_constr eq (make_eq ()) ->
begin
let f1,_ = decompose_app args.(1) in
try
if not (isConst f1) then failwith "";
- let finfos = find_Function_infos (destConst f1) in
+ let finfos = find_Function_infos (fst (destConst f1)) in
let f_correct = mkConst(Option.get finfos.correctness_lemma)
and kn = fst finfos.graph_ind
in
@@ -1258,7 +1267,7 @@ let invfun qhyp f g =
try
let f2,_ = decompose_app args.(2) in
if not (isConst f2) then failwith "";
- let finfos = find_Function_infos (destConst f2) in
+ let finfos = find_Function_infos (fst (destConst f2)) in
let f_correct = mkConst(Option.get finfos.correctness_lemma)
and kn = fst finfos.graph_ind
in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index ac54e44cc7..d0497f6f6c 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -70,7 +70,7 @@ let isVarf f x =
in global environment. *)
let ident_global_exist id =
try
- let ans = CRef (Libnames.Ident (Loc.ghost,id)) in
+ let ans = CRef (Libnames.Ident (Loc.ghost,id), None) in
let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in
true
with e when Errors.noncritical e -> false
@@ -134,16 +134,12 @@ let prNamedRLDecl s lc =
let showind (id:Id.t) =
let cstrid = Constrintern.global_reference id in
let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty cstrid in
- let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) ind1 in
+ let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) (fst ind1) in
List.iter (fun (nm, optcstr, tp) ->
print_string (string_of_name nm^":");
prconstr tp; print_string "\n")
ib1.mind_arity_ctxt;
- (match ib1.mind_arity with
- | Monomorphic x ->
- Printf.printf "arity :"; prconstr x.mind_user_arity
- | Polymorphic x ->
- Printf.printf "arity : universe?");
+ Printf.printf "arity :"; prconstr ib1.mind_arity.mind_user_arity;
Array.iteri
(fun i x -> Printf.printf"type constr %d :" i ; prconstr x)
ib1.mind_user_lc
@@ -888,7 +884,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
(* Declare inductive *)
let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in
- let mie,impls = Command.interp_mutual_inductive indl [] true (* means: not coinductive *) in
+ let mie,impls = Command.interp_mutual_inductive indl [] false (*FIXMEnon-poly *) true (* means: not coinductive *) in
(* Declare the mutual inductive block with its associated schemes *)
ignore (Command.declare_mutual_inductive_with_eliminations Declare.UserVerbose mie impls)
@@ -961,7 +957,7 @@ let funify_branches relinfo nfuns branch =
| _ -> assert false in
let is_dom c =
match kind_of_term c with
- | Ind((u,_)) | Construct((u,_),_) -> MutInd.equal u mut_induct
+ | Ind(((u,_),_)) | Construct(((u,_),_),_) -> MutInd.equal u mut_induct
| _ -> false in
let _dom_i c =
assert (is_dom c);
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 6148860730..96bf4c9216 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -52,29 +52,21 @@ let find_reference sl s =
let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in
locate (make_qualid dp (Id.of_string s))
-let (declare_fun : Id.t -> logical_kind -> constr -> global_reference) =
- fun f_id kind value ->
- let ce = {const_entry_body = Future.from_val
- (value, Declareops.no_seff);
- const_entry_secctx = None;
- const_entry_type = None;
- const_entry_opaque = false;
- const_entry_inline_code = false;
- const_entry_feedback = None;
- } in
- ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
+let declare_fun f_id kind ?(ctx=Univ.UContext.empty) value =
+ let ce = definition_entry ~univs:ctx value (*FIXME *) in
+ ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
let defined () = Lemmas.save_proof (Vernacexpr.Proved (false,None))
let def_of_const t =
match (kind_of_term t) with
Const sp ->
- (try (match body_of_constant (Global.lookup_constant sp) with
+ (try (match constant_opt_value_in (Global.env ()) sp with
| Some c -> c
| _ -> raise Not_found)
with Not_found ->
anomaly (str "Cannot find definition of constant " ++
- (Id.print (Label.to_id (con_label sp))))
+ (Id.print (Label.to_id (con_label (fst sp)))))
)
|_ -> assert false
@@ -83,6 +75,7 @@ let type_of_const t =
Const sp -> Typeops.type_of_constant (Global.env()) sp
|_ -> assert false
+let constr_of_global = Universes.constr_of_global
let constant sl s = constr_of_global (find_reference sl s)
@@ -188,7 +181,7 @@ let (value_f:constr list -> global_reference -> constr) =
let glob_body =
GCases
(d0,RegularStyle,None,
- [GApp(d0, GRef(d0,fterm), List.rev_map (fun x_id -> GVar(d0, x_id)) rev_x_id_l),
+ [GApp(d0, GRef(d0,fterm,None), List.rev_map (fun x_id -> GVar(d0, x_id)) rev_x_id_l),
(Anonymous,None)],
[d0, [v_id], [PatCstr(d0,(destIndRef
(delayed_force coq_sig_ref),1),
@@ -197,7 +190,7 @@ let (value_f:constr list -> global_reference -> constr) =
Anonymous)],
GVar(d0,v_id)])
in
- let body = understand Evd.empty env glob_body in
+ let body = fst (understand Evd.empty env glob_body)(*FIXME*) in
it_mkLambda_or_LetIn body context
let (declare_f : Id.t -> logical_kind -> constr list -> global_reference -> global_reference) =
@@ -302,6 +295,7 @@ let check_not_nested forbidden e =
| Lambda(_,t,b) -> check_not_nested t;check_not_nested b
| LetIn(_,v,t,b) -> check_not_nested t;check_not_nested b;check_not_nested v
| App(f,l) -> check_not_nested f;Array.iter check_not_nested l
+ | Proj (p,c) -> check_not_nested c
| Const _ -> ()
| Ind _ -> ()
| Construct _ -> ()
@@ -412,6 +406,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
match kind_of_term expr_info.info with
| CoFix _ | Fix _ -> error "Function cannot treat local fixpoint or cofixpoint"
+ | Proj _ -> error "Function cannot treat projections"
| LetIn(na,b,t,e) ->
begin
let new_continuation_tac =
@@ -640,7 +635,16 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info =
in
continuation_tac {info with info = new_e; forbidden_ids = new_forbidden}
+let pf_type c tac gl =
+ let evars, ty = Typing.e_type_of (pf_env gl) (project gl) c in
+ tclTHEN (Refiner.tclEVARS evars) (tac ty) gl
+let pf_typel l tac =
+ let rec aux tys l =
+ match l with
+ | [] -> tac (List.rev tys)
+ | hd :: tl -> pf_type hd (fun ty -> aux (ty::tys) tl)
+ in aux [] l
(* This is like the previous one except that it also rewrite on all
hypotheses except the ones given in the first argument. All the
@@ -660,12 +664,13 @@ let mkDestructEq :
let type_of_expr = pf_type_of g expr in
let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|])::
to_revert_constr in
+ pf_typel new_hyps (fun _ ->
tclTHENLIST
[Simple.generalize new_hyps;
(fun g2 ->
change_in_concl None
(pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) Evd.empty (pf_concl g2)) g2);
- Proofview.V82.of_tactic (simplest_case expr)], to_revert
+ Proofview.V82.of_tactic (simplest_case expr)]), to_revert
let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
@@ -1167,7 +1172,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
let get_current_subgoals_types () =
let p = Proof_global.give_me_the_proof () in
let { Evd.it=sgs ; sigma=sigma } = Proof.V82.subgoals p in
- List.map (Goal.V82.abstract_type sigma) sgs
+ sigma, List.map (Goal.V82.abstract_type sigma) sgs
let build_and_l l =
let and_constr = Coqlib.build_coq_and () in
@@ -1225,12 +1230,12 @@ let clear_goals =
let build_new_goal_type () =
- let sub_gls_types = get_current_subgoals_types () in
- (* Pp.msgnl (str "sub_gls_types1 := " ++ Pp.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *)
+ let sigma, sub_gls_types = get_current_subgoals_types () in
+ (* Pp.msgnl (str "sub_gls_types1 := " ++ Util.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *)
let sub_gls_types = clear_goals sub_gls_types in
(* Pp.msgnl (str "sub_gls_types2 := " ++ Pp.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *)
let res = build_and_l sub_gls_types in
- res
+ sigma, res
let is_opaque_constant c =
let cb = Global.lookup_constant c in
@@ -1239,7 +1244,7 @@ let is_opaque_constant c =
| Declarations.Undef _ -> true
| Declarations.Def _ -> false
-let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) =
+let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) =
(* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *)
let current_proof_name = get_current_proof_name () in
let name = match goal_name with
@@ -1265,7 +1270,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
let lid = ref [] in
let h_num = ref (-1) in
Proof_global.discard_all ();
- build_proof
+ build_proof (Univ.ContextSet.empty)
( fun gls ->
let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
tclTHENSEQ
@@ -1312,8 +1317,8 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
in
Lemmas.start_proof
na
- (Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma)
- gls_type
+ (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma)
+ (gls_type, ctx)
hook;
if Indfun_common.is_strict_tcc ()
then
@@ -1330,7 +1335,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
(fun c ->
tclTHENSEQ
[Proofview.V82.of_tactic intros;
- Simple.apply (interp_constr Evd.empty (Global.env()) c);
+ Simple.apply (fst (interp_constr Evd.empty (Global.env()) c)) (*FIXME*);
tclCOMPLETE (Proofview.V82.of_tactic Auto.default_auto)
]
)
@@ -1354,22 +1359,24 @@ let com_terminate
relation
rec_arg_num
thm_name using_lemmas
- nb_args
+ nb_args ctx
hook =
- let start_proof (tac_start:tactic) (tac_end:tactic) =
+ let ctx = Univ.ContextSet.of_context ctx in
+ let start_proof ctx (tac_start:tactic) (tac_end:tactic) =
let (evmap, env) = Lemmas.get_current_context() in
Lemmas.start_proof thm_name
- (Global, Proof Lemma) ~sign:(Environ.named_context_val env)
- (compute_terminate_type nb_args fonctional_ref) hook;
+ (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env)
+ (compute_terminate_type nb_args fonctional_ref, ctx) hook;
ignore (by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start)));
ignore (by (Proofview.V82.tactic (observe_tac (str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref
input_type relation rec_arg_num ))))
in
- start_proof tclIDTAC tclIDTAC;
+ start_proof ctx tclIDTAC tclIDTAC;
try
- let new_goal_type = build_new_goal_type () in
- open_new_goal start_proof using_lemmas tcc_lemma_ref
+ let sigma, new_goal_type = build_new_goal_type () in
+ open_new_goal start_proof (Evd.get_universe_context_set sigma)
+ using_lemmas tcc_lemma_ref
(Some tcc_lemma_name)
(new_goal_type);
with Failure "empty list of subgoals!" ->
@@ -1384,7 +1391,7 @@ let start_equation (f:global_reference) (term_f:global_reference)
(cont_tactic:Id.t list -> tactic) g =
let ids = pf_ids_of_hyps g in
let terminate_constr = constr_of_global term_f in
- let nargs = nb_prod (type_of_const terminate_constr) in
+ let nargs = nb_prod (fst (type_of_const terminate_constr)) (*FIXME*) in
let x = n_x_id ids nargs in
tclTHENLIST [
h_intros x;
@@ -1406,8 +1413,8 @@ let (com_eqn : int -> Id.t ->
let (evmap, env) = Lemmas.get_current_context() in
let f_constr = constr_of_global f_ref in
let equation_lemma_type = subst1 f_constr equation_lemma_type in
- (Lemmas.start_proof eq_name (Global, Proof Lemma)
- ~sign:(Environ.named_context_val env) equation_lemma_type (fun _ _ -> ());
+ (Lemmas.start_proof eq_name (Global, false, Proof Lemma)
+ ~sign:(Environ.named_context_val env) (equation_lemma_type, (*FIXME*)Univ.ContextSet.empty) (fun _ _ -> ());
ignore (by
(Proofview.V82.tactic (start_equation f_ref terminate_ref
(fun x ->
@@ -1445,13 +1452,15 @@ let (com_eqn : int -> Id.t ->
let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq
generate_induction_principle using_lemmas : unit =
- let function_type = interp_constr Evd.empty (Global.env()) type_of_f in
- let env = push_named (function_name,None,function_type) (Global.env()) in
+ let env = Global.env() in
+ let evd = ref (Evd.from_env env) in
+ let function_type = interp_type_evars evd env type_of_f in
+ let env = push_named (function_name,None,function_type) env in
(* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *)
- let equation_lemma_type =
- nf_betaiotazeta
- (interp_constr Evd.empty env ~impls:rec_impls eq)
- in
+ let ty = interp_type_evars evd env ~impls:rec_impls eq in
+ let evm, nf = Evarutil.nf_evars_and_universes !evd in
+ let equation_lemma_type = nf_betaiotazeta (nf ty) in
+ let function_type = nf function_type in
(* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *)
let res_vars,eq' = decompose_prod equation_lemma_type in
let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> (x,None,y)) res_vars) env in
@@ -1471,13 +1480,14 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let equation_id = add_suffix function_name "_equation" in
let functional_id = add_suffix function_name "_F" in
let term_id = add_suffix function_name "_terminate" in
- let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) res in
+ let ctx = Evd.universe_context evm in
+ let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx res in
let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in
let relation =
- interp_constr
+ fst (*FIXME*)(interp_constr
Evd.empty
env_with_pre_rec_args
- r
+ r)
in
let tcc_lemma_name = add_suffix function_name "_tcc" in
let tcc_lemma_constr = ref None in
@@ -1524,6 +1534,5 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
term_id
using_lemmas
(List.length res_vars)
- hook)
+ ctx hook)
()
-
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index 2ef6852036..f60eedbe6e 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -12,9 +12,9 @@ bool ->
Constrintern.internalization_env ->
Constrexpr.constr_expr ->
Constrexpr.constr_expr ->
- int -> Constrexpr.constr_expr -> (Names.constant ->
+ int -> Constrexpr.constr_expr -> (Term.pconstant ->
Term.constr option ref ->
- Names.constant ->
- Names.constant -> int -> Term.types -> int -> Term.constr -> 'a) -> Constrexpr.constr_expr list -> unit
+ Term.pconstant ->
+ Term.pconstant -> int -> Term.types -> int -> Term.constr -> 'a) -> Constrexpr.constr_expr list -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:21:11 +0000