aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--parsing/pptactic.ml7
-rw-r--r--parsing/printer.ml19
-rw-r--r--plugins/cc/cctac.ml39
-rw-r--r--plugins/dp/dp.ml9
-rw-r--r--plugins/funind/functional_principles_proofs.ml25
-rw-r--r--plugins/funind/functional_principles_types.ml23
-rw-r--r--plugins/funind/invfun.ml3
-rw-r--r--plugins/funind/recdef.ml31
-rw-r--r--plugins/omega/coq_omega.ml3
-rw-r--r--plugins/rtauto/refl_tauto.ml5
-rw-r--r--plugins/setoid_ring/newring.ml43
-rw-r--r--plugins/subtac/subtac_classes.ml1
-rw-r--r--plugins/subtac/subtac_command.ml3
-rw-r--r--plugins/subtac/subtac_pretyping_F.ml17
-rw-r--r--plugins/subtac/subtac_utils.ml13
-rw-r--r--pretyping/indrec.ml49
-rw-r--r--pretyping/recordops.ml5
-rw-r--r--tactics/extratactics.ml415
-rw-r--r--toplevel/classes.ml1
-rw-r--r--toplevel/record.ml23
-rw-r--r--toplevel/whelp.ml43
21 files changed, 138 insertions, 159 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 64b8b7bc9..6f0896cc8 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -19,7 +19,6 @@ open Pattern
open Ppextend
open Ppconstr
open Printer
-open Termops
let pr_global x = Nametab.pr_global_env Idset.empty x
@@ -388,11 +387,11 @@ let pr_by_tactic prt = function
| tac -> spc() ++ str "by " ++ prt tac
let pr_hyp_location pr_id = function
- | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs
- | occs, InHypTypeOnly ->
+ | occs, Termops.InHyp -> spc () ++ pr_with_occurrences pr_id occs
+ | occs, Termops.InHypTypeOnly ->
spc () ++
pr_with_occurrences (fun id -> str "(type of " ++ pr_id id ++ str ")") occs
- | occs, InHypValueOnly ->
+ | occs, Termops.InHypValueOnly ->
spc () ++
pr_with_occurrences (fun id -> str "(value of " ++ pr_id id ++ str ")") occs
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 34637b1e8..c575fde52 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -11,7 +11,6 @@ open Util
open Names
open Nameops
open Term
-open Termops
open Sign
open Environ
open Global
@@ -62,7 +61,7 @@ let pr_constr_under_binders_env_gen pr env (ids,c) =
(* we also need to preserve the actual names of the patterns *)
(* So what to do? *)
let assums = List.map (fun id -> (Name id,(* dummy *) mkProp)) ids in
- pr (push_rels_assum assums env) c
+ pr (Termops.push_rels_assum assums env) c
let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_constr_env
let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_lconstr_env
@@ -88,9 +87,9 @@ let pr_ljudge_env env j =
let pr_ljudge j = pr_ljudge_env (Global.env()) j
let pr_lrawconstr_env env c =
- pr_lconstr_expr (extern_rawconstr (vars_of_env env) c)
+ pr_lconstr_expr (extern_rawconstr (Termops.vars_of_env env) c)
let pr_rawconstr_env env c =
- pr_constr_expr (extern_rawconstr (vars_of_env env) c)
+ pr_constr_expr (extern_rawconstr (Termops.vars_of_env env) c)
let pr_lrawconstr c =
pr_lconstr_expr (extern_rawconstr Idset.empty c)
@@ -101,14 +100,14 @@ let pr_cases_pattern t =
pr_cases_pattern_expr (extern_cases_pattern Idset.empty t)
let pr_lconstr_pattern_env env c =
- pr_lconstr_pattern_expr (extern_constr_pattern (names_of_rel_context env) c)
+ pr_lconstr_pattern_expr (extern_constr_pattern (Termops.names_of_rel_context env) c)
let pr_constr_pattern_env env c =
- pr_constr_pattern_expr (extern_constr_pattern (names_of_rel_context env) c)
+ pr_constr_pattern_expr (extern_constr_pattern (Termops.names_of_rel_context env) c)
let pr_lconstr_pattern t =
- pr_lconstr_pattern_expr (extern_constr_pattern empty_names_context t)
+ pr_lconstr_pattern_expr (extern_constr_pattern Termops.empty_names_context t)
let pr_constr_pattern t =
- pr_constr_pattern_expr (extern_constr_pattern empty_names_context t)
+ pr_constr_pattern_expr (extern_constr_pattern Termops.empty_names_context t)
let pr_sort s = pr_rawsort (extern_sort s)
@@ -120,7 +119,7 @@ let _ = Termops.set_print_constr pr_lconstr_env
let pr_global_env = pr_global_env
let pr_global = pr_global_env Idset.empty
-let pr_constant env cst = pr_global_env (vars_of_env env) (ConstRef cst)
+let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst)
let pr_existential env ev = pr_lconstr_env env (mkEvar ev)
let pr_inductive env ind = pr_lconstr_env env (mkInd ind)
let pr_constructor env cstr = pr_lconstr_env env (mkConstruct cstr)
@@ -438,7 +437,7 @@ let pr_prim_rule = function
| [] -> mt () in
(str"cofix " ++ pr_id f ++ str" with " ++ print_mut others)
| Refine c ->
- str(if occur_meta c then "refine " else "exact ") ++
+ str(if Termops.occur_meta c then "refine " else "exact ") ++
Constrextern.with_meta_as_hole pr_constr c
| Convert_concl (c,_) ->
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 1054b6ecd..ec31f8917 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -18,7 +18,6 @@ open Nameops
open Inductiveops
open Declarations
open Term
-open Termops
open Tacmach
open Tactics
open Tacticals
@@ -64,8 +63,8 @@ let rec decompose_term env sigma t=
let tf=decompose_term env sigma f in
let targs=Array.map (decompose_term env sigma) args in
Array.fold_left (fun s t->Appli (s,t)) tf targs
- | Prod (_,a,_b) when not (dependent (mkRel 1) _b) ->
- let b = pop _b in
+ | Prod (_,a,_b) when not (Termops.dependent (mkRel 1) _b) ->
+ let b = Termops.pop _b in
let sort_b = sf_of env sigma b in
let sort_a = sf_of env sigma a in
Appli(Appli(Product (sort_a,sort_b) ,
@@ -111,8 +110,8 @@ let rec pattern_of_constr env sigma c =
(array_map_to_list (pattern_of_constr env sigma) args) in
PApp (pf,List.rev pargs),
List.fold_left Intset.union Intset.empty lrels
- | Prod (_,a,_b) when not (dependent (mkRel 1) _b) ->
- let b =pop _b in
+ | Prod (_,a,_b) when not (Termops.dependent (mkRel 1) _b) ->
+ let b = Termops.pop _b in
let pa,sa = pattern_of_constr env sigma a in
let pb,sb = pattern_of_constr env sigma b in
let sort_b = sf_of env sigma b in
@@ -258,19 +257,19 @@ let rec proof_tac p gls =
| SymAx c ->
let l=constr_of_term p.p_lhs and
r=constr_of_term p.p_rhs in
- let typ = refresh_universes (pf_type_of gls l) in
+ let typ = Termops.refresh_universes (pf_type_of gls l) in
exact_check
(mkApp(Lazy.force _sym_eq,[|typ;r;l;c|])) gls
| Refl t ->
let lr = constr_of_term t in
- let typ = refresh_universes (pf_type_of gls lr) in
+ let typ = Termops.refresh_universes (pf_type_of gls lr) in
exact_check
(mkApp(Lazy.force _refl_equal,[|typ;constr_of_term t|])) gls
| Trans (p1,p2)->
let t1 = constr_of_term p1.p_lhs and
t2 = constr_of_term p1.p_rhs and
t3 = constr_of_term p2.p_rhs in
- let typ = refresh_universes (pf_type_of gls t2) in
+ let typ = Termops.refresh_universes (pf_type_of gls t2) in
let prf =
mkApp(Lazy.force _trans_eq,[|typ;t1;t2;t3;_M 1;_M 2|]) in
tclTHENS (refine prf) [(proof_tac p1);(proof_tac p2)] gls
@@ -279,9 +278,9 @@ let rec proof_tac p gls =
and tx1=constr_of_term p2.p_lhs
and tf2=constr_of_term p1.p_rhs
and tx2=constr_of_term p2.p_rhs in
- let typf = refresh_universes (pf_type_of gls tf1) in
- let typx = refresh_universes (pf_type_of gls tx1) in
- let typfx = refresh_universes (pf_type_of gls (mkApp (tf1,[|tx1|]))) in
+ let typf = Termops.refresh_universes (pf_type_of gls tf1) in
+ let typx = Termops.refresh_universes (pf_type_of gls tx1) in
+ let typfx = Termops.refresh_universes (pf_type_of gls (mkApp (tf1,[|tx1|]))) in
let id = pf_get_new_id (id_of_string "f") gls in
let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
let lemma1 =
@@ -309,8 +308,8 @@ let rec proof_tac p gls =
let ti=constr_of_term prf.p_lhs in
let tj=constr_of_term prf.p_rhs in
let default=constr_of_term p.p_lhs in
- let intype=refresh_universes (pf_type_of gls ti) in
- let outtype=refresh_universes (pf_type_of gls default) in
+ let intype = Termops.refresh_universes (pf_type_of gls ti) in
+ let outtype = Termops.refresh_universes (pf_type_of gls default) in
let special=mkRel (1+nargs-argind) in
let proj=build_projection intype outtype cstr special default gls in
let injt=
@@ -319,7 +318,7 @@ let rec proof_tac p gls =
let refute_tac c t1 t2 p gls =
let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
- let intype=refresh_universes (pf_type_of gls tt1) in
+ let intype = Termops.refresh_universes (pf_type_of gls tt1) in
let neweq=
mkApp(Lazy.force _eq,
[|intype;tt1;tt2|]) in
@@ -330,7 +329,7 @@ let refute_tac c t1 t2 p gls =
let convert_to_goal_tac c t1 t2 p gls =
let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
- let sort=refresh_universes (pf_type_of gls tt2) in
+ let sort = Termops.refresh_universes (pf_type_of gls tt2) in
let neweq=mkApp(Lazy.force _eq,[|sort;tt1;tt2|]) in
let e=pf_get_new_id (id_of_string "e") gls in
let x=pf_get_new_id (id_of_string "X") gls in
@@ -350,14 +349,14 @@ let convert_to_hyp_tac c1 t1 c2 t2 p gls =
let discriminate_tac cstr p gls =
let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
- let intype=refresh_universes (pf_type_of gls t1) in
+ let intype = Termops.refresh_universes (pf_type_of gls t1) in
let concl=pf_concl gls in
- let outsort=mkType (new_univ ()) in
+ let outsort = mkType (Termops.new_univ ()) in
let xid=pf_get_new_id (id_of_string "X") gls in
let tid=pf_get_new_id (id_of_string "t") gls in
let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in
let trivial=pf_type_of gls identity in
- let outtype=mkType (new_univ ()) in
+ let outtype = mkType (Termops.new_univ ()) in
let pred=mkLambda(Name xid,outtype,mkRel 1) in
let hid=pf_get_new_id (id_of_string "Heq") gls in
let proj=build_projection intype outtype cstr trivial concl gls in
@@ -412,7 +411,7 @@ let cc_tactic depth additionnal_terms gls=
str "\"congruence with (" ++
prlist_with_sep
(fun () -> str ")" ++ pr_spc () ++ str "(")
- (print_constr_env (pf_env gls))
+ (Termops.print_constr_env (pf_env gls))
terms_to_complete ++
str ")\","
end);
@@ -454,7 +453,7 @@ let simple_reflexivity () = apply (Lazy.force _refl_equal)
let f_equal gl =
let cut_eq c1 c2 =
- let ty = refresh_universes (pf_type_of gl c1) in
+ let ty = Termops.refresh_universes (pf_type_of gl c1) in
tclTHENTRY
(Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|])))
(simple_reflexivity ())
diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml
index b800170de..22ae4aaf9 100644
--- a/plugins/dp/dp.ml
+++ b/plugins/dp/dp.ml
@@ -23,7 +23,6 @@ open Fol
open Names
open Nameops
open Namegen
-open Termops
open Coqlib
open Hipattern
open Libnames
@@ -148,7 +147,7 @@ let fresh_var = function
env names, and returns the new variables together with the new
environment *)
let coq_rename_vars env vars =
- let avoid = ref (ids_of_named_context (Environ.named_context env)) in
+ let avoid = ref (Termops.ids_of_named_context (Environ.named_context env)) in
List.fold_right
(fun (na,t) (newvars, newenv) ->
let id = next_name_away na !avoid in
@@ -183,7 +182,7 @@ let decomp_type_lambdas env t =
let decompose_arrows =
let rec arrows_rec l c = match kind_of_term c with
- | Prod (_,t,c) when not (dependent (mkRel 1) c) -> arrows_rec (t :: l) c
+ | Prod (_,t,c) when not (Termops.dependent (mkRel 1) c) -> arrows_rec (t :: l) c
| Cast (c,_,_) -> arrows_rec l c
| _ -> List.rev l, c
in
@@ -195,8 +194,8 @@ let rec eta_expanse t vars env i =
t, vars, env
else
match kind_of_term (Typing.type_of env Evd.empty t) with
- | Prod (n, a, b) when not (dependent (mkRel 1) b) ->
- let avoid = ids_of_named_context (Environ.named_context env) in
+ | Prod (n, a, b) when not (Termops.dependent (mkRel 1) b) ->
+ let avoid = Termops.ids_of_named_context (Environ.named_context env) in
let id = next_name_away n avoid in
let env' = Environ.push_named (id, None, a) env in
let t' = mkApp (t, [| mkVar id |]) in
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index bc12fcea9..43658e802 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1,7 +1,6 @@
open Printer
open Util
open Term
-open Termops
open Namegen
open Names
open Declarations
@@ -263,7 +262,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
in
let sub = compute_substitution Intmap.empty (snd t1) (snd t2) in
let sub = compute_substitution sub (fst t1) (fst t2) in
- let end_of_type_with_pop = pop end_of_type in (*the equation will be removed *)
+ let end_of_type_with_pop = Termops.pop end_of_type in (*the equation will be removed *)
let new_end_of_type =
(* Ugly hack to prevent Map.fold order change between ocaml-3.08.3 and ocaml-3.08.4
Can be safely replaced by the next comment for Ocaml >= 3.08.4
@@ -286,7 +285,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
try
let witness = Intmap.find i sub in
if b' <> None then anomaly "can not redefine a rel!";
- (pop end_of_type,ctxt_size,mkLetIn(x',witness,t',witness_fun))
+ (Termops.pop end_of_type,ctxt_size,mkLetIn(x',witness,t',witness_fun))
with Not_found ->
(mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun)
)
@@ -411,7 +410,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
begin
let pte,pte_args = (destApp t_x) in
let (* fix_info *) prove_rec_hyp = (Idmap.find (destVar pte) ptes_infos).proving_tac in
- let popped_t' = pop t' in
+ let popped_t' = Termops.pop t' in
let real_type_of_hyp = it_mkProd_or_LetIn popped_t' context in
let prove_new_type_of_hyp =
let context_length = List.length context in
@@ -461,7 +460,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
(* observe (str "In "++Ppconstr.pr_id hyp_id++ *)
(* str " removing useless precond True" *)
(* ); *)
- let popped_t' = pop t' in
+ let popped_t' = Termops.pop t' in
let real_type_of_hyp =
it_mkProd_or_LetIn popped_t' context
in
@@ -489,7 +488,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
]
else if is_trivial_eq t_x
then (* t_x := t = t => we remove this precond *)
- let popped_t' = pop t' in
+ let popped_t' = Termops.pop t' in
let real_type_of_hyp =
it_mkProd_or_LetIn popped_t' context
in
@@ -589,7 +588,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
let fun_body =
mkLambda(Anonymous,
pf_type_of g' term,
- replace_term term (mkRel 1) dyn_infos.info
+ Termops.replace_term term (mkRel 1) dyn_infos.info
)
in
let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in
@@ -909,8 +908,8 @@ let generalize_non_dep hyp g =
let to_revert,_ =
Environ.fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) ->
if List.mem hyp hyps
- or List.exists (occur_var_in_decl env hyp) keep
- or occur_var env hyp hyp_typ
+ or List.exists (Termops.occur_var_in_decl env hyp) keep
+ or Termops.occur_var env hyp hyp_typ
or Termops.is_section_variable hyp (* should be dangerous *)
then (clear,decl::keep)
else (hyp::clear,keep))
@@ -1300,7 +1299,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 [(all_occurrences,Names.EvalConstRef fname)];
+ [unfold_in_concl [(Termops.all_occurrences, Names.EvalConstRef fname)];
let do_prove =
build_proof
interactive_proof
@@ -1400,7 +1399,7 @@ let build_clause eqs =
{
Tacexpr.onhyps =
Some (List.map
- (fun id -> (Rawterm.all_occurrences_expr,id),InHyp)
+ (fun id -> (Rawterm.all_occurrences_expr, id), Termops.InHyp)
eqs
);
Tacexpr.concl_occs = Rawterm.no_occurrences_expr
@@ -1416,7 +1415,7 @@ let rec rewrite_eqs_in_eqs eqs =
(fun id gl ->
observe_tac
(Format.sprintf "rewrite %s in %s " (string_of_id eq) (string_of_id id))
- (tclTRY (Equality.general_rewrite_in true all_occurrences (* dep proofs also: *) true id (mkVar eq) false))
+ (tclTRY (Equality.general_rewrite_in true Termops.all_occurrences (* dep proofs also: *) true id (mkVar eq) false))
gl
)
eqs
@@ -1438,7 +1437,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
(fun g ->
if is_mes
then
- unfold_in_concl [(all_occurrences, evaluable_of_global_reference (delayed_force ltof_ref))] g
+ unfold_in_concl [(Termops.all_occurrences, evaluable_of_global_reference (delayed_force ltof_ref))] g
else tclIDTAC g
);
observe_tac "rew_and_finish"
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index e0b08599d..6034f19e6 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -1,7 +1,6 @@
open Printer
open Util
open Term
-open Termops
open Namegen
open Names
open Declarations
@@ -139,7 +138,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
in
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
+ let res = mkApp(rel_to_fun.(i), Array.map Termops.pop (array_get_start args)) in
(* observe (str "replacing " ++ pr_lconstr c ++ str " by " ++ pr_lconstr res); *)
res
in
@@ -198,58 +197,58 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
begin
try
let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in
- let new_x : name = get_name (ids_of_context env) x in
+ let new_x : name = get_name (Termops.ids_of_context env) x in
let new_env = Environ.push_rel (x,None,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
+ then (Termops.pop new_b), filter_map (eq_constr (mkRel 1)) Termops.pop binders_to_remove_from_b
else
(
bind_fun(new_x,new_t,new_b),
list_union_eq
eq_constr
binders_to_remove_from_t
- (List.map pop binders_to_remove_from_b)
+ (List.map Termops.pop binders_to_remove_from_b)
)
with
| Toberemoved ->
(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in
- new_b, List.map pop binders_to_remove_from_b
+ new_b, List.map Termops.pop binders_to_remove_from_b
| Toberemoved_with_rel (n,c) ->
(* observe (str "Decl of "++Ppconstr.pr_name 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 eq_constr (mkRel n) (List.map Termops.pop binders_to_remove_from_b)
end
and compute_new_princ_type_for_letin remove env x v t b =
begin
try
let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in
let new_v,binders_to_remove_from_v = compute_new_princ_type remove env v in
- let new_x : name = get_name (ids_of_context env) x in
+ let new_x : name = get_name (Termops.ids_of_context env) x in
let new_env = Environ.push_rel (x,Some 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
+ then (Termops.pop new_b),filter_map (eq_constr (mkRel 1)) Termops.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)
- (List.map pop binders_to_remove_from_b)
+ (List.map Termops.pop binders_to_remove_from_b)
)
with
| Toberemoved ->
(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in
- new_b, List.map pop binders_to_remove_from_b
+ new_b, List.map Termops.pop binders_to_remove_from_b
| Toberemoved_with_rel (n,c) ->
(* observe (str "Decl of "++Ppconstr.pr_name 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 eq_constr (mkRel n) (List.map Termops.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
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index f0ea133c6..24382f875 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -16,7 +16,6 @@ open Tacticals
open Tactics
open Indfun_common
open Tacmach
-open Termops
open Sign
open Hiddentac
@@ -686,7 +685,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
h_generalize (List.map mkVar ids);
thin ids
]
- else unfold_in_concl [(all_occurrences,Names.EvalConstRef (destConst f))]
+ else unfold_in_concl [(Termops.all_occurrences, Names.EvalConstRef (destConst f))]
in
(* The proof of each branche itself *)
let ind_number = ref 0 in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index e329196ac..c42ecac42 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -9,7 +9,6 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
open Term
-open Termops
open Namegen
open Environ
open Declarations
@@ -374,7 +373,7 @@ let rec mk_intros_and_continue thin_intros (extra_eqn:bool)
h_intros thin_intros;
tclMAP
- (fun eq -> tclTRY (Equality.general_rewrite_in true all_occurrences (* deps proofs also: *) true teq eq false))
+ (fun eq -> tclTRY (Equality.general_rewrite_in true Termops.all_occurrences (* deps proofs also: *) true teq eq false))
(List.rev eqs);
(fun g1 ->
let ty_teq = pf_type_of g1 (mkVar teq) in
@@ -382,7 +381,7 @@ let rec mk_intros_and_continue thin_intros (extra_eqn:bool)
let _,args = try destApp ty_teq with _ -> Pp.msgnl (Printer.pr_goal g1 ++ fnl () ++ pr_id teq ++ str ":" ++ Printer.pr_lconstr ty_teq); assert false in
args.(1),args.(2)
in
- cont_function (mkVar teq::eqs) (replace_term teq_lhs teq_rhs expr) g1
+ cont_function (mkVar teq::eqs) (Termops.replace_term teq_lhs teq_rhs expr) g1
)
]
@@ -435,7 +434,7 @@ let tclUSER tac is_mes l g =
clear_tac;
if is_mes
then tclTHEN
- (unfold_in_concl [(all_occurrences, evaluable_of_global_reference
+ (unfold_in_concl [(Termops.all_occurrences, evaluable_of_global_reference
(delayed_force ltof_ref))])
tac
else tac
@@ -534,7 +533,7 @@ let rec list_cond_rewrite k def pmax cond_eqs le_proofs =
Nameops.out_name k_na,Nameops.out_name def_na
in
tclTHENS
- (general_rewrite_bindings false all_occurrences
+ (general_rewrite_bindings false Termops.all_occurrences
(* dep proofs also: *) true
(mkVar eq,
ExplicitBindings[dummy_loc, NamedHyp k_id, mkVar k;
@@ -577,7 +576,7 @@ let rec introduce_all_equalities func eqs values specs bound le_proofs
observe_tac "refl equal" (apply (delayed_force refl_equal))] g
| spec1::specs ->
fun g ->
- let ids = ids_of_named_context (pf_hyps g) in
+ let ids = Termops.ids_of_named_context (pf_hyps g) in
let p = next_ident_away_in_goal p_id ids in
let ids = p::ids in
let pmax = next_ident_away_in_goal pmax_id ids in
@@ -623,7 +622,7 @@ let rec introduce_all_values concl_tac is_mes acc_inv func context_fn
(List.rev values) (List.rev specs) (delayed_force coq_O) [] [])]
| arg::args ->
(fun g ->
- let ids = ids_of_named_context (pf_hyps g) in
+ let ids = Termops.ids_of_named_context (pf_hyps g) in
let rec_res = next_ident_away_in_goal rec_res_id ids in
let ids = rec_res::ids in
let hspec = next_ident_away_in_goal hspec_id ids in
@@ -836,7 +835,7 @@ let rec instantiate_lambda t l =
let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_arg_num : tactic =
begin
fun g ->
- let ids = ids_of_named_context (pf_hyps g) in
+ let ids = Termops.ids_of_named_context (pf_hyps g) in
let func_body = (def_of_const (constr_of_global func)) in
let (f_name, _, body1) = destLambda func_body in
let f_id =
@@ -924,7 +923,7 @@ let clear_goals =
| Prod(Name id as na,t',b) ->
let b' = clear_goal b in
if noccurn 1 b' && (is_rec_res id)
- then pop b'
+ then Termops.pop b'
else if b' == b then t
else mkProd(na,t',b')
| _ -> map_constr clear_goal t
@@ -952,7 +951,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
let sign = Global.named_context () in
let sign = clear_proofs sign in
let na = next_global_ident_away name [] in
- if occur_existential gls_type then
+ if Termops.occur_existential gls_type then
Util.error "\"abstract\" cannot handle existentials";
let hook _ _ =
let opacity =
@@ -1158,7 +1157,7 @@ let start_equation (f:global_reference) (term_f:global_reference)
let x = n_x_id ids nargs in
tclTHENLIST [
h_intros x;
- unfold_in_concl [(all_occurrences, evaluable_of_global_reference f)];
+ unfold_in_concl [(Termops.all_occurrences, evaluable_of_global_reference f)];
observe_tac "simplest_case"
(simplest_case (mkApp (terminate_constr,
Array.of_list (List.map mkVar x))));
@@ -1200,7 +1199,7 @@ let rec introduce_all_values_eq cont_tac functional termine
simpl_iter (onHyp heq2);
unfold_in_hyp [((true,[1]), evaluable_of_global_reference
(global_of_constr functional))]
- (heq2, InHyp);
+ (heq2, Termops.InHyp);
tclTHENS
(fun gls ->
let t_eq = compute_renamed_type gls (mkVar heq2) in
@@ -1208,7 +1207,7 @@ let rec introduce_all_values_eq cont_tac functional termine
let _,_,t = destProd t_eq in let def_na,_,_ = destProd t in
Nameops.out_name def_na
in
- observe_tac "rewrite heq" (general_rewrite_bindings false all_occurrences
+ observe_tac "rewrite heq" (general_rewrite_bindings false Termops.all_occurrences
(* dep proofs also: *) true (mkVar heq2,
ExplicitBindings[dummy_loc,NamedHyp def_id,
f]) false) gls)
@@ -1264,7 +1263,7 @@ let rec introduce_all_values_eq cont_tac functional termine
f_S(mkVar pmax');
dummy_loc, NamedHyp def_id, f])
in
- observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false all_occurrences (* dep proofs also: *) true
+ observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false Termops.all_occurrences (* dep proofs also: *) true
c_b false))
g
)
@@ -1321,7 +1320,7 @@ let rec prove_eq nb_arg (termine:constr) (f:constr)(functional:global_reference
_,[] -> observe_tac "base_leaf_eq(1)" (base_leaf_eq functional eqs f)
| fn,args ->
fun g ->
- let ids = ids_of_named_context (pf_hyps g) in
+ let ids = Termops.ids_of_named_context (pf_hyps g) in
observe_tac "rec_leaf_eq" (rec_leaf_eq termine f ids
(constr_of_global functional)
eqs expr fn args) g))
@@ -1330,7 +1329,7 @@ let rec prove_eq nb_arg (termine:constr) (f:constr)(functional:global_reference
_,[] -> observe_tac "base_leaf_eq(2)" ( base_leaf_eq functional eqs f)
| fn,args ->
fun g ->
- let ids = ids_of_named_context (pf_hyps g) in
+ let ids = Termops.ids_of_named_context (pf_hyps g) in
observe_tac "rec_leaf_eq" (rec_leaf_eq
termine f ids (constr_of_global functional)
eqs expr fn args) g));;
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index c457115d3..c36cded17 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -20,7 +20,6 @@ open Proof_type
open Names
open Nameops
open Term
-open Termops
open Declarations
open Environ
open Sign
@@ -131,7 +130,7 @@ let exists_tac c = constructor_tac false (Some 1) 1 (Rawterm.ImplicitBindings [c
let generalize_tac t = generalize_time (generalize t)
let elim t = elim_time (simplest_elim t)
let exact t = exact_time (Tactics.refine t)
-let unfold s = Tactics.unfold_in_concl [all_occurrences, Lazy.force s]
+let unfold s = Tactics.unfold_in_concl [Termops.all_occurrences, Lazy.force s]
let rev_assoc k =
let rec loop = function
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 3e9cc781f..cd4a7d3b0 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -10,7 +10,6 @@ module Search = Explore.Make(Proof_search)
open Util
open Term
-open Termops
open Names
open Evd
open Tacmach
@@ -102,7 +101,7 @@ let rec make_form atom_env gls term =
let cciterm=special_whd gls term in
match kind_of_term cciterm with
Prod(_,a,b) ->
- if not (dependent (mkRel 1) b) &&
+ if not (Termops.dependent (mkRel 1) b) &&
Retyping.get_sort_family_of
(pf_env gls) (Tacmach.project gls) a = InProp
then
@@ -142,7 +141,7 @@ let rec make_hyps atom_env gls lenv = function
| (id,None,typ)::rest ->
let hrec=
make_hyps atom_env gls (typ::lenv) rest in
- if List.exists (dependent (mkVar id)) lenv ||
+ if List.exists (Termops.dependent (mkVar id)) lenv ||
(Retyping.get_sort_family_of
(pf_env gls) (Tacmach.project gls) typ <> InProp)
then
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 052406867..741d22a8a 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -17,7 +17,6 @@ open Environ
open Libnames
open Tactics
open Rawterm
-open Termops
open Tacticals
open Tacexpr
open Pcoq
@@ -102,7 +101,7 @@ let protect_tac map =
Tactics.reduct_option (protect_red map,DEFAULTcast) None ;;
let protect_tac_in map id =
- Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id,InHyp));;
+ Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Termops.InHyp));;
TACTIC EXTEND protect_fv
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 93f9b586b..31e630741 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -20,7 +20,6 @@ open Constrintern
open Subtac_command
open Typeclasses
open Typeclasses_errors
-open Termops
open Decl_kinds
open Entries
open Util
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 634a6ea60..397bda9b0 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -21,7 +21,6 @@ open Tacmach
open Tactic_debug
open Topconstr
open Term
-open Termops
open Tacexpr
open Safe_typing
open Typing
@@ -133,7 +132,7 @@ let collect_non_rec env =
let i =
list_try_find_i
(fun i f ->
- if List.for_all (fun (_, def) -> not (occur_var env f def)) ldefrec
+ if List.for_all (fun (_, def) -> not (Termops.occur_var env f def)) ldefrec
then i else failwith "try_find_i")
0 lnamerec
in
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 6154b19ad..311889448 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -13,7 +13,6 @@ open Names
open Sign
open Evd
open Term
-open Termops
open Reductionops
open Environ
open Type_errors
@@ -106,7 +105,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
else id
let invert_ltac_bound_name env id0 id =
- try mkRel (pi1 (lookup_rel_id id (rel_context env)))
+ try mkRel (pi1 (Termops.lookup_rel_id id (rel_context env)))
with Not_found ->
errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++
str " depends on pattern variable name " ++ pr_id id ++
@@ -115,7 +114,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let pretype_id loc env sigma (lvar,unbndltacvars) id =
let id = strip_meta id in (* May happen in tactics defined by Grammar *)
try
- let (n,_,typ) = lookup_rel_id id (rel_context env) in
+ let (n,_,typ) = Termops.lookup_rel_id id (rel_context env) in
{ uj_val = mkRel n; uj_type = lift n typ }
with Not_found ->
try
@@ -151,7 +150,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let s' = mkProd (Anonymous, ind, s) in
let ccl = lift 1 (decomp n pj.uj_val) in
let ccl' = mkLambda (Anonymous, ind, ccl) in
- {uj_val=it_mkLambda ccl' sign; uj_type=it_mkProd s' sign}
+ {uj_val=Termops.it_mkLambda ccl' sign; uj_type=Termops.it_mkProd s' sign}
(*************************************************************************)
(* Main pretyping function *)
@@ -224,7 +223,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
match tycon with
| Some (None, ty) -> ty
| None | Some _ ->
- e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ()) in
+ e_new_evar evdref env ~src:(loc, InternalHole) (Termops.new_Type ()) in
{ uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
| RRec (loc,fixkind,names,bl,lar,vdef) ->
@@ -386,7 +385,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| RProd(loc,name,k,c1,c2) ->
let j = pretype_type empty_valcon env evdref lvar c1 in
let var = (name,j.utj_val) in
- let env' = push_rel_assum var env in
+ let env' = Termops.push_rel_assum var env in
let j' = pretype_type empty_valcon env' evdref lvar c2 in
let resj =
try judge_of_product env name j j'
@@ -395,7 +394,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| RLetIn(loc,name,c1,c2) ->
let j = pretype empty_tycon env evdref lvar c1 in
- let t = refresh_universes j.uj_type in
+ let t = Termops.refresh_universes j.uj_type in
let var = (name,Some j.uj_val,t) in
let tycon = lift_tycon 1 tycon in
let j' = pretype tycon (push_rel var env) evdref lvar c2 in
@@ -503,7 +502,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let p = match tycon with
| Some (None, ty) -> ty
| None | Some _ ->
- e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ())
+ e_new_evar evdref env ~src:(loc,InternalHole) (Termops.new_Type ())
in
it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
let pred = nf_evar ( !evdref) pred in
@@ -584,7 +583,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
{ utj_val = v;
utj_type = s }
| None ->
- let s = new_Type_sort () in
+ let s = Termops.new_Type_sort () in
{ utj_val = e_new_evar evdref env ~src:loc (mkSort s);
utj_type = s})
| c ->
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index 689b110f8..106ac4d09 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -414,7 +414,6 @@ let string_of_intset d =
open Printer
open Ppconstr
open Nameops
-open Termops
open Evd
let pr_meta_map evd =
@@ -426,11 +425,11 @@ let pr_meta_map evd =
| (mv,Cltyp (na,b)) ->
hov 0
(pr_meta mv ++ pr_name na ++ str " : " ++
- print_constr b.rebus ++ fnl ())
+ Termops.print_constr b.rebus ++ fnl ())
| (mv,Clval(na,b,_)) ->
hov 0
(pr_meta mv ++ pr_name na ++ str " := " ++
- print_constr (fst b).rebus ++ fnl ())
+ Termops.print_constr (fst b).rebus ++ fnl ())
in
prlist pr_meta_binding ml
@@ -441,11 +440,11 @@ let pr_evar_info evi =
(*pr_idl (List.rev (ids_of_named_context (evar_context evi))) *)
Printer.pr_named_context (Global.env()) (evar_context evi)
in
- let pty = print_constr evi.evar_concl in
+ let pty = Termops.print_constr evi.evar_concl in
let pb =
match evi.evar_body with
| Evar_empty -> mt ()
- | Evar_defined c -> spc() ++ str"=> " ++ print_constr c
+ | Evar_defined c -> spc() ++ str"=> " ++ Termops.print_constr c
in
hov 2 (str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]")
@@ -459,11 +458,11 @@ let pr_evar_map sigma =
let pr_constraints pbs =
h 0
(prlist_with_sep pr_fnl (fun (pbty,t1,t2) ->
- print_constr t1 ++ spc() ++
+ Termops.print_constr t1 ++ spc() ++
str (match pbty with
| Reduction.CONV -> "=="
| Reduction.CUMUL -> "<=") ++
- spc() ++ print_constr t2) pbs)
+ spc() ++ Termops.print_constr t2) pbs)
let pr_evar_map evd =
let pp_evm =
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 941b6f7df..acded3ac5 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -16,7 +16,6 @@ open Names
open Libnames
open Nameops
open Term
-open Termops
open Namegen
open Declarations
open Entries
@@ -55,7 +54,7 @@ let mis_make_case_com dep env sigma ind (mib,mip as specif) kind =
if not (List.mem kind (elim_sorts specif)) then
raise
(RecursionSchemeError
- (NotAllowedCaseAnalysis (false,new_sort_in_family kind,ind)));
+ (NotAllowedCaseAnalysis (false, Termops.new_sort_in_family kind, ind)));
let ndepar = mip.mind_nrealargs_ctxt + 1 in
@@ -63,7 +62,7 @@ let mis_make_case_com dep env sigma ind (mib,mip as specif) kind =
(* mais pas très joli ... (mais manque get_sort_of à ce niveau) *)
let env' = push_rel_context lnamespar env in
- let indf = make_ind_family(ind, extended_rel_list 0 lnamespar) in
+ let indf = make_ind_family(ind, Termops.extended_rel_list 0 lnamespar) in
let constrs = get_constructors env indf in
let rec add_branch env k =
@@ -79,8 +78,8 @@ let mis_make_case_com dep env sigma ind (mib,mip as specif) kind =
let pbody =
appvect
(mkRel (ndepar + nbprod),
- if dep then extended_rel_vect 0 deparsign
- else extended_rel_vect 1 arsign) in
+ if dep then Termops.extended_rel_vect 0 deparsign
+ else Termops.extended_rel_vect 1 arsign) in
let p =
it_mkLambda_or_LetIn_name env'
((if dep then mkLambda_name env' else mkLambda)
@@ -90,7 +89,7 @@ let mis_make_case_com dep env sigma ind (mib,mip as specif) kind =
it_mkLambda_or_LetIn_name env'
(mkCase (ci, lift ndepar p,
mkRel 1,
- rel_vect ndepar k))
+ Termops.rel_vect ndepar k))
deparsign
else
let cs = lift_constructor (k+1) constrs.(k) in
@@ -98,7 +97,7 @@ let mis_make_case_com dep env sigma ind (mib,mip as specif) kind =
mkLambda_string "f" t
(add_branch (push_rel (Anonymous, None, t) env) (k+1))
in
- let typP = make_arity env' dep indf (new_sort_in_family kind) in
+ let typP = make_arity env' dep indf (Termops.new_sort_in_family kind) in
it_mkLambda_or_LetIn_name env
(mkLambda_string "P" typP
(add_branch (push_rel (Anonymous,None,typP) env') 0)) lnamespar
@@ -138,7 +137,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
let base = applist (lift i pk,realargs) in
if depK then
Reduction.beta_appvect
- base [|applist (mkRel (i+1),extended_rel_list 0 sign)|]
+ base [|applist (mkRel (i+1), Termops.extended_rel_list 0 sign)|]
else
base
| _ -> assert false
@@ -210,7 +209,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c)
| Ind _ ->
let realargs = list_skipn nparrec largs
- and arg = appvect (mkRel (i+1),extended_rel_vect 0 hyps) in
+ and arg = appvect (mkRel (i+1), Termops.extended_rel_vect 0 hyps) in
applist(lift i fk,realargs@[arg])
| _ -> assert false
in
@@ -296,7 +295,7 @@ let mis_make_indrec env sigma listdepkind mib =
(* arity in the context of the fixpoint, i.e.
P1..P_nrec f1..f_nbconstruct *)
- let args = extended_rel_list (nrec+nbconstruct) lnamesparrec in
+ let args = Termops.extended_rel_list (nrec+nbconstruct) lnamesparrec in
let indf = make_ind_family(indi,args) in
let arsign,_ = get_arity env indf in
@@ -310,15 +309,15 @@ let mis_make_indrec env sigma listdepkind mib =
(* constructors in context of the Cases expr, i.e.
P1..P_nrec f1..f_nbconstruct F_1..F_nrec a_1..a_nar x:I *)
- let args' = extended_rel_list (dect+nrec) lnamesparrec in
- let args'' = extended_rel_list ndepar lnonparrec in
+ let args' = Termops.extended_rel_list (dect+nrec) lnamesparrec in
+ let args'' = Termops.extended_rel_list ndepar lnonparrec in
let indf' = make_ind_family(indi,args'@args'') in
let branches =
let constrs = get_constructors env indf' in
- let fi = rel_vect (dect-i-nctyi) nctyi in
+ let fi = Termops.rel_vect (dect-i-nctyi) nctyi in
let vecfi = Array.map
- (fun f -> appvect (f,extended_rel_vect ndepar lnonparrec))
+ (fun f -> appvect (f, Termops.extended_rel_vect ndepar lnonparrec))
fi
in
array_map3
@@ -339,9 +338,9 @@ let mis_make_indrec env sigma listdepkind mib =
let deparsign' = (Anonymous,None,depind')::arsign' in
let pargs =
- let nrpar = extended_rel_list (2*ndepar) lnonparrec
- and nrar = if dep then extended_rel_list 0 deparsign'
- else extended_rel_list 1 arsign'
+ let nrpar = Termops.extended_rel_list (2*ndepar) lnonparrec
+ and nrar = if dep then Termops.extended_rel_list 0 deparsign'
+ else Termops.extended_rel_list 1 arsign'
in nrpar@nrar
in
@@ -360,15 +359,15 @@ let mis_make_indrec env sigma listdepkind mib =
(mkCase (ci, pred,
mkRel 1,
branches))
- (lift_rel_context nrec deparsign)
+ (Termops.lift_rel_context nrec deparsign)
in
(* type of i-th component of the mutual fixpoint *)
let typtyi =
let concl =
- let pargs = if dep then extended_rel_vect 0 deparsign
- else extended_rel_vect 1 arsign
+ let pargs = if dep then Termops.extended_rel_vect 0 deparsign
+ else Termops.extended_rel_vect 1 arsign
in appvect (mkRel (nbconstruct+ndepar+nonrecpar+j),pargs)
in it_mkProd_or_LetIn_name env
concl
@@ -395,7 +394,7 @@ let mis_make_indrec env sigma listdepkind mib =
else
let recarg = (dest_subterms recargsvec.(tyi)).(j) in
let recarg = recargpar@recarg in
- let vargs = extended_rel_list (nrec+i+j) lnamesparrec in
+ let vargs = Termops.extended_rel_list (nrec+i+j) lnamesparrec in
let cs = get_constructor (indi,mibi,mipi,vargs) (j+1) in
let p_0 =
type_rec_branch
@@ -409,8 +408,8 @@ let mis_make_indrec env sigma listdepkind mib =
in
let rec put_arity env i = function
| (indi,_,_,dep,kinds)::rest ->
- let indf = make_ind_family (indi,extended_rel_list i lnamesparrec) in
- let typP = make_arity env dep indf (new_sort_in_family kinds) in
+ let indf = make_ind_family (indi, Termops.extended_rel_list i lnamesparrec) in
+ let typP = make_arity env dep indf (Termops.new_sort_in_family kinds) in
mkLambda_string "P" typP
(put_arity (push_rel (Anonymous,None,typP) env) (i+1) rest)
| [] ->
@@ -504,7 +503,7 @@ let check_arities listdepkind =
let kelim = elim_sorts (mibi,mipi) in
if not (List.exists ((=) kind) kelim) then raise
(RecursionSchemeError
- (NotAllowedCaseAnalysis (true,new_sort_in_family kind,mind)))
+ (NotAllowedCaseAnalysis (true, Termops.new_sort_in_family kind,mind)))
else if List.mem ni ln then raise
(RecursionSchemeError (NotMutualInScheme (mind,mind)))
else ni::ln)
@@ -569,5 +568,5 @@ let lookup_eliminator ind_sp s =
(strbrk "Cannot find the elimination combinator " ++
pr_id id ++ strbrk ", the elimination of the inductive definition " ++
pr_global_env Idset.empty (IndRef ind_sp) ++
- strbrk " on sort " ++ pr_sort_family s ++
+ strbrk " on sort " ++ Termops.pr_sort_family s ++
strbrk " is probably not allowed.")
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index d477ec34a..ccedf1520 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -19,7 +19,6 @@ open Names
open Libnames
open Nametab
open Term
-open Termops
open Typeops
open Libobject
open Library
@@ -206,7 +205,7 @@ let cs_pattern_of_constr t =
_ -> raise Not_found
end
| Rel n -> Default_cs, pred n, []
- | Prod (_,a,b) when not (dependent (mkRel 1) b) -> Prod_cs, -1, [a;pop b]
+ | Prod (_,a,b) when not (Termops.dependent (mkRel 1) b) -> Prod_cs, -1, [a; Termops.pop b]
| Sort s -> Sort_cs (family_of_sort s), -1, []
| _ ->
begin
@@ -240,7 +239,7 @@ let compute_canonical_projections (con,ind) =
(let con_pp = Nametab.pr_global_env Idset.empty (ConstRef con)
and proji_sp_pp = Nametab.pr_global_env Idset.empty (ConstRef proji_sp) in
msg_warning (str "No global reference exists for projection value"
- ++ print_constr t ++ str " in instance "
+ ++ Termops.print_constr t ++ str " in instance "
++ con_pp ++ str " of " ++ proji_sp_pp ++ str ", ignoring it."));
l
end
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 49ff459c6..8955b6c7e 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -18,7 +18,6 @@ open Tacexpr
open Rawterm
open Tactics
open Util
-open Termops
open Evd
open Equality
open Compat
@@ -228,11 +227,11 @@ TACTIC EXTEND rewrite_star
| [ "rewrite" "*" orient(o) open_constr(c) "at" occurrences(occ) "in" hyp(id) by_arg_tac(tac) ] ->
[ rewrite_star (Some id) o (occurrences_of occ) c tac ]
| [ "rewrite" "*" orient(o) open_constr(c) "in" hyp(id) by_arg_tac(tac) ] ->
- [ rewrite_star (Some id) o all_occurrences c tac ]
+ [ rewrite_star (Some id) o Termops.all_occurrences c tac ]
| [ "rewrite" "*" orient(o) open_constr(c) "at" occurrences(occ) by_arg_tac(tac) ] ->
[ rewrite_star None o (occurrences_of occ) c tac ]
| [ "rewrite" "*" orient(o) open_constr(c) by_arg_tac(tac) ] ->
- [ rewrite_star None o all_occurrences c tac ]
+ [ rewrite_star None o Termops.all_occurrences c tac ]
END
(**********************************************************************)
@@ -538,7 +537,7 @@ END
(**********************************************************************)
let subst_var_with_hole occ tid t =
- let occref = if occ > 0 then ref occ else error_invalid_occurrence [occ] in
+ let occref = if occ > 0 then ref occ else Termops.error_invalid_occurrence [occ] in
let locref = ref 0 in
let rec substrec = function
| RVar (_,id) as x ->
@@ -549,7 +548,7 @@ let subst_var_with_hole occ tid t =
| c -> map_rawconstr_left_to_right substrec c in
let t' = substrec t
in
- if !occref > 0 then error_invalid_occurrence [occ] else t'
+ if !occref > 0 then Termops.error_invalid_occurrence [occ] else t'
let subst_hole_with_term occ tc t =
let locref = ref 0 in
@@ -570,9 +569,9 @@ let out_arg = function
let hResolve id c occ t gl =
let sigma = project gl in
- let env = clear_named_body id (pf_env gl) in
- let env_ids = ids_of_context env in
- let env_names = names_of_rel_context env in
+ let env = Termops.clear_named_body id (pf_env gl) in
+ let env_ids = Termops.ids_of_context env in
+ let env_names = Termops.names_of_rel_context env in
let c_raw = Detyping.detype true env_ids env_names c in
let t_raw = Detyping.detype true env_ids env_names t in
let rec resolve_hole t_hole =
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 821fc0fad..09b983622 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -10,7 +10,6 @@
open Names
open Decl_kinds
open Term
-open Termops
open Sign
open Entries
open Evd
diff --git a/toplevel/record.ml b/toplevel/record.ml
index b87d11d54..b751db85b 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -12,7 +12,6 @@ open Names
open Libnames
open Nameops
open Term
-open Termops
open Environ
open Declarations
open Entries
@@ -59,7 +58,7 @@ let typecheck_params_and_fields id t ps nots fs =
let env0 = Global.env () in
let evars = ref Evd.empty in
let (env1,newps), imps = interp_context_evars evars env0 ps in
- let fullarity = it_mkProd_or_LetIn (Option.cata (fun x -> x) (new_Type ()) t) newps in
+ let fullarity = it_mkProd_or_LetIn (Option.cata (fun x -> x) (Termops.new_Type ()) t) newps in
let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in
let env2,impls,newfs,data =
interp_fields_evars evars env_ar nots (binders_of_decls fs)
@@ -148,7 +147,7 @@ let subst_projection fid l c =
let instantiate_possibly_recursive_type indsp paramdecls fields =
let subst = list_map_i (fun i _ -> mkRel i) 1 paramdecls in
- substl_rel_context (subst@[mkInd indsp]) fields
+ Termops.substl_rel_context (subst@[mkInd indsp]) fields
(* We build projections *)
let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls fields =
@@ -156,11 +155,11 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
let (mib,mip) = Global.lookup_inductive indsp in
let paramdecls = mib.mind_params_ctxt in
let r = mkInd indsp in
- let rp = applist (r, extended_rel_list 0 paramdecls) in
- let paramargs = extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*)
+ let rp = applist (r, Termops.extended_rel_list 0 paramdecls) in
+ let paramargs = Termops.extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*)
let x = match name with Some n -> Name n | None -> Namegen.named_hd (Global.env()) r Anonymous in
let fields = instantiate_possibly_recursive_type indsp paramdecls fields in
- let lifted_fields = lift_rel_context 1 fields in
+ let lifted_fields = Termops.lift_rel_context 1 fields in
let (_,kinds,sp_projs,_) =
list_fold_left3
(fun (nfi,kinds,sp_projs,subst) coe (fi,optci,ti) impls ->
@@ -234,7 +233,7 @@ open Typeclasses
let declare_structure finite infer id idbuild paramimpls params arity fieldimpls fields
?(kind=StructureComponent) ?name is_coe coers sign =
let nparams = List.length params and nfields = List.length fields in
- let args = extended_rel_list nfields params in
+ let args = Termops.extended_rel_list nfields params in
let ind = applist (mkRel (1+nparams+nfields), args) in
let type_constructor = it_mkProd_or_LetIn ind fields in
let mie_ind =
@@ -248,7 +247,7 @@ let declare_structure finite infer id idbuild paramimpls params arity fieldimpls
(* there is probably a way to push this to "declare_mutual" *)
begin match finite with
| BiFinite ->
- if dependent (mkRel (nparams+1)) (it_mkProd_or_LetIn mkProp fields) then
+ if Termops.dependent (mkRel (nparams+1)) (it_mkProd_or_LetIn mkProp fields) then
error "Records declared with the keyword Record or Structure cannot be recursive. Maybe you meant to define an Inductive or CoInductive record."
| _ -> ()
end;
@@ -306,7 +305,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
let cst = Declare.declare_constant (snd id)
(DefinitionEntry class_entry, IsDefinition Definition)
in
- let inst_type = appvectc (mkConst cst) (rel_vect 0 (List.length params)) in
+ let inst_type = appvectc (mkConst cst) (Termops.rel_vect 0 (List.length params)) in
let proj_type = it_mkProd_or_LetIn (mkProd(Name (snd id), inst_type, lift 1 field)) params in
let proj_body = it_mkLambda_or_LetIn (mkLambda (Name (snd id), inst_type, mkRel 1)) params in
let proj_entry =
@@ -325,9 +324,9 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
if infer then Evd.fold (fun ev evi _ -> Recordops.declare_method (ConstRef cst) ev sign) sign ();
cref, [proj_name, Some proj_cst]
| _ ->
- let idarg = Namegen.next_ident_away (snd id) (ids_of_context (Global.env())) in
+ let idarg = Namegen.next_ident_away (snd id) (Termops.ids_of_context (Global.env())) in
let ind = declare_structure BiFinite infer (snd id) idbuild paramimpls
- params (Option.cata (fun x -> x) (new_Type ()) arity) fieldimpls fields
+ params (Option.cata (fun x -> x) (Termops.new_Type ()) arity) fieldimpls fields
~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) sign
in
IndRef ind, (List.map2 (fun (id, _, _) y -> (Nameops.out_name id, y))
@@ -385,7 +384,7 @@ let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuil
if infer then search_record declare_class_instance gr sign;
gr
| _ ->
- let arity = Option.default (new_Type ()) sc in
+ let arity = Option.default (Termops.new_Type ()) sc in
let implfs = List.map
(fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in
let ind = declare_structure finite infer idstruc idbuild implpars params arity implfs fields is_coe coers sign in
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index f597773fa..906629997 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -18,7 +18,6 @@ open Environ
open Rawterm
open Libnames
open Nametab
-open Termops
open Detyping
open Constrintern
open Dischargedhypsmap
@@ -196,7 +195,7 @@ let whelp_elim ind =
let on_goal f =
let { Evd.it=goals ; sigma=sigma } = Proof.V82.subgoals (get_pftreestate ()) in
let gls = { Evd.it=List.hd goals ; sigma = sigma } in
- f (it_mkNamedProd_or_LetIn (pf_concl gls) (pf_hyps gls))
+ f (Termops.it_mkNamedProd_or_LetIn (pf_concl gls) (pf_hyps gls))
type whelp_request =
| Locate of string
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 06:14:06 +0000