aboutsummaryrefslogtreecommitdiff
path: root/plugins/subtac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/subtac')
-rw-r--r--plugins/subtac/subtac.ml2
-rw-r--r--plugins/subtac/subtac_cases.ml24
-rw-r--r--plugins/subtac/subtac_command.ml10
-rw-r--r--plugins/subtac/subtac_pretyping.ml6
-rw-r--r--plugins/subtac/subtac_pretyping.mli2
-rw-r--r--plugins/subtac/subtac_pretyping_F.ml48
-rw-r--r--plugins/subtac/subtac_utils.ml2
-rw-r--r--plugins/subtac/subtac_utils.mli2
8 files changed, 48 insertions, 48 deletions
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 62fa0b2c9f..0ea2290db8 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -88,7 +88,7 @@ let start_proof_and_print env isevars idopt k t hook =
start_proof_com env isevars idopt k t hook;
print_subgoals ()
-let _ = Detyping.set_detype_anonymous (fun loc n -> RVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n)))
+let _ = Detyping.set_detype_anonymous (fun loc n -> GVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n)))
let assumption_message id =
Flags.if_verbose message ((string_of_id id) ^ " is assumed")
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index b6a42b6b46..5ef6f0f881 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -86,7 +86,7 @@ let mkSpecialLetInJudge j (na,(deppat,nondeppat,d,t)) =
type rhs =
{ rhs_env : env;
avoid_ids : identifier list;
- it : rawconstr;
+ it : glob_constr;
}
type equation =
@@ -234,7 +234,7 @@ type pattern_matching_problem =
mat : matrix;
caseloc : loc;
casestyle: case_style;
- typing_function: type_constraint -> env -> rawconstr -> unsafe_judgment }
+ typing_function: type_constraint -> env -> glob_constr -> unsafe_judgment }
(*--------------------------------------------------------------------------*
* A few functions to infer the inductive type from the patterns instead of *
@@ -366,10 +366,10 @@ let find_tomatch_tycon isevars env loc = function
| None -> empty_tycon
let coerce_row typing_fun isevars env pats (tomatch,(_,indopt)) =
- let loc = Some (loc_of_rawconstr tomatch) in
+ let loc = Some (loc_of_glob_constr tomatch) in
let tycon = find_tomatch_tycon isevars env loc indopt in
let j = typing_fun tycon env tomatch in
- let evd, j = Coercion.inh_coerce_to_base (loc_of_rawconstr tomatch) env !isevars j in
+ let evd, j = Coercion.inh_coerce_to_base (loc_of_glob_constr tomatch) env !isevars j in
isevars := evd;
let typ = nf_evar ( !isevars) j.uj_type in
let t =
@@ -527,7 +527,7 @@ let extract_rhs pb =
let occur_in_rhs na rhs =
match na with
| Anonymous -> false
- | Name id -> occur_rawconstr id rhs.it
+ | Name id -> occur_glob_constr id rhs.it
let is_dep_patt eqn = function
| PatVar (_,name) -> occur_in_rhs name eqn.rhs
@@ -1515,7 +1515,7 @@ let mk_JMeq typ x typ' y =
mkApp (delayed_force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |])
let mk_JMeq_refl typ x = mkApp (delayed_force Subtac_utils.jmeq_refl, [| typ; x |])
-let hole = RHole (dummy_loc, Evd.QuestionMark (Evd.Define true))
+let hole = GHole (dummy_loc, Evd.QuestionMark (Evd.Define true))
let constr_of_pat env isevars arsign pat avoid =
let rec typ env (ty, realargs) pat avoid =
@@ -1604,12 +1604,12 @@ let vars_of_ctx ctx =
match b with
| Some t' when kind_of_term t' = Rel 0 ->
prev,
- (RApp (dummy_loc,
- (RRef (dummy_loc, delayed_force refl_ref)), [hole; RVar (dummy_loc, prev)])) :: vars
+ (GApp (dummy_loc,
+ (GRef (dummy_loc, delayed_force refl_ref)), [hole; GVar (dummy_loc, prev)])) :: vars
| _ ->
match na with
Anonymous -> raise (Invalid_argument "vars_of_ctx")
- | Name n -> n, RVar (dummy_loc, n) :: vars)
+ | Name n -> n, GVar (dummy_loc, n) :: vars)
ctx (id_of_string "vars_of_ctx_error", [])
in List.rev y
@@ -1741,13 +1741,13 @@ let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity =
let branch_name = id_of_string ("branch_" ^ (string_of_int !i)) in
let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in
let branch =
- let bref = RVar (dummy_loc, branch_name) in
+ let bref = GVar (dummy_loc, branch_name) in
match vars_of_ctx rhs_rels with
[] -> bref
- | l -> RApp (dummy_loc, bref, l)
+ | l -> GApp (dummy_loc, bref, l)
in
let branch = match ineqs with
- Some _ -> RApp (dummy_loc, branch, [ hole ])
+ Some _ -> GApp (dummy_loc, branch, [ hole ])
| None -> branch
in
incr i;
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 8527766305..24fdd679b3 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -84,16 +84,16 @@ let interp_constr_judgment isevars env c =
{ uj_val = evar_nf isevars j.uj_val; uj_type = evar_nf isevars j.uj_type }
let locate_if_isevar loc na = function
- | RHole _ ->
+ | GHole _ ->
(try match na with
- | Name id -> rawconstr_of_aconstr loc (Reserve.find_reserved_type id)
+ | Name id -> glob_constr_of_aconstr loc (Reserve.find_reserved_type id)
| Anonymous -> raise Not_found
- with Not_found -> RHole (loc, Evd.BinderType na))
+ with Not_found -> GHole (loc, Evd.BinderType na))
| x -> x
let interp_binder sigma env na t =
let t = Constrintern.intern_gen true ( !sigma) env t in
- SPretyping.understand_tcc_evars sigma env IsType (locate_if_isevar (loc_of_rawconstr t) na t)
+ SPretyping.understand_tcc_evars sigma env IsType (locate_if_isevar (loc_of_glob_constr t) na t)
let interp_context_evars evdref env params =
let bl = Constrintern.intern_context false !evdref env params in
@@ -102,7 +102,7 @@ let interp_context_evars evdref env params =
(fun (env,params,n,impls) (na, k, b, t) ->
match b with
None ->
- let t' = locate_if_isevar (loc_of_rawconstr t) na t in
+ let t' = locate_if_isevar (loc_of_glob_constr t) na t in
let t = SPretyping.understand_tcc_evars evdref env IsType t' in
let d = (na,None,t) in
let impls =
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index 2eb7408aae..09cc17328c 100644
--- a/plugins/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
@@ -58,7 +58,7 @@ let my_print_rec_info env t =
str "Wf proof: " ++ my_print_constr env t.wf_proof ++ spc () ++
str "Abbreviated Type: " ++ my_print_constr env t.f_type ++ spc () ++
str "Full type: " ++ my_print_constr env t.f_fulltype
-(* trace (str "pretype for " ++ (my_print_rawconstr env c) ++ *)
+(* trace (str "pretype for " ++ (my_print_glob_constr env c) ++ *)
(* str " and tycon "++ my_print_tycon env tycon ++ *)
(* str " in environment: " ++ my_print_env env); *)
@@ -81,9 +81,9 @@ let find_with_index x l =
open Vernacexpr
-let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr =
+let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.glob_constr =
Constrintern.intern_constr evd env
-let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr =
+let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.glob_constr =
Constrintern.intern_type evd env
let env_with_binders env isevars l =
diff --git a/plugins/subtac/subtac_pretyping.mli b/plugins/subtac/subtac_pretyping.mli
index 48906b23cf..2b0c8fda28 100644
--- a/plugins/subtac/subtac_pretyping.mli
+++ b/plugins/subtac/subtac_pretyping.mli
@@ -13,7 +13,7 @@ module Pretyping : Pretyping.S
val interp :
Environ.env ->
Evd.evar_map ref ->
- Rawterm.rawconstr ->
+ Rawterm.glob_constr ->
Evarutil.type_constraint -> Term.constr * Term.constr
val subtac_process : ?is_type:bool -> env -> evar_map ref -> identifier -> local_binder list ->
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 3d79508c3a..debd4f0532 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -189,22 +189,22 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
(* in environment [env], with existential variables [( evdref)] and *)
(* the type constraint tycon *)
let rec pretype (tycon : type_constraint) env evdref lvar c =
-(* let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_rawconstr env c ++ *)
+(* let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_glob_constr env c ++ *)
(* str " with tycon " ++ Evarutil.pr_tycon env tycon) *)
(* with _ -> () *)
(* in *)
match c with
- | RRef (loc,ref) ->
+ | GRef (loc,ref) ->
inh_conv_coerce_to_tycon loc env evdref
(pretype_ref evdref env ref)
tycon
- | RVar (loc, id) ->
+ | GVar (loc, id) ->
inh_conv_coerce_to_tycon loc env evdref
(pretype_id loc env !evdref lvar id)
tycon
- | REvar (loc, ev, instopt) ->
+ | GEvar (loc, ev, instopt) ->
(* Ne faudrait-il pas s'assurer que hyps est bien un
sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
let hyps = evar_context (Evd.find !evdref ev) in
@@ -215,10 +215,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let j = (Retyping.get_judgment_of env !evdref c) in
inh_conv_coerce_to_tycon loc env evdref j tycon
- | RPatVar (loc,(someta,n)) ->
+ | GPatVar (loc,(someta,n)) ->
anomaly "Found a pattern variable in a rawterm to type"
- | RHole (loc,k) ->
+ | GHole (loc,k) ->
let ty =
match tycon with
| Some (None, ty) -> ty
@@ -226,7 +226,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
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) ->
+ | GRec (loc,fixkind,names,bl,lar,vdef) ->
let rec type_bl env ctxt = function
[] -> ctxt
| (na,k,None,ty)::bl ->
@@ -306,10 +306,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
make_judge (mkCoFix cofix) ftys.(i) in
inh_conv_coerce_to_tycon loc env evdref fixj tycon
- | RSort (loc,s) ->
+ | GSort (loc,s) ->
inh_conv_coerce_to_tycon loc env evdref (pretype_sort s) tycon
- | RApp (loc,f,args) ->
+ | GApp (loc,f,args) ->
let length = List.length args in
let ftycon =
let ty =
@@ -326,11 +326,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| _ -> None
in
let fj = pretype ftycon env evdref lvar f in
- let floc = loc_of_rawconstr f in
+ let floc = loc_of_glob_constr f in
let rec apply_rec env n resj tycon = function
| [] -> resj
| c::rest ->
- let argloc = loc_of_rawconstr c in
+ let argloc = loc_of_glob_constr c in
let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in
let resty = whd_betadeltaiota env !evdref resj.uj_type in
match kind_of_term resty with
@@ -364,7 +364,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| _ -> resj in
inh_conv_coerce_to_tycon loc env evdref resj tycon
- | RLambda(loc,name,k,c1,c2) ->
+ | GLambda(loc,name,k,c1,c2) ->
let tycon' = evd_comb1
(fun evd tycon ->
match tycon with
@@ -382,7 +382,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let resj = judge_of_abstraction env name j j' in
inh_conv_coerce_to_tycon loc env evdref resj tycon
- | RProd(loc,name,k,c1,c2) ->
+ | GProd(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' = Termops.push_rel_assum var env in
@@ -392,7 +392,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
with TypeError _ as e -> Loc.raise loc e in
inh_conv_coerce_to_tycon loc env evdref resj tycon
- | RLetIn(loc,name,c1,c2) ->
+ | GLetIn(loc,name,c1,c2) ->
let j = pretype empty_tycon env evdref lvar c1 in
let t = Termops.refresh_universes j.uj_type in
let var = (name,Some j.uj_val,t) in
@@ -401,12 +401,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
{ uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
uj_type = subst1 j.uj_val j'.uj_type }
- | RLetTuple (loc,nal,(na,po),c,d) ->
+ | GLetTuple (loc,nal,(na,po),c,d) ->
let cj = pretype empty_tycon env evdref lvar c in
let (IndType (indf,realargs)) =
try find_rectype env !evdref cj.uj_type
with Not_found ->
- let cloc = loc_of_rawconstr c in
+ let cloc = loc_of_glob_constr c in
error_case_not_inductive_loc cloc env !evdref cj
in
let cstrs = get_constructors env indf in
@@ -466,12 +466,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
in
{ uj_val = v; uj_type = ccl })
- | RIf (loc,c,(na,po),b1,b2) ->
+ | GIf (loc,c,(na,po),b1,b2) ->
let cj = pretype empty_tycon env evdref lvar c in
let (IndType (indf,realargs)) =
try find_rectype env !evdref cj.uj_type
with Not_found ->
- let cloc = loc_of_rawconstr c in
+ let cloc = loc_of_glob_constr c in
error_case_not_inductive_loc cloc env !evdref cj in
let cstrs = get_constructors env indf in
if Array.length cstrs <> 2 then
@@ -536,12 +536,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
in
{ uj_val = v; uj_type = p }
- | RCases (loc,sty,po,tml,eqns) ->
+ | GCases (loc,sty,po,tml,eqns) ->
Cases.compile_cases loc sty
((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref)
tycon env (* loc *) (po,tml,eqns)
- | RCast (loc,c,k) ->
+ | GCast (loc,c,k) ->
let cj =
match k with
CastCoerce ->
@@ -557,7 +557,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
in
inh_conv_coerce_to_tycon loc env evdref cj tycon
- | RDynamic (loc,d) ->
+ | GDynamic (loc,d) ->
if (Dyn.tag d) = "constr" then
let c = constr_out d in
let j = (Retyping.get_judgment_of env !evdref c) in
@@ -568,7 +568,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
(* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
and pretype_type valcon env evdref lvar = function
- | RHole loc ->
+ | GHole loc ->
(match valcon with
| Some v ->
let s =
@@ -588,7 +588,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
utj_type = s})
| c ->
let j = pretype empty_tycon env evdref lvar c in
- let loc = loc_of_rawconstr c in
+ let loc = loc_of_glob_constr c in
let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in
match valcon with
| None -> tj
@@ -596,7 +596,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
if e_cumul env evdref v tj.utj_val then tj
else
error_unexpected_type_loc
- (loc_of_rawconstr c) env !evdref tj.utj_val v
+ (loc_of_glob_constr c) env !evdref tj.utj_val v
let pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c =
let c' = match kind with
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index 106ac4d091..43b55ca95f 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -116,7 +116,7 @@ let my_print_rel_context env ctx = Printer.pr_rel_context env ctx
let my_print_context = Termops.print_rel_context
let my_print_named_context = Termops.print_named_context
let my_print_env = Termops.print_env
-let my_print_rawconstr = Printer.pr_rawconstr_env
+let my_print_glob_constr = Printer.pr_glob_constr_env
let my_print_evardefs = Evd.pr_evar_map
let my_print_tycon_type = Evarutil.pr_tycon_type
diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli
index f56c2932e5..659a677812 100644
--- a/plugins/subtac/subtac_utils.mli
+++ b/plugins/subtac/subtac_utils.mli
@@ -74,7 +74,7 @@ val my_print_context : env -> std_ppcmds
val my_print_rel_context : env -> rel_context -> std_ppcmds
val my_print_named_context : env -> std_ppcmds
val my_print_env : env -> std_ppcmds
-val my_print_rawconstr : env -> rawconstr -> std_ppcmds
+val my_print_glob_constr : env -> glob_constr -> std_ppcmds
val my_print_tycon_type : env -> type_constraint_type -> std_ppcmds
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-28 00:22:31 +0000