aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml18
-rw-r--r--plugins/funind/functional_principles_types.ml65
-rw-r--r--plugins/funind/functional_principles_types.mli2
-rw-r--r--plugins/funind/g_indfun.ml42
-rw-r--r--plugins/funind/glob_term_to_relation.ml91
-rw-r--r--plugins/funind/glob_term_to_relation.mli2
-rw-r--r--plugins/funind/indfun.ml20
-rw-r--r--plugins/funind/indfun_common.ml28
-rw-r--r--plugins/funind/indfun_common.mli8
-rw-r--r--plugins/funind/invfun.ml3
-rw-r--r--plugins/funind/merge.ml29
-rw-r--r--plugins/funind/recdef.ml62
-rw-r--r--plugins/funind/recdef.mli7
13 files changed, 187 insertions, 150 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index bd5fb1d923..62ca706264 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1,7 +1,7 @@
open Printer
open CErrors
open Util
-open Term
+open Constr
open EConstr
open Vars
open Namegen
@@ -44,6 +44,10 @@ let observe_tac s tac g = observe_tac_stream (str s) tac g
*)
+let pr_leconstr_fp =
+ let sigma, env = Pfedit.get_current_context () in
+ Printer.pr_leconstr_env env sigma
+
let debug_queue = Stack.create ()
let rec print_debug_queue e =
@@ -172,7 +176,7 @@ let is_incompatible_eq sigma t =
| _ -> false
with e when CErrors.noncritical e -> false
in
- if res then observe (str "is_incompatible_eq " ++ Printer.pr_leconstr t);
+ if res then observe (str "is_incompatible_eq " ++ pr_leconstr_fp t);
res
let change_hyp_with_using msg hyp_id t tac : tactic =
@@ -220,7 +224,8 @@ let find_rectype env sigma c =
let isAppConstruct ?(env=Global.env ()) sigma t =
try
let t',l = find_rectype env sigma t in
- observe (str "isAppConstruct : " ++ Printer.pr_leconstr t ++ str " -> " ++ Printer.pr_leconstr (applist (t',l)));
+ observe (str "isAppConstruct : " ++ Printer.pr_leconstr_env env sigma t ++ str " -> " ++
+ Printer.pr_leconstr_env env sigma (applist (t',l)));
true
with Not_found -> false
@@ -233,7 +238,8 @@ exception NoChange
let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
let nochange ?t' msg =
begin
- observe (str ("Not treating ( "^msg^" )") ++ pr_leconstr t ++ str " " ++ match t' with None -> str "" | Some t -> Printer.pr_leconstr t );
+ observe (str ("Not treating ( "^msg^" )") ++ pr_leconstr_env env sigma t ++ str " " ++
+ match t' with None -> str "" | Some t -> Printer.pr_leconstr_env env sigma t );
raise NoChange;
end
in
@@ -841,7 +847,7 @@ let build_proof
| Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
and build_proof do_finalize dyn_infos g =
(* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *)
- observe_tac_stream (str "build_proof with " ++ Printer.pr_leconstr dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g
+ observe_tac_stream (str "build_proof with " ++ pr_leconstr_fp dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g
and build_proof_args do_finalize dyn_infos (* f_args' args *) :tactic =
fun g ->
let (f_args',args) = dyn_infos.info in
@@ -1135,7 +1141,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
princ_params
);
observe (str "fbody_with_full_params := " ++
- pr_leconstr fbody_with_full_params
+ pr_leconstr_env (Global.env ()) !evd fbody_with_full_params
);
let all_funs_with_full_params =
Array.map (fun f -> applist(f, List.rev_map var_of_decl full_params)) all_funs
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 018b515170..7a9bbd92cf 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -1,7 +1,9 @@
open Printer
open CErrors
-open Util
open Term
+open Sorts
+open Util
+open Constr
open Vars
open Namegen
open Names
@@ -80,7 +82,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
let is_pte =
let set = List.fold_right Id.Set.add ptes_vars Id.Set.empty in
fun t ->
- match kind_of_term t with
+ match Constr.kind t with
| Var id -> Id.Set.mem id set
| _ -> false
in
@@ -100,13 +102,13 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
let pre_princ = EConstr.Unsafe.to_constr pre_princ in
let pre_princ = substl (List.map mkVar ptes_vars) pre_princ in
let is_dom c =
- match kind_of_term c with
+ match Constr.kind c with
| 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
+ match Constr.kind c with
| Ind((_,num),_) -> num
| Construct(((_,num),_),_) -> num
| _ -> assert false
@@ -114,12 +116,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
let dummy_var = mkVar (Id.of_string "________") in
let mk_replacement c i args =
let res = mkApp(rel_to_fun.(i), Array.map pop (array_get_start args)) in
- observe (str "replacing " ++ pr_lconstr c ++ str " by " ++ pr_lconstr res);
+ observe (str "replacing " ++
+ pr_lconstr_env env Evd.empty c ++ str " by " ++
+ pr_lconstr_env env Evd.empty res);
res
in
let rec compute_new_princ_type remove env pre_princ : types*(constr list) =
let (new_princ_type,_) as res =
- match kind_of_term pre_princ with
+ match Constr.kind pre_princ with
| Rel n ->
begin
try match Environ.lookup_rel n env with
@@ -149,12 +153,12 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
in
let new_f,binders_to_remove_from_f = compute_new_princ_type remove env f in
applistc new_f new_args,
- list_union_eq eq_constr binders_to_remove_from_f binders_to_remove
+ list_union_eq Constr.equal binders_to_remove_from_f binders_to_remove
| LetIn(x,v,t,b) ->
compute_new_princ_type_for_letin remove env x v t b
| _ -> pre_princ,[]
in
-(* let _ = match kind_of_term pre_princ with *)
+(* let _ = match Constr.kind pre_princ with *)
(* | Prod _ -> *)
(* observe(str "compute_new_princ_type for "++ *)
(* pr_lconstr_env env pre_princ ++ *)
@@ -170,13 +174,13 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
let new_x : Name.t = get_name (Termops.ids_of_context env) x in
let new_env = Environ.push_rel (LocalAssum (x,t)) env in
let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
- if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
- then (pop new_b), filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
+ if List.exists (Constr.equal (mkRel 1)) binders_to_remove_from_b
+ then (pop new_b), filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b
else
(
bind_fun(new_x,new_t,new_b),
list_union_eq
- eq_constr
+ Constr.equal
binders_to_remove_from_t
(List.map pop binders_to_remove_from_b)
)
@@ -189,7 +193,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
| Toberemoved_with_rel (n,c) ->
(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *)
let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in
- new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
+ new_b, list_add_set_eq Constr.equal (mkRel n) (List.map pop binders_to_remove_from_b)
end
and compute_new_princ_type_for_letin remove env x v t b =
begin
@@ -199,14 +203,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
let new_x : Name.t = get_name (Termops.ids_of_context env) x in
let new_env = Environ.push_rel (LocalDef (x,v,t)) env in
let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
- if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
- then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
+ if List.exists (Constr.equal (mkRel 1)) binders_to_remove_from_b
+ then (pop new_b),filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b
else
(
mkLetIn(new_x,new_v,new_t,new_b),
list_union_eq
- eq_constr
- (list_union_eq eq_constr binders_to_remove_from_t binders_to_remove_from_v)
+ Constr.equal
+ (list_union_eq Constr.equal binders_to_remove_from_t binders_to_remove_from_v)
(List.map pop binders_to_remove_from_b)
)
@@ -218,12 +222,12 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
| Toberemoved_with_rel (n,c) ->
(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *)
let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in
- new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
+ new_b, list_add_set_eq Constr.equal (mkRel n) (List.map pop binders_to_remove_from_b)
end
and compute_new_princ_type_with_acc remove env e (c_acc,to_remove_acc) =
let new_e,to_remove_from_e = compute_new_princ_type remove env e
in
- new_e::c_acc,list_union_eq eq_constr to_remove_from_e to_remove_acc
+ new_e::c_acc,list_union_eq Constr.equal to_remove_from_e to_remove_acc
in
(* observe (str "Computing new principe from " ++ pr_lconstr_env env_with_params_and_predicates pre_princ); *)
let pre_res,_ =
@@ -329,7 +333,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
| Some (id) -> id,id
| None ->
let id_of_f = Label.to_id (Constant.label (fst f)) in
- id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort)
+ id_of_f,Indrec.make_elimination_ident id_of_f (Sorts.family type_sort)
in
let names = ref [new_princ_name] in
let hook =
@@ -344,8 +348,11 @@ let generate_functional_principle (evd: Evd.evar_map ref)
let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in
(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
- let univs = (snd (Evd.universe_context ~names:[] ~extensible:true evd')) in
- let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs value in
+ let univs =
+ let poly = Flags.is_universe_polymorphism () in
+ Evd.const_univ_entry ~poly evd'
+ in
+ let ce = Declare.definition_entry ~univs value in
ignore(
Declare.declare_constant
name
@@ -389,7 +396,7 @@ exception Not_Rec
let get_funs_constant mp dp =
let get_funs_constant const e : (Names.Constant.t*int) array =
- match kind_of_term ((strip_lam e)) with
+ match Constr.kind ((strip_lam e)) with
| Fix((_,(na,_,_))) ->
Array.mapi
(fun i na ->
@@ -430,7 +437,7 @@ let get_funs_constant mp dp =
let first_params = List.hd l_params in
List.iter
(fun params ->
- if not (List.equal (fun (n1, c1) (n2, c2) -> Name.equal n1 n2 && eq_constr c1 c2) first_params params)
+ if not (List.equal (fun (n1, c1) (n2, c2) -> Name.equal n1 n2 && Constr.equal c1 c2) first_params params)
then user_err Pp.(str "Not a mutal recursive block")
)
l_params
@@ -439,7 +446,7 @@ let get_funs_constant mp dp =
let _check_bodies =
try
let extract_info is_first body =
- match kind_of_term body with
+ match Constr.kind body with
| Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca)
| _ ->
if is_first && Int.equal (List.length l_bodies) 1
@@ -450,7 +457,7 @@ let get_funs_constant mp dp =
let check body = (* Hope this is correct *)
let eq_infos (ia1, na1, ta1, ca1) (ia2, na2, ta2, ca2) =
Array.equal Int.equal ia1 ia2 && Array.equal Name.equal na1 na2 &&
- Array.equal eq_constr ta1 ta2 && Array.equal eq_constr ca1 ca2
+ Array.equal Constr.equal ta1 ta2 && Array.equal Constr.equal ca1 ca2
in
if not (eq_infos first_infos (extract_info false body))
then user_err Pp.(str "Not a mutal recursive block")
@@ -564,7 +571,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
List.map (* we can now compute the other principles *)
(fun scheme_type ->
incr i;
- observe (Printer.pr_lconstr scheme_type);
+ observe (Printer.pr_lconstr_env env sigma scheme_type);
let type_concl = (strip_prod_assum scheme_type) in
let applied_f = List.hd (List.rev (snd (decompose_app type_concl))) in
let f = fst (decompose_app applied_f) in
@@ -574,10 +581,10 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
let t = (strip_prod_assum t) in
let applied_g = List.hd (List.rev (snd (decompose_app t))) in
let g = fst (decompose_app applied_g) in
- if eq_constr f g
+ if Constr.equal f g
then raise (Found_type j);
- observe (Printer.pr_lconstr f ++ str " <> " ++
- Printer.pr_lconstr g)
+ observe (Printer.pr_lconstr_env env sigma f ++ str " <> " ++
+ Printer.pr_lconstr_env env sigma g)
)
ta;
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index 2eb1b7935d..a3315f22cf 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -7,7 +7,7 @@
(************************************************************************)
open Names
-open Term
+open Constr
val generate_functional_principle :
Evd.evar_map ref ->
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 829556a71e..87609296bc 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -154,7 +154,7 @@ VERNAC COMMAND EXTEND Function
| _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in
match
Vernac_classifier.classify_vernac
- (Vernacexpr.VernacFixpoint(None, List.map snd recsl))
+ (Vernacexpr.VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))
with
| Vernacexpr.VtSideff ids, _ when hard ->
Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index e8e5bfccc1..fa43536304 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1,7 +1,7 @@
open Printer
open Pp
open Names
-open Term
+open Constr
open Vars
open Glob_term
open Glob_ops
@@ -378,29 +378,30 @@ let add_pat_variables pat typ env : Environ.env =
fst (
Context.Rel.fold_outside
(fun decl (env,ctxt) ->
- let open Context.Rel.Declaration in
- match decl with
+ let open Context.Rel.Declaration in
+ let sigma, _ = Pfedit.get_current_context () in
+ match decl with
| LocalAssum (Anonymous,_) | LocalDef (Anonymous,_,_) -> assert false
| LocalAssum (Name id, t) ->
- let new_t = substl ctxt t in
- observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++
- str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++
- str "new type := " ++ Printer.pr_lconstr new_t ++ fnl ()
- );
- let open Context.Named.Declaration in
- (Environ.push_named (LocalAssum (id,new_t)) env,mkVar id::ctxt)
- | LocalDef (Name id, v, t) ->
- let new_t = substl ctxt t in
- let new_v = substl ctxt v in
- observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++
- str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++
- str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () ++
- str "old value := " ++ Printer.pr_lconstr v ++ fnl () ++
- str "new value := " ++ Printer.pr_lconstr new_v ++ fnl ()
- );
- let open Context.Named.Declaration in
- (Environ.push_named (LocalDef (id,new_v,new_t)) env,mkVar id::ctxt)
- )
+ let new_t = substl ctxt t in
+ observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++
+ str "old type := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++
+ str "new type := " ++ Printer.pr_lconstr_env env sigma new_t ++ fnl ()
+ );
+ let open Context.Named.Declaration in
+ (Environ.push_named (LocalAssum (id,new_t)) env,mkVar id::ctxt)
+ | LocalDef (Name id, v, t) ->
+ let new_t = substl ctxt t in
+ let new_v = substl ctxt v in
+ observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++
+ str "old type := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++
+ str "new type := " ++ Printer.pr_lconstr_env env sigma new_t ++ fnl () ++
+ str "old value := " ++ Printer.pr_lconstr_env env sigma v ++ fnl () ++
+ str "new value := " ++ Printer.pr_lconstr_env env sigma new_v ++ fnl ()
+ );
+ let open Context.Named.Declaration in
+ (Environ.push_named (LocalDef (id,new_v,new_t)) env,mkVar id::ctxt)
+ )
(Environ.rel_context new_env)
~init:(env,[])
)
@@ -478,7 +479,7 @@ let rec pattern_to_term_and_type env typ = DAst.with_val (function
let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
- observe (str " Entering : " ++ Printer.pr_glob_constr rt);
+ observe (str " Entering : " ++ Printer.pr_glob_constr_env env rt);
let open CAst in
match DAst.get rt with
| GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ ->
@@ -651,8 +652,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
try Inductiveops.find_inductive env (Evd.from_env env) b_typ
with Not_found ->
user_err (str "Cannot find the inductive associated to " ++
- Printer.pr_glob_constr b ++ str " in " ++
- Printer.pr_glob_constr rt ++ str ". try again with a cast")
+ Printer.pr_glob_constr_env env b ++ str " in " ++
+ Printer.pr_glob_constr_env env rt ++ str ". try again with a cast")
in
let case_pats = build_constructors_of_type (fst ind) [] in
assert (Int.equal (Array.length case_pats) 2);
@@ -683,8 +684,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
try Inductiveops.find_inductive env (Evd.from_env env) b_typ
with Not_found ->
user_err (str "Cannot find the inductive associated to " ++
- Printer.pr_glob_constr b ++ str " in " ++
- Printer.pr_glob_constr rt ++ str ". try again with a cast")
+ Printer.pr_glob_constr_env env b ++ str " in " ++
+ Printer.pr_glob_constr_env env rt ++ str ". try again with a cast")
in
let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in
assert (Int.equal (Array.length case_pats) 1);
@@ -896,24 +897,24 @@ let same_raw_term rt1 rt2 =
| GHole _, GHole _ -> true
| _ -> false
let decompose_raw_eq lhs rhs =
- let rec decompose_raw_eq lhs rhs acc =
- observe (str "decomposing eq for " ++ pr_glob_constr lhs ++ str " " ++ pr_glob_constr rhs);
- let (rhd,lrhs) = glob_decompose_app rhs in
- let (lhd,llhs) = glob_decompose_app lhs in
- observe (str "lhd := " ++ pr_glob_constr lhd);
- observe (str "rhd := " ++ pr_glob_constr rhd);
+ let _, env = Pfedit.get_current_context () in
+ let rec decompose_raw_eq lhs rhs acc =
+ observe (str "decomposing eq for " ++ pr_glob_constr_env env lhs ++ str " " ++ pr_glob_constr_env env rhs);
+ let (rhd,lrhs) = glob_decompose_app rhs in
+ let (lhd,llhs) = glob_decompose_app lhs in
+ observe (str "lhd := " ++ pr_glob_constr_env env lhd);
+ observe (str "rhd := " ++ pr_glob_constr_env env rhd);
observe (str "llhs := " ++ int (List.length llhs));
observe (str "lrhs := " ++ int (List.length lrhs));
- let sllhs = List.length llhs in
- let slrhs = List.length lrhs in
- if same_raw_term lhd rhd && Int.equal sllhs slrhs
+ let sllhs = List.length llhs in
+ let slrhs = List.length lrhs in
+ if same_raw_term lhd rhd && Int.equal sllhs slrhs
then
(* let _ = assert false in *)
List.fold_right2 decompose_raw_eq llhs lrhs acc
else (lhs,rhs)::acc
in
decompose_raw_eq lhs rhs []
-
exception Continue
(*
@@ -922,7 +923,7 @@ exception Continue
eliminates some meaningless equalities, applies some rewrites......
*)
let rec rebuild_cons env nb_args relname args crossed_types depth rt =
- observe (str "rebuilding : " ++ pr_glob_constr rt);
+ observe (str "rebuilding : " ++ pr_glob_constr_env env rt);
let open Context.Rel.Declaration in
let open CAst in
match DAst.get rt with
@@ -966,7 +967,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
let id = match DAst.get id with GVar id -> id | _ -> assert false in
begin
try
- observe (str "computing new type for eq : " ++ pr_glob_constr rt);
+ observe (str "computing new type for eq : " ++ pr_glob_constr_env env rt);
let t' =
try fst (Pretyping.understand env (Evd.from_env env) t)(*FIXME*)
with e when CErrors.noncritical e -> raise Continue
@@ -1011,11 +1012,11 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
let eq' =
DAst.make ?loc:loc1 @@ GApp(DAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;DAst.make ?loc:loc3 @@ GVar id;rt_typ;rt])
in
- observe (str "computing new type for jmeq : " ++ pr_glob_constr eq');
+ observe (str "computing new type for jmeq : " ++ pr_glob_constr_env env eq');
let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in
observe (str " computing new type for jmeq : done") ;
let new_args =
- match kind_of_term eq'_as_constr with
+ match Constr.kind eq'_as_constr with
| App(_,[|_;_;ty;_|]) ->
let ty = Array.to_list (snd (destApp ty)) in
let ty' = snd (Util.List.chop nparam ty) in
@@ -1098,7 +1099,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
rebuild_cons env nb_args relname args crossed_types depth new_rt
else raise Continue
with Continue ->
- observe (str "computing new type for prod : " ++ pr_glob_constr rt);
+ observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt);
let t',ctx = Pretyping.understand env (Evd.from_env env) t in
let new_env = Environ.push_rel (LocalAssum (n,t')) env in
let new_b,id_to_exclude =
@@ -1114,7 +1115,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
| _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
end
| _ ->
- observe (str "computing new type for prod : " ++ pr_glob_constr rt);
+ observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt);
let t',ctx = Pretyping.understand env (Evd.from_env env) t in
let new_env = Environ.push_rel (LocalAssum (n,t')) env in
let new_b,id_to_exclude =
@@ -1133,7 +1134,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
begin
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);
+ observe (str "computing new type for lambda : " ++ pr_glob_constr_env env rt);
let t',ctx = Pretyping.understand env (Evd.from_env env) t in
match n with
| Name id ->
@@ -1297,7 +1298,7 @@ let rec rebuild_return_type rt =
CAst.make @@ Constrexpr.CSort(GType []))
let do_build_inductive
- evd (funconstants: Term.pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list)
+ evd (funconstants: pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list)
returned_types
(rtl:glob_constr list) =
let _time1 = System.get_time () in
diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli
index 0cab5a6d35..ff0e98d00f 100644
--- a/plugins/funind/glob_term_to_relation.mli
+++ b/plugins/funind/glob_term_to_relation.mli
@@ -11,7 +11,7 @@ val build_inductive :
Id.t list -> (* The list of function name *)
*)
Evd.evar_map ->
- Term.pconstant list ->
+ Constr.pconstant list ->
(Name.t*Glob_term.glob_constr*Glob_term.glob_constr option) list list -> (* The list of function args *)
Constrexpr.constr_expr list -> (* The list of function returned type *)
Glob_term.glob_constr list -> (* the list of body *)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index dab094f913..9e22ad3063 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -1,7 +1,8 @@
open CErrors
+open Sorts
open Util
open Names
-open Term
+open Constr
open EConstr
open Pp
open Indfun_common
@@ -46,7 +47,7 @@ let functional_induction with_clean c princl pat =
try find_Function_infos c'
with Not_found ->
user_err (str "Cannot find induction information on "++
- Printer.pr_leconstr (mkConst c') )
+ Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') )
in
match Tacticals.elimination_sort_of_goal g with
| InProp -> finfo.prop_lemma
@@ -74,7 +75,7 @@ let functional_induction with_clean c princl pat =
(* mkConst(const_of_id princ_name ),g (\* FIXME *\) *)
with Not_found -> (* This one is neither defined ! *)
user_err (str "Cannot find induction principle for "
- ++Printer.pr_leconstr (mkConst c') )
+ ++ Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') )
in
let princ = EConstr.of_constr princ in
(princ,NoBindings,Tacmach.pf_unsafe_type_of g' princ,g')
@@ -841,12 +842,13 @@ let rec get_args b t : Constrexpr.local_binder_expr list *
let make_graph (f_ref:global_reference) =
let c,c_body =
match f_ref with
- | ConstRef c ->
- begin try c,Global.lookup_constant c
- with Not_found ->
- raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr (mkConst c)) )
- end
- | _ -> raise (UserError (None, str "Not a function reference") )
+ | ConstRef c ->
+ begin try c,Global.lookup_constant c
+ with Not_found ->
+ let sigma, env = Pfedit.get_current_context () in
+ raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr_env env sigma (mkConst c)) )
+ end
+ | _ -> raise (UserError (None, str "Not a function reference") )
in
(match Global.body_of_constant_body c_body with
| None -> error "Cannot build a graph over an axiom!"
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 76fcd5ec87..8bf6e48fdb 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -1,8 +1,10 @@
open Names
open Pp
+open Constr
open Libnames
open Globnames
open Refiner
+
let mk_prefix pre id = Id.of_string (pre^(Id.to_string id))
let mk_rel_id = mk_prefix "R_"
let mk_correct_id id = Nameops.add_suffix (mk_rel_id id) "_correct"
@@ -111,7 +113,7 @@ let const_of_id id =
(str "cannot find " ++ Id.print id)
let def_of_const t =
- match (Term.kind_of_term t) with
+ match Constr.kind t with
Term.Const sp ->
(try (match Environ.constant_opt_value_in (Global.env()) sp with
| Some c -> c
@@ -330,18 +332,18 @@ let discharge_Function (_,finfos) =
is_general = finfos.is_general
}
-open Term
-
let pr_ocst c =
- Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) c (mt ())
+ let sigma, env = Pfedit.get_current_context () in
+ Option.fold_right (fun v acc -> Printer.pr_lconstr_env env sigma (mkConst v)) c (mt ())
let pr_info f_info =
+ let sigma, env = Pfedit.get_current_context () in
str "function_constant := " ++
- Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++
+ Printer.pr_lconstr_env env sigma (mkConst f_info.function_constant)++ fnl () ++
str "function_constant_type := " ++
(try
- Printer.pr_lconstr
- (fst (Global.type_of_global_in_context (Global.env ()) (ConstRef f_info.function_constant)))
+ Printer.pr_lconstr_env env sigma
+ (fst (Global.type_of_global_in_context env (ConstRef f_info.function_constant)))
with e when CErrors.noncritical e -> mt ()) ++ fnl () ++
str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++
str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++
@@ -349,7 +351,7 @@ let pr_info f_info =
str "rect_lemma := " ++ pr_ocst f_info.rect_lemma ++ fnl () ++
str "rec_lemma := " ++ pr_ocst f_info.rec_lemma ++ fnl () ++
str "prop_lemma := " ++ pr_ocst f_info.prop_lemma ++ fnl () ++
- str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl ()
+ str "graph_ind := " ++ Printer.pr_lconstr_env env sigma (mkInd f_info.graph_ind) ++ fnl ()
let pr_table tb =
let l = Cmap_env.fold (fun k v acc -> v::acc) tb [] in
@@ -545,16 +547,16 @@ let prodn n env b =
(* compose_prod [xn:Tn;..;x1:T1] b = (x1:T1)..(xn:Tn)b *)
let compose_prod l b = prodn (List.length l) l b
-type tcc_lemma_value =
+type tcc_lemma_value =
| Undefined
- | Value of Term.constr
+ | Value of constr
| Not_needed
-(* We only "purify" on exceptions *)
+(* We only "purify" on exceptions. XXX: What is this doing here? *)
let funind_purify f x =
- let st = Vernacentries.freeze_interp_state `No in
+ let st = Vernacstate.freeze_interp_state `No in
try f x
with e ->
let e = CErrors.push e in
- Vernacentries.unfreeze_interp_state st;
+ Vernacstate.unfreeze_interp_state st;
Exninfo.iraise e
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index d41abee87e..5cc7163aa3 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -38,7 +38,7 @@ val chop_rlambda_n : int -> Glob_term.glob_constr ->
val chop_rprod_n : int -> Glob_term.glob_constr ->
(Name.t*Glob_term.glob_constr) list * Glob_term.glob_constr
-val def_of_const : Term.constr -> Term.constr
+val def_of_const : Constr.t -> Constr.t
val eq : EConstr.constr Lazy.t
val refl_equal : EConstr.constr Lazy.t
val const_of_id: Id.t -> Globnames.global_reference(* constantyes *)
@@ -118,10 +118,10 @@ val decompose_lam_n : Evd.evar_map -> int -> EConstr.t ->
(Names.Name.t * EConstr.t) list * EConstr.t
val compose_lam : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t
val compose_prod : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t
-
-type tcc_lemma_value =
+
+type tcc_lemma_value =
| Undefined
- | Value of Term.constr
+ | Value of Constr.t
| Not_needed
val funind_purify : ('a -> 'b) -> ('a -> 'b)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 93317fce1b..694c800514 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -12,6 +12,7 @@ open CErrors
open Util
open Names
open Term
+open Constr
open EConstr
open Vars
open Pp
@@ -850,7 +851,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt
in
let type_of_lemma = nf_zeta type_of_lemma in
- observe (str "type_of_lemma := " ++ Printer.pr_leconstr type_of_lemma);
+ observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env env !evd type_of_lemma);
type_of_lemma,type_info
)
funs_constr
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 77c26f8ce6..9e2774ff32 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -18,6 +18,7 @@ open Vernacexpr
open Pp
open Names
open Term
+open Constr
open Vars
open Declarations
open Glob_term
@@ -36,19 +37,19 @@ let rec popn i c = if i<=0 then c else pop (popn (i-1) c)
(** Substitutions in constr *)
let compare_constr_nosub t1 t2 =
- if compare_constr (fun _ _ -> false) t1 t2
+ if Constr.compare_head (fun _ _ -> false) t1 t2
then true
else false
let rec compare_constr' t1 t2 =
if compare_constr_nosub t1 t2
then true
- else (compare_constr (compare_constr') t1 t2)
+ else (Constr.compare_head (compare_constr') t1 t2)
let rec substitterm prof t by_t in_u =
if (compare_constr' (lift prof t) in_u)
then (lift prof by_t)
- else map_constr_with_binders succ
+ else Constr.map_with_binders succ
(fun i -> substitterm i t by_t) prof in_u
let lift_ldecl n ldecl = List.map (fun (x,y) -> x,lift n y) ldecl
@@ -89,20 +90,28 @@ let next_ident_fresh (id:Id.t) =
(* comment this line to see debug msgs *)
let msg x = () ;; let pr_lconstr c = str ""
(* uncomment this to see debugging *)
-let prconstr c = msg (str" " ++ Printer.pr_lconstr c)
-let prconstrnl c = msg (str" " ++ Printer.pr_lconstr c ++ str"\n")
+let prconstr c =
+ let sigma, env = Pfedit.get_current_context () in
+ msg (str" " ++ Printer.pr_lconstr_env env sigma c)
+
+let prconstrnl c =
+ let sigma, env = Pfedit.get_current_context () in
+ msg (str" " ++ Printer.pr_lconstr_env env sigma c ++ str"\n")
+
let prlistconstr lc = List.iter prconstr lc
let prstr s = msg(str s)
let prNamedConstr s c =
+ let sigma, env = Pfedit.get_current_context () in
begin
msg(str "");
- msg(str(s^" {§ ") ++ Printer.pr_lconstr c ++ str " §} ");
+ msg(str(s^" {§ ") ++ Printer.pr_lconstr_env env sigma c ++ str " §} ");
msg(str "");
end
let prNamedRConstr s c =
+ let sigma, env = Pfedit.get_current_context () in
begin
msg(str "");
- msg(str(s^" {§ ") ++ Printer.pr_glob_constr c ++ str " §} ");
+ msg(str(s^" {§ ") ++ Printer.pr_glob_constr_env env c ++ str " §} ");
msg(str "");
end
let prNamedLConstr_aux lc = List.iter (prNamedConstr "\n") lc
@@ -954,16 +963,16 @@ let funify_branches relinfo nfuns branch =
| Some (IndRef ((mutual_ind,i) as ind)) -> mutual_ind,ind
| _ -> assert false in
let is_dom c =
- match kind_of_term c with
+ match Constr.kind c with
| Ind(((u,_),_)) | Construct(((u,_),_),_) -> MutInd.equal u mut_induct
| _ -> false in
let _dom_i c =
assert (is_dom c);
- match kind_of_term c with
+ match Constr.kind c with
| Ind((u,i)) | Construct((u,_),i) -> i
| _ -> assert false in
let _is_pred c shift =
- match kind_of_term c with
+ match Constr.kind c with
| Rel i -> let reali = i-shift in (reali>=0 && reali<relinfo.nbranches)
| _ -> false in
(* FIXME: *)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 76f859ed72..b0a76137b7 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -9,7 +9,7 @@
module CVars = Vars
-open Term
+open Constr
open EConstr
open Vars
open Namegen
@@ -53,6 +53,10 @@ let coq_constant m s = EConstr.of_constr @@ Universes.constr_of_global @@
let arith_Nat = ["Arith";"PeanoNat";"Nat"]
let arith_Lt = ["Arith";"Lt"]
+let pr_leconstr_rd =
+ let sigma, env = Pfedit.get_current_context () in
+ Printer.pr_leconstr_env env sigma
+
let coq_init_constant s =
EConstr.of_constr (
Universes.constr_of_global @@
@@ -62,14 +66,14 @@ 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 f_id kind ?(ctx=Univ.UContext.empty) value =
- let ce = definition_entry ~univs:ctx value (*FIXME *) in
+let declare_fun f_id kind ?univs value =
+ let ce = definition_entry ?univs value (*FIXME *) in
ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Transparent,None)))
let def_of_const t =
- match (kind_of_term t) with
+ match (Constr.kind t) with
Const sp ->
(try (match constant_opt_value_in (Global.env ()) sp with
| Some c -> c
@@ -143,7 +147,7 @@ let nat = function () -> (coq_init_constant "nat")
let iter_ref () =
try find_reference ["Recdef"] "iter"
with Not_found -> user_err Pp.(str "module Recdef not loaded")
-let iter = function () -> (constr_of_global (delayed_force iter_ref))
+let iter_rd = function () -> (constr_of_global (delayed_force iter_ref))
let eq = function () -> (coq_init_constant "eq")
let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS")
let le_lt_n_Sm = function () -> (coq_constant arith_Lt "le_lt_n_Sm")
@@ -175,8 +179,9 @@ let simpl_iter clause =
clause
(* Others ugly things ... *)
-let (value_f:Term.constr list -> global_reference -> Term.constr) =
+let (value_f: Constr.t list -> global_reference -> Constr.t) =
let open Term in
+ let open Constr in
fun al fterm ->
let rev_x_id_l =
(
@@ -207,7 +212,7 @@ let (value_f:Term.constr list -> global_reference -> Term.constr) =
let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in
it_mkLambda_or_LetIn body context
-let (declare_f : Id.t -> logical_kind -> Term.constr list -> global_reference -> global_reference) =
+let (declare_f : Id.t -> logical_kind -> Constr.t list -> global_reference -> global_reference) =
fun f_id kind input_type fterm_ref ->
declare_fun f_id kind (value_f input_type fterm_ref);;
@@ -335,7 +340,8 @@ let check_not_nested sigma forbidden e =
try
check_not_nested e
with UserError(_,p) ->
- user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_leconstr e ++ str " " ++ p)
+ let _, env = Pfedit.get_current_context () in
+ user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_leconstr_env env sigma e ++ str " " ++ p)
(* ['a info] contains the local information for traveling *)
type 'a infos =
@@ -453,7 +459,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
jinfo.otherS () expr_info continuation_tac expr_info g
with e when CErrors.noncritical e ->
- user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
+ user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
end
| Lambda(n,t,b) ->
begin
@@ -461,7 +467,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
jinfo.otherS () expr_info continuation_tac expr_info g
with e when CErrors.noncritical e ->
- user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
+ user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
end
| Case(ci,t,a,l) ->
begin
@@ -489,8 +495,8 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
jinfo.apP (f,args) expr_info continuation_tac in
travel_args jinfo
expr_info.is_main_branch new_continuation_tac new_infos g
- | Case _ -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)")
- | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr expr_info.info ++ Pp.str ".")
+ | Case _ -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)")
+ | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ Pp.str ".")
end
| Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} g
| Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ ->
@@ -513,7 +519,7 @@ and travel_args jinfo is_final continuation_tac infos =
{infos with info=arg;is_final=false}
and travel jinfo continuation_tac expr_info =
observe_tac
- (str jinfo.message ++ Printer.pr_leconstr expr_info.info)
+ (str jinfo.message ++ pr_leconstr_rd expr_info.info)
(travel_aux jinfo continuation_tac expr_info)
(* Termination proof *)
@@ -729,7 +735,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
let destruct_tac,rev_to_thin_intro =
mkDestructEq [expr_info.rec_arg_id] a' g in
let to_thin_intro = List.rev rev_to_thin_intro in
- observe_tac (str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr a')
+ observe_tac (str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr_env (pf_env g) sigma a')
(try
(tclTHENS
destruct_tac
@@ -738,7 +744,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
with
| UserError(Some "Refiner.thensn_tac3",_)
| UserError(Some "Refiner.tclFAIL_s",_) ->
- (observe_tac (str "is computable " ++ Printer.pr_leconstr new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} )
+ (observe_tac (str "is computable " ++ Printer.pr_leconstr_env (pf_env g) sigma new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} )
))
g
@@ -989,11 +995,11 @@ let rec intros_values_eq expr_info acc =
let equation_others _ expr_info continuation_tac infos =
if expr_info.is_final && expr_info.is_main_branch
then
- observe_tac (str "equation_others (cont_tac +intros) " ++ Printer.pr_leconstr expr_info.info)
+ observe_tac (str "equation_others (cont_tac +intros) " ++ pr_leconstr_rd expr_info.info)
(tclTHEN
(continuation_tac infos)
- (observe_tac (str "intros_values_eq equation_others " ++ Printer.pr_leconstr expr_info.info) (intros_values_eq expr_info [])))
- else observe_tac (str "equation_others (cont_tac) " ++ Printer.pr_leconstr expr_info.info) (continuation_tac infos)
+ (observe_tac (str "intros_values_eq equation_others " ++ pr_leconstr_rd expr_info.info) (intros_values_eq expr_info [])))
+ else observe_tac (str "equation_others (cont_tac) " ++ pr_leconstr_rd expr_info.info) (continuation_tac infos)
let equation_app f_and_args expr_info continuation_tac infos =
if expr_info.is_final && expr_info.is_main_branch
@@ -1039,11 +1045,12 @@ let prove_eq = travel equation_info
*)
let compute_terminate_type nb_args func =
let open Term in
+ let open Constr in
let open CVars in
let _,a_arrow_b,_ = destLambda(def_of_const (constr_of_global func)) in
let rev_args,b = decompose_prod_n nb_args a_arrow_b in
let left =
- mkApp(delayed_force iter,
+ mkApp(delayed_force iter_rd,
Array.of_list
(lift 5 a_arrow_b:: mkRel 3::
constr_of_global func::mkRel 1::
@@ -1222,8 +1229,8 @@ 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
- sigma, List.map (Goal.V82.abstract_type sigma) sgs
+ let sgs,_,_,_,sigma = Proof.proof p in
+ sigma, List.map (Goal.V82.abstract_type sigma) sgs
exception EmptySubgoals
let build_and_l sigma l =
@@ -1416,7 +1423,7 @@ let com_terminate
nb_args ctx
hook =
let start_proof ctx (tac_start:tactic) (tac_end:tactic) =
- let (evmap, env) = Lemmas.get_current_context() in
+ let evmap, env = Pfedit.get_current_context () in
Lemmas.start_proof thm_name
(Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env)
ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) hook;
@@ -1460,7 +1467,7 @@ let start_equation (f:global_reference) (term_f:global_reference)
let (com_eqn : int -> Id.t ->
global_reference -> global_reference -> global_reference
- -> Term.constr -> unit) =
+ -> Constr.t -> unit) =
fun nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type ->
let open CVars in
let opacity =
@@ -1468,7 +1475,7 @@ let (com_eqn : int -> Id.t ->
| ConstRef c -> is_opaque_constant c
| _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.")
in
- let (evmap, env) = Lemmas.get_current_context() in
+ let evmap, env = Pfedit.get_current_context () in
let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in
let f_constr = constr_of_global f_ref in
let equation_lemma_type = subst1 f_constr equation_lemma_type in
@@ -1514,6 +1521,7 @@ 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 open Term in
+ let open Constr in
let open CVars in
let env = Global.env() in
let evd = ref (Evd.from_env env) in
@@ -1536,7 +1544,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
(* Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *)
(* Pp.msgnl (str "rec_arg_num := " ++ str (string_of_int rec_arg_num)); *)
(* Pp.msgnl (str "eq' := " ++ str (string_of_int rec_arg_num)); *)
- match kind_of_term eq' with
+ match Constr.kind eq' with
| App(e,[|_;_;eq_fix|]) ->
mkLambda (Name function_name,function_type,subst_var function_name (compose_lam res_vars eq_fix))
| _ -> failwith "Recursive Definition (res not eq)"
@@ -1548,8 +1556,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let functional_id = add_suffix function_name "_F" in
let term_id = add_suffix function_name "_terminate" in
let functional_ref =
- let ctx = (snd (Evd.universe_context ~names:[] ~extensible:true evm)) in
- declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx res
+ let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evm) in
+ declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res
in
(* Refresh the global universes, now including those of _F *)
let evm = Evd.from_env (Global.env ()) in
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index 63bbdbe7e3..50b84731b5 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -1,3 +1,4 @@
+open Constr
(* val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference *)
val tclUSER_if_not_mes :
@@ -11,9 +12,9 @@ bool ->
Constrintern.internalization_env ->
Constrexpr.constr_expr ->
Constrexpr.constr_expr ->
- int -> Constrexpr.constr_expr -> (Term.pconstant ->
+ int -> Constrexpr.constr_expr -> (pconstant ->
Indfun_common.tcc_lemma_value ref ->
- Term.pconstant ->
- Term.pconstant -> int -> EConstr.types -> int -> EConstr.constr -> 'a) -> Constrexpr.constr_expr list -> unit
+ pconstant ->
+ pconstant -> int -> EConstr.types -> int -> EConstr.constr -> 'a) -> Constrexpr.constr_expr list -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 09:08:46 +0000