aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/correctness/ptactic.ml3
-rw-r--r--contrib/fourier/fourierR.ml2
-rw-r--r--contrib/interface/name_to_ast.ml4
-rw-r--r--contrib/subtac/subtac_cases.ml6
-rw-r--r--contrib/subtac/subtac_pretyping_F.ml4
-rw-r--r--contrib/xml/cic2acic.ml7
-rw-r--r--contrib/xml/doubleTypeInference.ml2
-rw-r--r--contrib/xml/xmlcommand.ml9
8 files changed, 15 insertions, 22 deletions
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index e7610923c..b99a3621d 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -138,7 +138,7 @@ let (loop_ids : tactic) = fun gl ->
then
tclTHEN (clear [id]) (arec al) gl
else if n >= 7 & String.sub s 0 7 = "Variant" then begin
- match pf_matches gl eq_pattern (body_of_type a) with
+ match pf_matches gl eq_pattern a with
| [_; _,varphi; _] when isVar varphi ->
let phi = destVar varphi in
if Termops.occur_var env phi concl then
@@ -159,7 +159,6 @@ let (assumption_bis : tactic) = fun gl ->
let rec arec = function
| [] -> Util.error "No such assumption"
| (s,a) :: al ->
- let a = body_of_type a in
if pf_conv_x_leq gl a concl then
refine (mkVar s) gl
else if pf_is_matching gl and_pattern a then
diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml
index 16705262d..d97e64970 100644
--- a/contrib/fourier/fourierR.ml
+++ b/contrib/fourier/fourierR.ml
@@ -492,7 +492,7 @@ let rec fourier gl=
in tac gl)
with _ ->
(* les hypothèses *)
- let hyps = List.map (fun (h,t)-> (mkVar h,(body_of_type t)))
+ let hyps = List.map (fun (h,t)-> (mkVar h,t))
(list_of_sign (pf_hyps gl)) in
let lineq =ref [] in
List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index bbde91aac..b0a34cfd1 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -135,13 +135,13 @@ let implicits_to_ast_list implicits =
let make_variable_ast name typ implicits =
(VernacAssumption
((Local,Definitional),false,(*inline flag*)
- [false,([dummy_loc,name], constr_to_ast (body_of_type typ))]))
+ [false,([dummy_loc,name], constr_to_ast typ)]))
::(implicits_to_ast_list implicits);;
let make_definition_ast name c typ implicits =
VernacDefinition ((Global,false,Definition), (dummy_loc,name), DefineBody ([], None,
- (constr_to_ast c), Some (constr_to_ast (body_of_type typ))),
+ (constr_to_ast c), Some (constr_to_ast typ)),
(fun _ _ -> ()))
::(implicits_to_ast_list implicits);;
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 27efe0470..c1889b689 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1772,8 +1772,7 @@ let subst_rel_context k ctx subst =
let lift_rel_contextn n k sign =
let rec liftrec k = function
| (na,c,t)::sign ->
- (na,option_map (liftn n k) c,type_app (liftn n k) t)
- ::(liftrec (k-1) sign)
+ (na,option_map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
| [] -> []
in
liftrec (rel_context_length sign + k) sign
@@ -2066,8 +2065,7 @@ let build_dependent_signature env evars avoid tomatchs arsign =
let liftn_rel_context n k sign =
let rec liftrec k = function
| (na,c,t)::sign ->
- (na,option_map (liftn n k) c,type_app (liftn n k) t)
- ::(liftrec (k-1) sign)
+ (na,option_map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
| [] -> []
in
liftrec (k + rel_context_length sign) sign
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index c2132f61b..ab542feb2 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -67,8 +67,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let mt_evd = Evd.empty
- let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)
-
(* Utilisé pour inférer le prédicat des Cases *)
(* Semble exagérement fort *)
(* Faudra préférer une unification entre les types de toutes les clauses *)
@@ -113,7 +111,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
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
- { uj_val = mkRel n; uj_type = type_app (lift n) typ }
+ { uj_val = mkRel n; uj_type = lift n typ }
with Not_found ->
try
List.assoc id lvar
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index 8a5967a23..75e428e14 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -241,16 +241,15 @@ let typeur sigma metamap =
| T.Var id ->
(try
let (_,_,ty) = Environ.lookup_named id env in
- T.body_of_type ty
+ ty
with Not_found ->
Util.anomaly ("type_of: variable "^(Names.string_of_id id)^" unbound"))
| T.Const c ->
let cb = Environ.lookup_constant c env in
Typeops.type_of_constant_type env (cb.Declarations.const_type)
| T.Evar ev -> Evd.existential_type sigma ev
- | T.Ind ind -> T.body_of_type (Inductiveops.type_of_inductive env ind)
- | T.Construct cstr ->
- T.body_of_type (Inductiveops.type_of_constructor env cstr)
+ | T.Ind ind -> Inductiveops.type_of_inductive env ind
+ | T.Construct cstr -> Inductiveops.type_of_constructor env cstr
| T.Case (_,p,c,lf) ->
let Inductiveops.IndType(_,realargs) =
try Inductiveops.find_rectype env sigma (type_of env c)
diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml
index cce788912..de8c540ca 100644
--- a/contrib/xml/doubleTypeInference.ml
+++ b/contrib/xml/doubleTypeInference.ml
@@ -51,7 +51,7 @@ let type_judgment env sigma j =
;;
let type_judgment_cprop env sigma j =
- match Term.kind_of_term(whd_betadeltaiotacprop env sigma (Term.body_of_type j.Environ.uj_type)) with
+ match Term.kind_of_term(whd_betadeltaiotacprop env sigma j.Environ.uj_type) with
| Term.Sort s -> Some {Environ.utj_val = j.Environ.uj_val; Environ.utj_type = s }
| _ -> None (* None means the CProp constant *)
;;
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 012713239..1aabd4348 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -329,14 +329,13 @@ let mk_variable_obj id body typ =
let variables = search_variables () in
let params = filter_params variables hyps'' in
Acic.Variable
- (Names.string_of_id id, unsharedbody,
- (Unshare.unshare (Term.body_of_type typ)), params)
+ (Names.string_of_id id, unsharedbody, Unshare.unshare typ, params)
;;
(* Unsharing is not performed on the body, that must be already unshared. *)
(* The evar map and the type, instead, are unshared by this function. *)
let mk_current_proof_obj is_a_variable id bo ty evar_map env =
- let unshared_ty = Unshare.unshare (Term.body_of_type ty) in
+ let unshared_ty = Unshare.unshare ty in
let metasenv =
List.map
(function
@@ -384,7 +383,7 @@ let mk_current_proof_obj is_a_variable id bo ty evar_map env =
let mk_constant_obj id bo ty variables hyps =
let hyps = string_list_of_named_context_list hyps in
- let ty = Unshare.unshare (Term.body_of_type ty) in
+ let ty = Unshare.unshare ty in
let params = filter_params variables hyps in
match bo with
None ->
@@ -413,7 +412,7 @@ let mk_inductive_obj sp mib packs variables nparams hyps finite =
let cons =
(Array.fold_right (fun (name,lc) i -> (name,lc)::i)
(Array.mapi
- (fun j x ->(x,Unshare.unshare (Term.body_of_type lc.(j)))) consnames)
+ (fun j x ->(x,Unshare.unshare lc.(j))) consnames)
[]
)
in
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-30 13:40:36 +0000