aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml26
-rw-r--r--pretyping/detyping.ml208
-rw-r--r--pretyping/detyping.mli6
-rw-r--r--pretyping/glob_ops.ml268
-rw-r--r--pretyping/patternops.ml45
-rw-r--r--pretyping/pretyping.ml36
6 files changed, 292 insertions, 297 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 5314859358..347c49f448 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -348,8 +348,8 @@ let find_tomatch_tycon evdref env loc = function
empty_tycon,None
let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) =
- let loc = Some (loc_of_glob_constr tomatch) in
- let tycon,realnames = find_tomatch_tycon evdref env loc indopt in
+ let loc = loc_of_glob_constr tomatch in
+ let tycon,realnames = find_tomatch_tycon evdref env (Some loc) indopt in
let j = typing_fun tycon env evdref tomatch in
let evd, j = Coercion.inh_coerce_to_base (loc_of_glob_constr tomatch) env !evdref j in
evdref := evd;
@@ -357,7 +357,7 @@ let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) =
let t =
try try_find_ind env !evdref typ realnames
with Not_found ->
- unify_tomatch_with_patterns evdref env loc typ pats realnames in
+ unify_tomatch_with_patterns evdref env (Some loc) typ pats realnames in
(j.uj_val,t)
let coerce_to_indtype typing_fun evdref env matx tomatchl =
@@ -1535,7 +1535,7 @@ substituer après par les initiaux *)
* and linearizing the _ patterns.
* Syntactic correctness has already been done in astterm *)
let matx_of_eqns env eqns =
- let build_eqn (loc,ids,lpat,rhs) =
+ let build_eqn (loc,(ids,lpat,rhs)) =
let initial_lpat,initial_rhs = lpat,rhs in
let initial_rhs = rhs in
let rhs =
@@ -2059,8 +2059,8 @@ let mk_JMeq evdref typ x typ' y =
let mk_JMeq_refl evdref typ x =
papp evdref coq_JMeq_refl [| typ; x |]
-let hole =
- GHole (Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false),
+let hole = Loc.tag @@
+ GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false),
Misctypes.IntroAnonymous, None)
let constr_of_pat env evdref arsign pat avoid =
@@ -2160,13 +2160,13 @@ let vars_of_ctx sigma ctx =
match decl with
| LocalDef (na,t',t) when is_topvar sigma t' ->
prev,
- (GApp (Loc.ghost,
- (GRef (Loc.ghost, delayed_force coq_eq_refl_ref, None)),
- [hole; GVar (Loc.ghost, prev)])) :: vars
+ (Loc.tag @@ GApp (
+ (Loc.tag @@ GRef (delayed_force coq_eq_refl_ref, None)),
+ [hole; Loc.tag @@ GVar prev])) :: vars
| _ ->
match RelDecl.get_name decl with
Anonymous -> invalid_arg "vars_of_ctx"
- | Name n -> n, GVar (Loc.ghost, n) :: vars)
+ | Name n -> n, (Loc.tag @@ GVar n) :: vars)
ctx (Id.of_string "vars_of_ctx_error", [])
in List.rev y
@@ -2289,13 +2289,13 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in
let branch_decl = LocalDef (Name branch_name, lift !i bbody, lift !i btype) in
let branch =
- let bref = GVar (Loc.ghost, branch_name) in
+ let bref = Loc.tag @@ GVar branch_name in
match vars_of_ctx !evdref rhs_rels with
[] -> bref
- | l -> GApp (Loc.ghost, bref, l)
+ | l -> Loc.tag @@ GApp (bref, l)
in
let branch = match ineqs with
- Some _ -> GApp (Loc.ghost, branch, [ hole ])
+ Some _ -> Loc.tag @@ GApp (branch, [ hole ])
| None -> branch
in
incr i;
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index f3018ac64b..05d6a1ad4a 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -331,20 +331,20 @@ let is_nondep_branch sigma c l =
let extract_nondep_branches test c b l =
let rec strip l r =
- match r,l with
- | r, [] -> r
- | GLambda (_,_,_,_,t), false::l -> strip l t
- | GLetIn (_,_,_,_,t), true::l -> strip l t
+ match snd r,l with
+ | r', [] -> r
+ | GLambda (_,_,_,t), false::l -> strip l t
+ | GLetIn (_,_,_,t), true::l -> strip l t
(* FIXME: do we need adjustment? *)
| _,_ -> assert false in
if test c l then Some (strip l b) else None
let it_destRLambda_or_LetIn_names l c =
let rec aux l nal c =
- match c, l with
+ match snd c, l with
| _, [] -> (List.rev nal,c)
- | GLambda (_,na,_,_,c), false::l -> aux l (na::nal) c
- | GLetIn (_,na,_,_,c), true::l -> aux l (na::nal) c
+ | GLambda (na,_,_,c), false::l -> aux l (na::nal) c
+ | GLetIn (na,_,_,c), true::l -> aux l (na::nal) c
| _, true::l -> (* let-expansion *) aux l (Anonymous :: nal) c
| _, false::l ->
(* eta-expansion *)
@@ -355,11 +355,11 @@ let it_destRLambda_or_LetIn_names l c =
x
in
let x = next (free_glob_vars c) in
- let a = GVar (dl,x) in
+ let a = Loc.tag @@ GVar x in
aux l (Name x :: nal)
(match c with
- | GApp (loc,p,l) -> GApp (loc,p,l@[a])
- | _ -> (GApp (dl,c,[a])))
+ | loc, GApp (p,l) -> (loc, GApp (p,l@[a]))
+ | _ -> Loc.tag @@ GApp (c,[a]))
in aux l [] c
let detype_case computable detype detype_eqns testdep avoid data p c bl =
@@ -375,12 +375,12 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
| None -> Anonymous, None, None
| Some p ->
let nl,typ = it_destRLambda_or_LetIn_names k p in
- let n,typ = match typ with
- | GLambda (_,x,_,t,c) -> x, c
+ let n,typ = match snd typ with
+ | GLambda (x,_,t,c) -> x, c
| _ -> Anonymous, typ in
let aliastyp =
if List.for_all (Name.equal Anonymous) nl then None
- else Some (dl,(indsp,nl)) in
+ else Some (Loc.tag (indsp,nl)) in
n, aliastyp, Some typ
in
let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in
@@ -397,25 +397,25 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
else
st
with Not_found -> st
- in
+ in Loc.tag @@
match tag, aliastyp with
| LetStyle, None ->
let bl' = Array.map detype bl in
let (nal,d) = it_destRLambda_or_LetIn_names constagsl.(0) bl'.(0) in
- GLetTuple (dl,nal,(alias,pred),tomatch,d)
+ GLetTuple (nal,(alias,pred),tomatch,d)
| IfStyle, None ->
let bl' = Array.map detype bl in
let nondepbrs =
Array.map3 (extract_nondep_branches testdep) bl bl' constagsl in
if Array.for_all ((!=) None) nondepbrs then
- GIf (dl,tomatch,(alias,pred),
+ GIf (tomatch,(alias,pred),
Option.get nondepbrs.(0),Option.get nondepbrs.(1))
else
let eqnl = detype_eqns constructs constagsl bl in
- GCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
+ GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl)
| _ ->
let eqnl = detype_eqns constructs constagsl bl in
- GCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
+ GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl)
let detype_sort sigma = function
| Prop Null -> GProp
@@ -423,7 +423,7 @@ let detype_sort sigma = function
| Type u ->
GType
(if !print_universes
- then [dl, Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u)]
+ then [Loc.tag @@ Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u)]
else [])
type binder_kind = BProd | BLambda | BLetIn
@@ -431,36 +431,36 @@ type binder_kind = BProd | BLambda | BLetIn
(**********************************************************************)
(* Main detyping function *)
-let detype_anonymous = ref (fun loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable"))
+let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable"))
let set_detype_anonymous f = detype_anonymous := f
let detype_level sigma l =
- GType (Some (dl, Pp.string_of_ppcmds (Termops.pr_evd_level sigma l)))
+ GType (Some (Loc.tag @@ Pp.string_of_ppcmds (Termops.pr_evd_level sigma l)))
let detype_instance sigma l =
let l = EInstance.kind sigma l in
if Univ.Instance.is_empty l then None
else Some (List.map (detype_level sigma) (Array.to_list (Univ.Instance.to_array l)))
-let rec detype flags avoid env sigma t =
+let rec detype flags avoid env sigma t = Loc.tag @@
match EConstr.kind sigma (collapse_appl sigma t) with
| Rel n ->
(try match lookup_name_of_rel n (fst env) with
- | Name id -> GVar (dl, id)
- | Anonymous -> !detype_anonymous dl n
+ | Name id -> GVar id
+ | Anonymous -> snd @@ !detype_anonymous n
with Not_found ->
let s = "_UNBOUND_REL_"^(string_of_int n)
- in GVar (dl, Id.of_string s))
+ in GVar (Id.of_string s))
| Meta n ->
(* Meta in constr are not user-parsable and are mapped to Evar *)
(* using numbers to be unparsable *)
- GEvar (dl, Id.of_string ("M" ^ string_of_int n), [])
+ GEvar (Id.of_string ("M" ^ string_of_int n), [])
| Var id ->
- (try let _ = Global.lookup_named id in GRef (dl, VarRef id, None)
- with Not_found -> GVar (dl, id))
- | Sort s -> GSort (dl,detype_sort sigma (ESorts.kind sigma s))
+ (try let _ = Global.lookup_named id in GRef (VarRef id, None)
+ with Not_found -> GVar id)
+ | Sort s -> GSort (detype_sort sigma (ESorts.kind sigma s))
| Cast (c1,REVERTcast,c2) when not !Flags.raw_print ->
- detype flags avoid env sigma c1
+ snd (detype flags avoid env sigma c1)
| Cast (c1,k,c2) ->
let d1 = detype flags avoid env sigma c1 in
let d2 = detype flags avoid env sigma c2 in
@@ -469,34 +469,34 @@ let rec detype flags avoid env sigma t =
| NATIVEcast -> CastNative d2
| _ -> CastConv d2
in
- GCast(dl,d1,cast)
- | Prod (na,ty,c) -> detype_binder flags BProd avoid env sigma na None ty c
- | Lambda (na,ty,c) -> detype_binder flags BLambda avoid env sigma na None ty c
- | LetIn (na,b,ty,c) -> detype_binder flags BLetIn avoid env sigma na (Some b) ty c
+ GCast(d1,cast)
+ | Prod (na,ty,c) -> snd @@ detype_binder flags BProd avoid env sigma na None ty c
+ | Lambda (na,ty,c) -> snd @@ detype_binder flags BLambda avoid env sigma na None ty c
+ | LetIn (na,b,ty,c) -> snd @@ detype_binder flags BLetIn avoid env sigma na (Some b) ty c
| App (f,args) ->
let mkapp f' args' =
- match f' with
- | GApp (dl',f',args'') ->
- GApp (dl,f',args''@args')
- | _ -> GApp (dl,f',args')
+ match snd f' with
+ | GApp (f',args'') ->
+ GApp (f',args''@args')
+ | _ -> GApp (f',args')
in
mkapp (detype flags avoid env sigma f)
(Array.map_to_list (detype flags avoid env sigma) args)
- | Const (sp,u) -> GRef (dl, ConstRef sp, detype_instance sigma u)
+ | Const (sp,u) -> GRef (ConstRef sp, detype_instance sigma u)
| Proj (p,c) ->
let noparams () =
let pb = Environ.lookup_projection p (snd env) in
let pars = pb.Declarations.proj_npars in
- let hole = GHole(Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in
+ let hole = Loc.tag @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in
let args = List.make pars hole in
- GApp (dl, GRef (dl, ConstRef (Projection.constant p), None),
+ GApp (Loc.tag @@ GRef (ConstRef (Projection.constant p), None),
(args @ [detype flags avoid env sigma c]))
in
if fst flags || !Flags.in_debugger || !Flags.in_toplevel then
try noparams ()
with _ ->
(* lax mode, used by debug printers only *)
- GApp (dl, GRef (dl, ConstRef (Projection.constant p), None),
+ GApp (Loc.tag @@ GRef (ConstRef (Projection.constant p), None),
[detype flags avoid env sigma c])
else
if print_primproj_compatibility () && Projection.unfolded p then
@@ -514,12 +514,12 @@ let rec detype flags avoid env sigma t =
substl (c :: List.rev args) body'
with Retyping.RetypeError _ | Not_found ->
anomaly (str"Cannot detype an unfolded primitive projection.")
- in detype flags avoid env sigma c'
+ in snd @@ detype flags avoid env sigma c'
else
if print_primproj_params () then
try
let c = Retyping.expand_projection (snd env) sigma p c [] in
- detype flags avoid env sigma c
+ snd @@ detype flags avoid env sigma c
with Retyping.RetypeError _ -> noparams ()
else noparams ()
@@ -546,14 +546,15 @@ let rec detype flags avoid env sigma t =
Id.of_string ("X" ^ string_of_int (Evar.repr evk)),
(Array.map_to_list (fun c -> (Id.of_string "__",c)) cl)
in
- GEvar (dl,id,
+ GEvar (id,
List.map (on_snd (detype flags avoid env sigma)) l)
| Ind (ind_sp,u) ->
- GRef (dl, IndRef ind_sp, detype_instance sigma u)
+ GRef (IndRef ind_sp, detype_instance sigma u)
| Construct (cstr_sp,u) ->
- GRef (dl, ConstructRef cstr_sp, detype_instance sigma u)
+ GRef (ConstructRef cstr_sp, detype_instance sigma u)
| Case (ci,p,c,bl) ->
let comp = computable sigma p (List.length (ci.ci_pp_info.ind_tags)) in
+ snd @@
detype_case comp (detype flags avoid env sigma)
(detype_eqns flags avoid env sigma ci comp)
(is_nondep_branch sigma) avoid
@@ -574,7 +575,7 @@ and detype_fix flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) =
let v = Array.map3
(fun c t i -> share_names flags (i+1) [] def_avoid def_env sigma c (lift n t))
bodies tys vn in
- GRec(dl,GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
+ GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
Array.map (fun (bl,_,_) -> bl) v,
Array.map (fun (_,_,ty) -> ty) v,
Array.map (fun (_,bd,_) -> bd) v)
@@ -590,7 +591,7 @@ and detype_cofix flags avoid env sigma n (names,tys,bodies) =
let v = Array.map2
(fun c t -> share_names flags 0 [] def_avoid def_env sigma c (lift ntys t))
bodies tys in
- GRec(dl,GCoFix n,Array.of_list (List.rev lfi),
+ GRec(GCoFix n,Array.of_list (List.rev lfi),
Array.map (fun (bl,_,_) -> bl) v,
Array.map (fun (_,_,ty) -> ty) v,
Array.map (fun (_,bd,_) -> bd) v)
@@ -635,7 +636,7 @@ and detype_eqns flags avoid env sigma ci computable constructs consnargsl bl =
try
if !Flags.raw_print || not (reverse_matching ()) then raise Exit;
let mat = build_tree Anonymous (snd flags) (avoid,env) sigma ci bl in
- List.map (fun (pat,((avoid,env),c)) -> (dl,[],[pat],detype flags avoid env sigma c))
+ List.map (fun (pat,((avoid,env),c)) -> Loc.tag ([],[pat],detype flags avoid env sigma c))
mat
with e when CErrors.noncritical e ->
Array.to_list
@@ -644,7 +645,7 @@ and detype_eqns flags avoid env sigma ci computable constructs consnargsl bl =
and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs branch =
let make_pat x avoid env b body ty ids =
if force_wildcard () && noccurn sigma 1 b then
- Loc.tag @@ PatVar (Anonymous),avoid,(add_name Anonymous body ty env),ids
+ Loc.tag @@ PatVar Anonymous,avoid,(add_name Anonymous body ty env),ids
else
let flag = if isgoal then RenamingForGoal else RenamingForCasesPattern (fst env,b) in
let na,avoid' = compute_displayed_name_in sigma flag avoid x b in
@@ -652,9 +653,9 @@ and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs bran
in
let rec buildrec ids patlist avoid env l b =
match EConstr.kind sigma b, l with
- | _, [] ->
- (dl, Id.Set.elements ids,
- [Loc.tag ~loc:dl @@ PatCstr(constr, List.rev patlist,Anonymous)],
+ | _, [] -> Loc.tag @@
+ (Id.Set.elements ids,
+ [Loc.tag @@ PatCstr(constr, List.rev patlist,Anonymous)],
detype flags avoid env sigma b)
| Lambda (x,t,b), false::l ->
let pat,new_avoid,new_env,new_ids = make_pat x avoid env b None t ids in
@@ -668,7 +669,7 @@ and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs bran
buildrec ids patlist avoid env l c
| _, true::l ->
- let pat = Loc.tag ~loc:dl @@ PatVar Anonymous in
+ let pat = Loc.tag @@ PatVar Anonymous in
buildrec ids (pat::patlist) avoid env l b
| _, false::l ->
@@ -683,21 +684,21 @@ and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs bran
in
buildrec Id.Set.empty [] avoid env construct_nargs branch
-and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c =
+and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c = Loc.tag @@
let flag = if isgoal then RenamingForGoal else RenamingElsewhereFor (fst env,c) in
let na',avoid' = match bk with
| BLetIn -> compute_displayed_let_name_in sigma flag avoid na c
| _ -> compute_displayed_name_in sigma flag avoid na c in
let r = detype flags avoid' (add_name na' body ty env) sigma c in
match bk with
- | BProd -> GProd (dl, na',Explicit,detype (lax,false) avoid env sigma ty, r)
- | BLambda -> GLambda (dl, na',Explicit,detype (lax,false) avoid env sigma ty, r)
+ | BProd -> GProd (na',Explicit,detype (lax,false) avoid env sigma ty, r)
+ | BLambda -> GLambda (na',Explicit,detype (lax,false) avoid env sigma ty, r)
| BLetIn ->
let c = detype (lax,false) avoid env sigma (Option.get body) in
(* Heuristic: we display the type if in Prop *)
let s = try Retyping.get_sort_family_of (snd env) sigma ty with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in
let t = if s != InProp then None else Some (detype (lax,false) avoid env sigma ty) in
- GLetIn (dl, na', c, t, r)
+ GLetIn (na', c, t, r)
let detype_rel_context ?(lax=false) where avoid env sigma sign =
let where = Option.map (fun c -> EConstr.it_mkLambda_or_LetIn c sign) where in
@@ -741,11 +742,11 @@ let detype_closed_glob ?lax isgoal avoid env sigma t =
| Name id -> Name (convert_id cl id)
| Anonymous -> Anonymous
in
- let rec detype_closed_glob cl = function
- | GVar (loc,id) ->
+ let rec detype_closed_glob cl cg = Loc.map (function
+ | GVar id ->
(* if [id] is bound to a name. *)
begin try
- GVar(loc,Id.Map.find id cl.idents)
+ GVar(Id.Map.find id cl.idents)
(* if [id] is bound to a typed term *)
with Not_found -> try
(* assumes [detype] does not raise [Not_found] exceptions *)
@@ -755,38 +756,39 @@ let detype_closed_glob ?lax isgoal avoid env sigma t =
[Printer.pr_constr_under_binders_env] does. *)
let assums = List.map (fun id -> LocalAssum (Name id,(* dummy *) mkProp)) b in
let env = push_rel_context assums env in
- detype ?lax isgoal avoid env sigma c
+ snd @@ detype ?lax isgoal avoid env sigma c
(* if [id] is bound to a [closed_glob_constr]. *)
with Not_found -> try
let {closure;term} = Id.Map.find id cl.untyped in
- detype_closed_glob closure term
+ snd @@ detype_closed_glob closure term
(* Otherwise [id] stands for itself *)
with Not_found ->
- GVar(loc,id)
+ GVar id
end
- | GLambda (loc,id,k,t,c) ->
+ | GLambda (id,k,t,c) ->
let id = convert_name cl id in
- GLambda(loc,id,k,detype_closed_glob cl t, detype_closed_glob cl c)
- | GProd (loc,id,k,t,c) ->
+ GLambda(id,k,detype_closed_glob cl t, detype_closed_glob cl c)
+ | GProd (id,k,t,c) ->
let id = convert_name cl id in
- GProd(loc,id,k,detype_closed_glob cl t, detype_closed_glob cl c)
- | GLetIn (loc,id,b,t,e) ->
+ GProd(id,k,detype_closed_glob cl t, detype_closed_glob cl c)
+ | GLetIn (id,b,t,e) ->
let id = convert_name cl id in
- GLetIn(loc,id,detype_closed_glob cl b, Option.map (detype_closed_glob cl) t, detype_closed_glob cl e)
- | GLetTuple (loc,ids,(n,r),b,e) ->
+ GLetIn(id,detype_closed_glob cl b, Option.map (detype_closed_glob cl) t, detype_closed_glob cl e)
+ | GLetTuple (ids,(n,r),b,e) ->
let ids = List.map (convert_name cl) ids in
let n = convert_name cl n in
- GLetTuple (loc,ids,(n,r),detype_closed_glob cl b, detype_closed_glob cl e)
- | GCases (loc,sty,po,tml,eqns) ->
+ GLetTuple (ids,(n,r),detype_closed_glob cl b, detype_closed_glob cl e)
+ | GCases (sty,po,tml,eqns) ->
let (tml,eqns) =
Glob_ops.map_pattern_binders (fun na -> convert_name cl na) tml eqns
in
let (tml,eqns) =
Glob_ops.map_pattern (fun c -> detype_closed_glob cl c) tml eqns
in
- GCases(loc,sty,po,tml,eqns)
+ GCases(sty,po,tml,eqns)
| c ->
- Glob_ops.map_glob_constr (detype_closed_glob cl) c
+ snd @@ Glob_ops.map_glob_constr (detype_closed_glob cl) cg
+ ) cg
in
detype_closed_glob t.closure t.term
@@ -804,41 +806,41 @@ let rec subst_cases_pattern subst (loc, pat) = Loc.tag ~loc @@
let (f_subst_genarg, subst_genarg_hook) = Hook.make ()
-let rec subst_glob_constr subst raw =
+let rec subst_glob_constr subst (loc, raw) = Loc.tag ~loc @@
match raw with
- | GRef (loc,ref,u) ->
+ | GRef (ref,u) ->
let ref',t = subst_global subst ref in
if ref' == ref then raw else
- detype false [] (Global.env()) Evd.empty (EConstr.of_constr t)
+ snd @@ detype false [] (Global.env()) Evd.empty (EConstr.of_constr t)
| GVar _ -> raw
| GEvar _ -> raw
| GPatVar _ -> raw
- | GApp (loc,r,rl) ->
+ | GApp (r,rl) ->
let r' = subst_glob_constr subst r
and rl' = List.smartmap (subst_glob_constr subst) rl in
if r' == r && rl' == rl then raw else
- GApp(loc,r',rl')
+ GApp(r',rl')
- | GLambda (loc,n,bk,r1,r2) ->
+ | GLambda (n,bk,r1,r2) ->
let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in
if r1' == r1 && r2' == r2 then raw else
- GLambda (loc,n,bk,r1',r2')
+ GLambda (n,bk,r1',r2')
- | GProd (loc,n,bk,r1,r2) ->
+ | GProd (n,bk,r1,r2) ->
let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in
if r1' == r1 && r2' == r2 then raw else
- GProd (loc,n,bk,r1',r2')
+ GProd (n,bk,r1',r2')
- | GLetIn (loc,n,r1,t,r2) ->
+ | GLetIn (n,r1,t,r2) ->
let r1' = subst_glob_constr subst r1 in
- let t' = Option.smartmap (subst_glob_constr subst) t in
let r2' = subst_glob_constr subst r2 in
+ let t' = Option.smartmap (subst_glob_constr subst) t in
if r1' == r1 && t == t' && r2' == r2 then raw else
- GLetIn (loc,n,r1',t',r2')
+ GLetIn (n,r1',t',r2')
- | GCases (loc,sty,rtno,rl,branches) ->
+ | GCases (sty,rtno,rl,branches) ->
let rtno' = Option.smartmap (subst_glob_constr subst) rtno
and rl' = List.smartmap (fun (a,x as y) ->
let a' = subst_glob_constr subst a in
@@ -849,33 +851,33 @@ let rec subst_glob_constr subst raw =
if sp == sp' then t else (loc,((sp',i),y))) topt in
if a == a' && topt == topt' then y else (a',(n,topt'))) rl
and branches' = List.smartmap
- (fun (loc,idl,cpl,r as branch) ->
+ (fun (loc,(idl,cpl,r) as branch) ->
let cpl' =
List.smartmap (subst_cases_pattern subst) cpl
and r' = subst_glob_constr subst r in
if cpl' == cpl && r' == r then branch else
- (loc,idl,cpl',r'))
+ (loc,(idl,cpl',r')))
branches
in
if rtno' == rtno && rl' == rl && branches' == branches then raw else
- GCases (loc,sty,rtno',rl',branches')
+ GCases (sty,rtno',rl',branches')
- | GLetTuple (loc,nal,(na,po),b,c) ->
+ | GLetTuple (nal,(na,po),b,c) ->
let po' = Option.smartmap (subst_glob_constr subst) po
and b' = subst_glob_constr subst b
and c' = subst_glob_constr subst c in
if po' == po && b' == b && c' == c then raw else
- GLetTuple (loc,nal,(na,po'),b',c')
+ GLetTuple (nal,(na,po'),b',c')
- | GIf (loc,c,(na,po),b1,b2) ->
+ | GIf (c,(na,po),b1,b2) ->
let po' = Option.smartmap (subst_glob_constr subst) po
and b1' = subst_glob_constr subst b1
and b2' = subst_glob_constr subst b2
and c' = subst_glob_constr subst c in
if c' == c && po' == po && b1' == b1 && b2' == b2 then raw else
- GIf (loc,c',(na,po'),b1',b2')
+ GIf (c',(na,po'),b1',b2')
- | GRec (loc,fix,ida,bl,ra1,ra2) ->
+ | GRec (fix,ida,bl,ra1,ra2) ->
let ra1' = Array.smartmap (subst_glob_constr subst) ra1
and ra2' = Array.smartmap (subst_glob_constr subst) ra2 in
let bl' = Array.smartmap
@@ -885,11 +887,11 @@ let rec subst_glob_constr subst raw =
if ty'==ty && obd'==obd then dcl else (na,k,obd',ty')))
bl in
if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else
- GRec (loc,fix,ida,bl',ra1',ra2')
+ GRec (fix,ida,bl',ra1',ra2')
| GSort _ -> raw
- | GHole (loc, knd, naming, solve) ->
+ | GHole (knd, naming, solve) ->
let nknd = match knd with
| Evar_kinds.ImplicitArg (ref, i, b) ->
let nref, _ = subst_global subst ref in
@@ -898,12 +900,12 @@ let rec subst_glob_constr subst raw =
in
let nsolve = Option.smartmap (Hook.get f_subst_genarg subst) solve in
if nsolve == solve && nknd == knd then raw
- else GHole (loc, nknd, naming, nsolve)
+ else GHole (nknd, naming, nsolve)
- | GCast (loc,r1,k) ->
+ | GCast (r1,k) ->
let r1' = subst_glob_constr subst r1 in
let k' = Miscops.smartmap_cast_type (subst_glob_constr subst) k in
- if r1' == r1 && k' == k then raw else GCast (loc,r1',k')
+ if r1' == r1 && k' == k then raw else GCast (r1',k')
(* Utilities to transform kernel cases to simple pattern-matching problem *)
@@ -914,7 +916,7 @@ let simple_cases_matrix_of_branches ind brs =
let p = Loc.tag @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in
let map name = try Some (Nameops.out_name name) with Failure _ -> None in
let ids = List.map_filter map nal in
- (Loc.ghost,ids,[p],c))
+ Loc.tag @@ (ids,[p],c))
brs
let return_type_of_predicate ind nrealargs_tags pred =
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 4c6f9129f6..84da3652f1 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -38,7 +38,7 @@ val detype : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> constr -> glob
val detype_case :
bool -> (constr -> glob_constr) ->
(constructor array -> bool list array -> constr array ->
- (Loc.t * Id.t list * cases_pattern list * glob_constr) list) ->
+ (Id.t list * cases_pattern list * glob_constr) Loc.located list) ->
(constr -> bool list -> bool) ->
Id.t list -> inductive * case_style * bool list array * bool list ->
constr option -> constr -> constr array -> glob_constr
@@ -54,7 +54,9 @@ val detype_closed_glob : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> cl
val lookup_name_as_displayed : env -> evar_map -> constr -> Id.t -> int option
val lookup_index_as_renamed : env -> evar_map -> constr -> int -> int option
-val set_detype_anonymous : (Loc.t -> int -> glob_constr) -> unit
+(* XXX: This is a hack and should go away *)
+val set_detype_anonymous : (?loc:Loc.t -> int -> glob_constr) -> unit
+
val force_wildcard : unit -> bool
val synthetize_type : unit -> bool
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 4cccaaf8ff..25ece5b8e9 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -22,10 +22,10 @@ let cases_predicate_names tml =
| (tm,(na,None)) -> [na]
| (tm,(na,Some (_,(_,nal)))) -> na::nal) tml)
-let mkGApp loc p t =
- match p with
- | GApp (loc,f,l) -> GApp (loc,f,l@[t])
- | _ -> GApp (loc,p,[t])
+let mkGApp loc p t = Loc.tag ~loc @@
+ match snd p with
+ | GApp (f,l) -> GApp (f,l@[t])
+ | _ -> GApp (p,[t])
let map_glob_decl_left_to_right f (na,k,obd,ty) =
let comp1 = Option.map f obd in
@@ -59,46 +59,46 @@ let cast_type_eq eq t1 t2 = match t1, t2 with
| CastNative t1, CastNative t2 -> eq t1 t2
| _ -> false
-let rec glob_constr_eq c1 c2 = match c1, c2 with
-| GRef (_, gr1, _), GRef (_, gr2, _) -> eq_gr gr1 gr2
-| GVar (_, id1), GVar (_, id2) -> Id.equal id1 id2
-| GEvar (_, id1, arg1), GEvar (_, id2, arg2) ->
+let rec glob_constr_eq (_loc1, c1) (_loc2, c2) = match c1, c2 with
+| GRef (gr1, _), GRef (gr2, _) -> eq_gr gr1 gr2
+| GVar id1, GVar id2 -> Id.equal id1 id2
+| GEvar (id1, arg1), GEvar (id2, arg2) ->
Id.equal id1 id2 &&
List.equal instance_eq arg1 arg2
-| GPatVar (_, (b1, pat1)), GPatVar (_, (b2, pat2)) ->
+| GPatVar (b1, pat1), GPatVar (b2, pat2) ->
(b1 : bool) == b2 && Id.equal pat1 pat2
-| GApp (_, f1, arg1), GApp (_, f2, arg2) ->
+| GApp (f1, arg1), GApp (f2, arg2) ->
glob_constr_eq f1 f2 && List.equal glob_constr_eq arg1 arg2
-| GLambda (_, na1, bk1, t1, c1), GLambda (_, na2, bk2, t2, c2) ->
+| GLambda (na1, bk1, t1, c1), GLambda (na2, bk2, t2, c2) ->
Name.equal na1 na2 && binding_kind_eq bk1 bk2 &&
glob_constr_eq t1 t2 && glob_constr_eq c1 c2
-| GProd (_, na1, bk1, t1, c1), GProd (_, na2, bk2, t2, c2) ->
+| GProd (na1, bk1, t1, c1), GProd (na2, bk2, t2, c2) ->
Name.equal na1 na2 && binding_kind_eq bk1 bk2 &&
glob_constr_eq t1 t2 && glob_constr_eq c1 c2
-| GLetIn (_, na1, b1, t1, c1), GLetIn (_, na2, b2, t2, c2) ->
+| GLetIn (na1, b1, t1, c1), GLetIn (na2, b2, t2, c2) ->
Name.equal na1 na2 && glob_constr_eq b1 b2 && Option.equal glob_constr_eq t1 t2 && glob_constr_eq c1 c2
-| GCases (_, st1, c1, tp1, cl1), GCases (_, st2, c2, tp2, cl2) ->
+| GCases (st1, c1, tp1, cl1), GCases (st2, c2, tp2, cl2) ->
case_style_eq st1 st2 && Option.equal glob_constr_eq c1 c2 &&
List.equal tomatch_tuple_eq tp1 tp2 &&
List.equal cases_clause_eq cl1 cl2
-| GLetTuple (_, na1, (n1, p1), c1, t1), GLetTuple (_, na2, (n2, p2), c2, t2) ->
+| GLetTuple (na1, (n1, p1), c1, t1), GLetTuple (na2, (n2, p2), c2, t2) ->
List.equal Name.equal na1 na2 && Name.equal n1 n2 &&
Option.equal glob_constr_eq p1 p2 && glob_constr_eq c1 c2 &&
glob_constr_eq t1 t2
-| GIf (_, m1, (pat1, p1), c1, t1), GIf (_, m2, (pat2, p2), c2, t2) ->
+| GIf (m1, (pat1, p1), c1, t1), GIf (m2, (pat2, p2), c2, t2) ->
glob_constr_eq m1 m2 && Name.equal pat1 pat2 &&
Option.equal glob_constr_eq p1 p2 && glob_constr_eq c1 c2 &&
glob_constr_eq t1 t2
-| GRec (_, kn1, id1, decl1, c1, t1), GRec (_, kn2, id2, decl2, c2, t2) ->
+| GRec (kn1, id1, decl1, c1, t1), GRec (kn2, id2, decl2, c2, t2) ->
fix_kind_eq kn1 kn2 && Array.equal Id.equal id1 id2 &&
Array.equal (fun l1 l2 -> List.equal glob_decl_eq l1 l2) decl1 decl2 &&
Array.equal glob_constr_eq c1 c2 &&
Array.equal glob_constr_eq t1 t2
-| GSort (_, s1), GSort (_, s2) -> Miscops.glob_sort_eq s1 s2
-| GHole (_, kn1, nam1, gn1), GHole (_, kn2, nam2, gn2) ->
+| GSort s1, GSort s2 -> Miscops.glob_sort_eq s1 s2
+| GHole (kn1, nam1, gn1), GHole (kn2, nam2, gn2) ->
Option.equal (==) gn1 gn2 (** Only thing sensible *) &&
Miscops.intro_pattern_naming_eq nam1 nam2
-| GCast (_, c1, t1), GCast (_, c2, t2) ->
+| GCast (c1, t1), GCast (c2, t2) ->
glob_constr_eq c1 c2 && cast_type_eq glob_constr_eq t1 t2
| _ -> false
@@ -109,7 +109,7 @@ and tomatch_tuple_eq (c1, p1) (c2, p2) =
let eq_pred (n1, o1) (n2, o2) = Name.equal n1 n2 && Option.equal eqp o1 o2 in
glob_constr_eq c1 c2 && eq_pred p1 p2
-and cases_clause_eq (_, id1, p1, c1) (_, id2, p2, c2) =
+and cases_clause_eq (_, (id1, p1, c1)) (_, (id2, p2, c2)) =
List.equal Id.equal id1 id2 && List.equal cases_pattern_eq p1 p2 &&
glob_constr_eq c1 c2
@@ -137,80 +137,82 @@ and fix_recursion_order_eq o1 o2 = match o1, o2 with
and instance_eq (x1,c1) (x2,c2) =
Id.equal x1 x2 && glob_constr_eq c1 c2
-let map_glob_constr_left_to_right f = function
- | GApp (loc,g,args) ->
+let map_glob_constr_left_to_right f = Loc.map (function
+ | GApp (g,args) ->
let comp1 = f g in
let comp2 = Util.List.map_left f args in
- GApp (loc,comp1,comp2)
- | GLambda (loc,na,bk,ty,c) ->
+ GApp (comp1,comp2)
+ | GLambda (na,bk,ty,c) ->
let comp1 = f ty in
let comp2 = f c in
- GLambda (loc,na,bk,comp1,comp2)
- | GProd (loc,na,bk,ty,c) ->
+ GLambda (na,bk,comp1,comp2)
+ | GProd (na,bk,ty,c) ->
let comp1 = f ty in
let comp2 = f c in
- GProd (loc,na,bk,comp1,comp2)
- | GLetIn (loc,na,b,t,c) ->
+ GProd (na,bk,comp1,comp2)
+ | GLetIn (na,b,t,c) ->
let comp1 = f b in
let compt = Option.map f t in
let comp2 = f c in
- GLetIn (loc,na,comp1,compt,comp2)
- | GCases (loc,sty,rtntypopt,tml,pl) ->
+ GLetIn (na,comp1,compt,comp2)
+ | GCases (sty,rtntypopt,tml,pl) ->
let comp1 = Option.map f rtntypopt in
let comp2 = Util.List.map_left (fun (tm,x) -> (f tm,x)) tml in
- let comp3 = Util.List.map_left (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl in
- GCases (loc,sty,comp1,comp2,comp3)
- | GLetTuple (loc,nal,(na,po),b,c) ->
+ let comp3 = Util.List.map_left (fun (loc,(idl,p,c)) -> (loc,(idl,p,f c))) pl in
+ GCases (sty,comp1,comp2,comp3)
+ | GLetTuple (nal,(na,po),b,c) ->
let comp1 = Option.map f po in
let comp2 = f b in
let comp3 = f c in
- GLetTuple (loc,nal,(na,comp1),comp2,comp3)
- | GIf (loc,c,(na,po),b1,b2) ->
+ GLetTuple (nal,(na,comp1),comp2,comp3)
+ | GIf (c,(na,po),b1,b2) ->
let comp1 = Option.map f po in
let comp2 = f b1 in
let comp3 = f b2 in
- GIf (loc,f c,(na,comp1),comp2,comp3)
- | GRec (loc,fk,idl,bl,tyl,bv) ->
+ GIf (f c,(na,comp1),comp2,comp3)
+ | GRec (fk,idl,bl,tyl,bv) ->
let comp1 = Array.map (Util.List.map_left (map_glob_decl_left_to_right f)) bl in
let comp2 = Array.map f tyl in
let comp3 = Array.map f bv in
- GRec (loc,fk,idl,comp1,comp2,comp3)
- | GCast (loc,c,k) ->
+ GRec (fk,idl,comp1,comp2,comp3)
+ | GCast (c,k) ->
let comp1 = f c in
let comp2 = Miscops.map_cast_type f k in
- GCast (loc,comp1,comp2)
+ GCast (comp1,comp2)
| (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) as x -> x
+ )
let map_glob_constr = map_glob_constr_left_to_right
let fold_return_type f acc (na,tyopt) = Option.fold_left f acc tyopt
-let fold_glob_constr f acc = function
+let fold_glob_constr f acc = Loc.with_unloc (function
| GVar _ -> acc
- | GApp (_,c,args) -> List.fold_left f (f acc c) args
- | GLambda (_,_,_,b,c) | GProd (_,_,_,b,c) ->
+ | GApp (c,args) -> List.fold_left f (f acc c) args
+ | GLambda (_,_,b,c) | GProd (_,_,b,c) ->
f (f acc b) c
- | GLetIn (_,_,b,t,c) ->
+ | GLetIn (_,b,t,c) ->
f (Option.fold_left f (f acc b) t) c
- | GCases (_,_,rtntypopt,tml,pl) ->
- let fold_pattern acc (_,idl,p,c) = f acc c in
+ | GCases (_,rtntypopt,tml,pl) ->
+ let fold_pattern acc (_,(idl,p,c)) = f acc c in
List.fold_left fold_pattern
(List.fold_left f (Option.fold_left f acc rtntypopt) (List.map fst tml))
pl
- | GLetTuple (_,_,rtntyp,b,c) ->
+ | GLetTuple (_,rtntyp,b,c) ->
f (f (fold_return_type f acc rtntyp) b) c
- | GIf (_,c,rtntyp,b1,b2) ->
+ | GIf (c,rtntyp,b1,b2) ->
f (f (f (fold_return_type f acc rtntyp) c) b1) b2
- | GRec (_,_,_,bl,tyl,bv) ->
+ | GRec (_,_,bl,tyl,bv) ->
let acc = Array.fold_left
(List.fold_left (fun acc (na,k,bbd,bty) ->
f (Option.fold_left f acc bbd) bty)) acc bl in
Array.fold_left f (Array.fold_left f acc tyl) bv
- | GCast (_,c,k) ->
+ | GCast (c,k) ->
let acc = match k with
| CastConv t | CastVM t | CastNative t -> f acc t | CastCoerce -> acc in
f acc c
| (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc
+ )
let iter_glob_constr f = fold_glob_constr (fun () -> f) ()
@@ -219,25 +221,25 @@ let same_id na id = match na with
| Name id' -> Id.equal id id'
let occur_glob_constr id =
- let rec occur = function
- | GVar (loc,id') -> Id.equal id id'
- | GApp (loc,f,args) -> (occur f) || (List.exists occur args)
- | GLambda (loc,na,bk,ty,c) ->
+ let rec occur gt = Loc.with_unloc (function
+ | GVar (id') -> Id.equal id id'
+ | GApp (f,args) -> (occur f) || (List.exists occur args)
+ | GLambda (na,bk,ty,c) ->
(occur ty) || (not (same_id na id) && (occur c))
- | GProd (loc,na,bk,ty,c) ->
+ | GProd (na,bk,ty,c) ->
(occur ty) || (not (same_id na id) && (occur c))
- | GLetIn (loc,na,b,t,c) ->
+ | GLetIn (na,b,t,c) ->
(Option.fold_left (fun b t -> occur t || b) (occur b) t) || (not (same_id na id) && (occur c))
- | GCases (loc,sty,rtntypopt,tml,pl) ->
+ | GCases (sty,rtntypopt,tml,pl) ->
(occur_option rtntypopt)
|| (List.exists (fun (tm,_) -> occur tm) tml)
|| (List.exists occur_pattern pl)
- | GLetTuple (loc,nal,rtntyp,b,c) ->
+ | GLetTuple (nal,rtntyp,b,c) ->
occur_return_type rtntyp id
|| (occur b) || (not (List.mem_f Name.equal (Name id) nal) && (occur c))
- | GIf (loc,c,rtntyp,b1,b2) ->
+ | GIf (c,rtntyp,b1,b2) ->
occur_return_type rtntyp id || (occur c) || (occur b1) || (occur b2)
- | GRec (loc,fk,idl,bl,tyl,bv) ->
+ | GRec (fk,idl,bl,tyl,bv) ->
not (Array.for_all4 (fun fid bl ty bd ->
let rec occur_fix = function
[] -> not (occur ty) && (Id.equal fid id || not(occur bd))
@@ -249,11 +251,11 @@ let occur_glob_constr id =
(match na with Name id' -> Id.equal id id' | _ -> not (occur_fix bl)) in
occur_fix bl)
idl bl tyl bv)
- | GCast (loc,c,k) -> (occur c) || (match k with CastConv t
+ | GCast (c,k) -> (occur c) || (match k with CastConv t
| CastVM t | CastNative t -> occur t | CastCoerce -> false)
| (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> false
-
- and occur_pattern (loc,idl,p,c) = not (Id.List.mem id idl) && (occur c)
+ ) gt
+ and occur_pattern (loc,(idl,p,c)) = not (Id.List.mem id idl) && (occur c)
and occur_option = function None -> false | Some p -> occur p
@@ -268,33 +270,33 @@ let add_name_to_ids set na =
| Name id -> Id.Set.add id set
let free_glob_vars =
- let rec vars bounded vs = function
- | GVar (loc,id') -> if Id.Set.mem id' bounded then vs else Id.Set.add id' vs
- | GApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args)
- | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) ->
+ let rec vars bounded vs = Loc.with_unloc @@ (function
+ | GVar (id') -> if Id.Set.mem id' bounded then vs else Id.Set.add id' vs
+ | GApp (f,args) -> List.fold_left (vars bounded) vs (f::args)
+ | GLambda (na,_,ty,c) | GProd (na,_,ty,c) ->
let vs' = vars bounded vs ty in
let bounded' = add_name_to_ids bounded na in
vars bounded' vs' c
- | GLetIn (loc,na,b,ty,c) ->
+ | GLetIn (na,b,ty,c) ->
let vs' = vars bounded vs b in
let vs'' = Option.fold_left (vars bounded) vs' ty in
let bounded' = add_name_to_ids bounded na in
vars bounded' vs'' c
- | GCases (loc,sty,rtntypopt,tml,pl) ->
+ | GCases (sty,rtntypopt,tml,pl) ->
let vs1 = vars_option bounded vs rtntypopt in
let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in
List.fold_left (vars_pattern bounded) vs2 pl
- | GLetTuple (loc,nal,rtntyp,b,c) ->
+ | GLetTuple (nal,rtntyp,b,c) ->
let vs1 = vars_return_type bounded vs rtntyp in
let vs2 = vars bounded vs1 b in
let bounded' = List.fold_left add_name_to_ids bounded nal in
vars bounded' vs2 c
- | GIf (loc,c,rtntyp,b1,b2) ->
+ | GIf (c,rtntyp,b1,b2) ->
let vs1 = vars_return_type bounded vs rtntyp in
let vs2 = vars bounded vs1 c in
let vs3 = vars bounded vs2 b1 in
vars bounded vs3 b2
- | GRec (loc,fk,idl,bl,tyl,bv) ->
+ | GRec (fk,idl,bl,tyl,bv) ->
let bounded' = Array.fold_right Id.Set.add idl bounded in
let vars_fix i vs fid =
let vs1,bounded1 =
@@ -312,11 +314,12 @@ let free_glob_vars =
vars bounded1 vs2 bv.(i)
in
Array.fold_left_i vars_fix vs idl
- | GCast (loc,c,k) -> let v = vars bounded vs c in
+ | GCast (c,k) -> let v = vars bounded vs c in
(match k with CastConv t | CastVM t | CastNative t -> vars bounded v t | _ -> v)
| (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs
+ )
- and vars_pattern bounded vs (loc,idl,p,c) =
+ and vars_pattern bounded vs (loc,(idl,p,c)) =
let bounded' = List.fold_right Id.Set.add idl bounded in
vars bounded' vs c
@@ -332,7 +335,7 @@ let free_glob_vars =
let glob_visible_short_qualid c =
let rec aux acc = function
- | GRef (_,c,_) ->
+ | _, GRef (c,_) ->
let qualid = Nametab.shortest_qualid_of_global Id.Set.empty c in
let dir,id = Libnames.repr_qualid qualid in
if DirPath.is_empty dir then id :: acc else acc
@@ -351,26 +354,26 @@ let add_and_check_ident id set =
Id.Set.add id set
let bound_glob_vars =
- let rec vars bound = function
- | GLambda (_,na,_,_,_) | GProd (_,na,_,_,_) | GLetIn (_,na,_,_,_) as c ->
+ let rec vars bound = Loc.with_loc (fun ~loc -> function
+ | GLambda (na,_,_,_) | GProd (na,_,_,_) | GLetIn (na,_,_,_) as c ->
let bound = name_fold add_and_check_ident na bound in
- fold_glob_constr vars bound c
- | GCases (loc,sty,rtntypopt,tml,pl) ->
+ fold_glob_constr vars bound (loc, c)
+ | GCases (sty,rtntypopt,tml,pl) ->
let bound = vars_option bound rtntypopt in
let bound =
List.fold_left (fun bound (tm,_) -> vars bound tm) bound tml in
List.fold_left vars_pattern bound pl
- | GLetTuple (loc,nal,rtntyp,b,c) ->
+ | GLetTuple (nal,rtntyp,b,c) ->
let bound = vars_return_type bound rtntyp in
let bound = vars bound b in
let bound = List.fold_right (name_fold add_and_check_ident) nal bound in
vars bound c
- | GIf (loc,c,rtntyp,b1,b2) ->
+ | GIf (c,rtntyp,b1,b2) ->
let bound = vars_return_type bound rtntyp in
let bound = vars bound c in
let bound = vars bound b1 in
vars bound b2
- | GRec (loc,fk,idl,bl,tyl,bv) ->
+ | GRec (fk,idl,bl,tyl,bv) ->
let bound = Array.fold_right Id.Set.add idl bound in
let vars_fix i bound fid =
let bound =
@@ -388,9 +391,10 @@ let bound_glob_vars =
in
Array.fold_left_i vars_fix bound idl
| (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GVar _) -> bound
- | GApp _ | GCast _ as c -> fold_glob_constr vars bound c
+ | GApp _ | GCast _ as c -> fold_glob_constr vars bound (loc, c)
+ )
- and vars_pattern bound (loc,idl,p,c) =
+ and vars_pattern bound (loc,(idl,p,c)) =
let bound = List.fold_right add_and_check_ident idl bound in
vars bound c
@@ -435,14 +439,14 @@ let rec map_case_pattern_binders f = Loc.map (function
else PatCstr(c,rps,rna)
)
-let map_cases_branch_binders f ((loc,il,cll,rhs) as x) : cases_clause =
+let map_cases_branch_binders f ((loc,(il,cll,rhs)) as x) : cases_clause =
(* spiwack: not sure if I must do something with the list of idents.
It is intended to be a superset of the free variable of the
right-hand side, if I understand correctly. But I'm not sure when
or how they are used. *)
let r = List.smartmap (fun cl -> map_case_pattern_binders f cl) cll in
if r == cll then x
- else loc,il,r,rhs
+ else loc,(il,r,rhs)
let map_pattern_binders f tomatch branches =
CList.smartmap (fun tm -> map_tomatch_binders f tm) tomatch,
@@ -452,29 +456,14 @@ let map_pattern_binders f tomatch branches =
let map_tomatch f (c,pp) : tomatch_tuple = f c , pp
-let map_cases_branch f (loc,il,cll,rhs) : cases_clause =
- loc , il , cll , f rhs
+let map_cases_branch f (loc,(il,cll,rhs)) : cases_clause =
+ loc , (il , cll , f rhs)
let map_pattern f tomatch branches =
List.map (fun tm -> map_tomatch f tm) tomatch,
List.map (fun br -> map_cases_branch f br) branches
-let loc_of_glob_constr = function
- | GRef (loc,_,_) -> loc
- | GVar (loc,_) -> loc
- | GEvar (loc,_,_) -> loc
- | GPatVar (loc,_) -> loc
- | GApp (loc,_,_) -> loc
- | GLambda (loc,_,_,_,_) -> loc
- | GProd (loc,_,_,_,_) -> loc
- | GLetIn (loc,_,_,_,_) -> loc
- | GCases (loc,_,_,_,_) -> loc
- | GLetTuple (loc,_,_,_,_) -> loc
- | GIf (loc,_,_,_,_) -> loc
- | GRec (loc,_,_,_,_,_) -> loc
- | GSort (loc,_) -> loc
- | GHole (loc,_,_,_) -> loc
- | GCast (loc,_,_) -> loc
+let loc_of_glob_constr (loc, _) = loc
(**********************************************************************)
(* Alpha-renaming *)
@@ -506,73 +495,74 @@ let rename_var l id =
if List.exists (fun (_,id') -> Id.equal id id') l then raise UnsoundRenaming
else id
-let rec rename_glob_vars l = function
- | GVar (loc,id) as r ->
+let rec rename_glob_vars l = Loc.map_with_loc (fun ~loc -> function
+ | GVar id as r ->
let id' = rename_var l id in
- if id == id' then r else GVar (loc,id')
- | GRef (_,VarRef id,_) as r ->
+ if id == id' then r else GVar id'
+ | GRef (VarRef id,_) as r ->
if List.exists (fun (_,id') -> Id.equal id id') l then raise UnsoundRenaming
else r
- | GProd (loc,na,bk,t,c) ->
+ | GProd (na,bk,t,c) ->
let na',l' = update_subst na l in
- GProd (loc,na,bk,rename_glob_vars l t,rename_glob_vars l' c)
- | GLambda (loc,na,bk,t,c) ->
+ GProd (na,bk,rename_glob_vars l t,rename_glob_vars l' c)
+ | GLambda (na,bk,t,c) ->
let na',l' = update_subst na l in
- GLambda (loc,na',bk,rename_glob_vars l t,rename_glob_vars l' c)
- | GLetIn (loc,na,b,t,c) ->
+ GLambda (na',bk,rename_glob_vars l t,rename_glob_vars l' c)
+ | GLetIn (na,b,t,c) ->
let na',l' = update_subst na l in
- GLetIn (loc,na',rename_glob_vars l b,Option.map (rename_glob_vars l) t,rename_glob_vars l' c)
+ GLetIn (na',rename_glob_vars l b,Option.map (rename_glob_vars l) t,rename_glob_vars l' c)
(* Lazy strategy: we fail if a collision with renaming occurs, rather than renaming further *)
- | GCases (loc,ci,po,tomatchl,cls) ->
+ | GCases (ci,po,tomatchl,cls) ->
let test_pred_pat (na,ino) =
test_na l na; Option.iter (fun (_,(_,nal)) -> List.iter (test_na l) nal) ino in
let test_clause idl = List.iter (test_id l) idl in
let po = Option.map (rename_glob_vars l) po in
let tomatchl = Util.List.map_left (fun (tm,x) -> test_pred_pat x; (rename_glob_vars l tm,x)) tomatchl in
- let cls = Util.List.map_left (fun (loc,idl,p,c) -> test_clause idl; (loc,idl,p,rename_glob_vars l c)) cls in
- GCases (loc,ci,po,tomatchl,cls)
- | GLetTuple (loc,nal,(na,po),c,b) ->
+ let cls = Util.List.map_left (fun (loc,(idl,p,c)) -> test_clause idl; (loc,(idl,p,rename_glob_vars l c))) cls in
+ GCases (ci,po,tomatchl,cls)
+ | GLetTuple (nal,(na,po),c,b) ->
List.iter (test_na l) (na::nal);
- GLetTuple (loc,nal,(na,Option.map (rename_glob_vars l) po),
+ GLetTuple (nal,(na,Option.map (rename_glob_vars l) po),
rename_glob_vars l c,rename_glob_vars l b)
- | GIf (loc,c,(na,po),b1,b2) ->
+ | GIf (c,(na,po),b1,b2) ->
test_na l na;
- GIf (loc,rename_glob_vars l c,(na,Option.map (rename_glob_vars l) po),
+ GIf (rename_glob_vars l c,(na,Option.map (rename_glob_vars l) po),
rename_glob_vars l b1,rename_glob_vars l b2)
- | GRec (loc,k,idl,decls,bs,ts) ->
+ | GRec (k,idl,decls,bs,ts) ->
Array.iter (test_id l) idl;
- GRec (loc,k,idl,
+ GRec (k,idl,
Array.map (List.map (fun (na,k,bbd,bty) ->
test_na l na; (na,k,Option.map (rename_glob_vars l) bbd,rename_glob_vars l bty))) decls,
Array.map (rename_glob_vars l) bs,
Array.map (rename_glob_vars l) ts)
- | r -> map_glob_constr (rename_glob_vars l) r
+ (* XXX: This located use case should be improved. *)
+ | r -> snd @@ map_glob_constr (rename_glob_vars l) (loc, r)
+ )
(**********************************************************************)
(* Conversion from glob_constr to cases pattern, if possible *)
-let rec cases_pattern_of_glob_constr na = function
- | GVar (loc,id) ->
+let rec cases_pattern_of_glob_constr na = Loc.map (function
+ | GVar id ->
begin match na with
| Name _ ->
(* Unable to manage the presence of both an alias and a variable *)
raise Not_found
- | Anonymous -> Loc.tag ~loc @@ PatVar (Name id)
+ | Anonymous -> PatVar (Name id)
end
- | GHole (loc,_,_,_) -> Loc.tag ~loc @@ PatVar na
- | GRef (loc,ConstructRef cstr,_) ->
- Loc.tag ~loc @@ PatCstr (cstr,[],na)
- | GApp (loc,GRef (_,ConstructRef cstr,_),l) ->
- Loc.tag ~loc @@ PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na)
+ | GHole (_,_,_) -> PatVar na
+ | GRef (ConstructRef cstr,_) -> PatCstr (cstr,[],na)
+ | GApp ((_loc, GRef (ConstructRef cstr,_)),l) ->
+ PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na)
| _ -> raise Not_found
+ )
(* Turn a closed cases pattern into a glob_constr *)
-let rec glob_constr_of_closed_cases_pattern_aux x = Loc.with_loc (fun ~loc -> function
- | PatCstr (cstr,[],Anonymous) ->
- GRef (loc,ConstructRef cstr,None)
- | PatCstr (cstr,l,Anonymous) ->
- let ref = GRef (loc,ConstructRef cstr,None) in
- GApp (loc,ref, List.map glob_constr_of_closed_cases_pattern_aux l)
+let rec glob_constr_of_closed_cases_pattern_aux x = Loc.map_with_loc (fun ~loc -> function
+ | PatCstr (cstr,[],Anonymous) -> GRef (ConstructRef cstr,None)
+ | PatCstr (cstr,l,Anonymous) ->
+ let ref = Loc.tag ~loc @@ GRef (ConstructRef cstr,None) in
+ GApp (ref, List.map glob_constr_of_closed_cases_pattern_aux l)
| _ -> raise Not_found
) x
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 48ae93f3ef..6696e174bd 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -324,46 +324,46 @@ let warn_cast_in_pattern =
CWarnings.create ~name:"cast-in-pattern" ~category:"automation"
(fun () -> Pp.strbrk "Casts are ignored in patterns")
-let rec pat_of_raw metas vars = function
- | GVar (_,id) ->
+let rec pat_of_raw metas vars = Loc.with_loc (fun ~loc -> function
+ | GVar id ->
(try PRel (List.index Name.equal (Name id) vars)
with Not_found -> PVar id)
- | GPatVar (_,(false,n)) ->
+ | GPatVar (false,n) ->
metas := n::!metas; PMeta (Some n)
- | GRef (_,gr,_) ->
+ | GRef (gr,_) ->
PRef (canonical_gr gr)
(* Hack to avoid rewriting a complete interpretation of patterns *)
- | GApp (_, GPatVar (_,(true,n)), cl) ->
+ | GApp ((_, GPatVar (true,n)), cl) ->
metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl)
- | GApp (_,c,cl) ->
+ | GApp (c,cl) ->
PApp (pat_of_raw metas vars c,
Array.of_list (List.map (pat_of_raw metas vars) cl))
- | GLambda (_,na,bk,c1,c2) ->
+ | GLambda (na,bk,c1,c2) ->
name_iter (fun n -> metas := n::!metas) na;
PLambda (na, pat_of_raw metas vars c1,
pat_of_raw metas (na::vars) c2)
- | GProd (_,na,bk,c1,c2) ->
+ | GProd (na,bk,c1,c2) ->
name_iter (fun n -> metas := n::!metas) na;
PProd (na, pat_of_raw metas vars c1,
pat_of_raw metas (na::vars) c2)
- | GLetIn (_,na,c1,t,c2) ->
+ | GLetIn (na,c1,t,c2) ->
name_iter (fun n -> metas := n::!metas) na;
PLetIn (na, pat_of_raw metas vars c1,
Option.map (pat_of_raw metas vars) t,
pat_of_raw metas (na::vars) c2)
- | GSort (_,s) ->
+ | GSort s ->
PSort s
| GHole _ ->
PMeta None
- | GCast (_,c,_) ->
+ | GCast (c,_) ->
warn_cast_in_pattern ();
pat_of_raw metas vars c
- | GIf (_,c,(_,None),b1,b2) ->
+ | GIf (c,(_,None),b1,b2) ->
PIf (pat_of_raw metas vars c,
pat_of_raw metas vars b1,pat_of_raw metas vars b2)
- | GLetTuple (loc,nal,(_,None),b,c) ->
- let mkGLambda c na =
- GLambda (loc,na,Explicit,GHole (loc,Evar_kinds.InternalHole, IntroAnonymous, None),c) in
+ | GLetTuple (nal,(_,None),b,c) ->
+ let mkGLambda c na = Loc.tag ~loc @@
+ GLambda (na,Explicit, Loc.tag @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in
let c = List.fold_left mkGLambda c nal in
let cip =
{ cip_style = LetStyle;
@@ -374,9 +374,9 @@ let rec pat_of_raw metas vars = function
let tags = List.map (fun _ -> false) nal (* Approximation which can be without let-ins... *) in
PCase (cip, PMeta None, pat_of_raw metas vars b,
[0,tags,pat_of_raw metas vars c])
- | GCases (loc,sty,p,[c,(na,indnames)],brs) ->
+ | GCases (sty,p,[c,(na,indnames)],brs) ->
let get_ind = function
- | (_,_,[_, PatCstr((ind,_),_,_)],_)::_ -> Some ind
+ | (_,(_,[_, PatCstr((ind,_),_,_)],_))::_ -> Some ind
| _ -> None
in
let ind_tags,ind = match indnames with
@@ -389,7 +389,7 @@ let rec pat_of_raw metas vars = function
| Some p, Some (_,(_,nal)) ->
let nvars = na :: List.rev nal @ vars in
rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p))
- | (None | Some (GHole _)), _ -> PMeta None
+ | (None | Some (_, GHole _)), _ -> PMeta None
| Some p, None ->
user_err ~loc (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.")
in
@@ -404,7 +404,8 @@ let rec pat_of_raw metas vars = function
one non-trivial branch. These facts are used in [Constrextern]. *)
PCase (info, pred, pat_of_raw metas vars c, brs)
- | r -> err ~loc:(loc_of_glob_constr r) (Pp.str "Non supported pattern.")
+ | r -> err ~loc (Pp.str "Non supported pattern.")
+ )
and pats_of_glob_branches loc metas vars ind brs =
let get_arg = function
@@ -415,8 +416,8 @@ and pats_of_glob_branches loc metas vars ind brs =
in
let rec get_pat indexes = function
| [] -> false, []
- | [(_,_,[_, PatVar(Anonymous)],GHole _)] -> true, [] (* ends with _ => _ *)
- | (_,_,[_, PatCstr((indsp,j),lv,_)],br) :: brs ->
+ | [(_,(_,[_, PatVar(Anonymous)],(_,GHole _)))] -> true, [] (* ends with _ => _ *)
+ | (_,(_,[_, PatCstr((indsp,j),lv,_)],br)) :: brs ->
let () = match ind with
| Some sp when eq_ind sp indsp -> ()
| _ ->
@@ -431,7 +432,7 @@ and pats_of_glob_branches loc metas vars ind brs =
let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in
let tags = List.map (fun _ -> false) lv (* approximation, w/o let-in *) in
ext, ((j-1, tags, pat) :: pats)
- | (loc,_,_,_) :: _ -> err ~loc (Pp.str "Non supported pattern.")
+ | (loc,(_,_,_)) :: _ -> err ~loc (Pp.str "Non supported pattern.")
in
get_pat Int.Set.empty brs
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index ae87cd8c02..5f9f4bb08a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -567,23 +567,23 @@ let (f_genarg_interp, genarg_interp_hook) = Hook.make ()
(* in environment [env], with existential variables [evdref] and *)
(* the type constraint tycon *)
-let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdref (lvar : ltac_var_map) t =
+let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdref (lvar : ltac_var_map) (loc, t) =
let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in
let pretype_type = pretype_type k0 resolve_tc in
let pretype = pretype k0 resolve_tc in
let open Context.Rel.Declaration in
match t with
- | GRef (loc,ref,u) ->
+ | GRef (ref,u) ->
inh_conv_coerce_to_tycon loc env evdref
(pretype_ref loc evdref env ref u)
tycon
- | GVar (loc, id) ->
+ | GVar id ->
inh_conv_coerce_to_tycon loc env evdref
(pretype_id (fun e r l t -> pretype tycon e r l t) k0 loc env evdref lvar id)
tycon
- | GEvar (loc, id, inst) ->
+ | GEvar (id, inst) ->
(* 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 evk =
@@ -596,7 +596,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref c) in
inh_conv_coerce_to_tycon loc env evdref j tycon
- | GPatVar (loc,(someta,n)) ->
+ | GPatVar (someta,n) ->
let env = ltac_interp_name_env k0 lvar env !evdref in
let ty =
match tycon with
@@ -605,7 +605,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let k = Evar_kinds.MatchingVar (someta,n) in
{ uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty }
- | GHole (loc, k, naming, None) ->
+ | GHole (k, naming, None) ->
let env = ltac_interp_name_env k0 lvar env !evdref in
let ty =
match tycon with
@@ -614,7 +614,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
new_type_evar env evdref loc in
{ uj_val = e_new_evar env evdref ~src:(loc,k) ~naming ty; uj_type = ty }
- | GHole (loc, k, _naming, Some arg) ->
+ | GHole (k, _naming, Some arg) ->
let env = ltac_interp_name_env k0 lvar env !evdref in
let ty =
match tycon with
@@ -626,7 +626,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let () = evdref := sigma in
{ uj_val = c; uj_type = ty }
- | GRec (loc,fixkind,names,bl,lar,vdef) ->
+ | GRec (fixkind,names,bl,lar,vdef) ->
let rec type_bl env ctxt = function
[] -> ctxt
| (na,bk,None,ty)::bl ->
@@ -711,11 +711,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
in
inh_conv_coerce_to_tycon loc env evdref fixj tycon
- | GSort (loc,s) ->
+ | GSort s ->
let j = pretype_sort loc evdref s in
inh_conv_coerce_to_tycon loc env evdref j tycon
- | GApp (loc,f,args) ->
+ | GApp (f,args) ->
let fj = pretype empty_tycon env evdref lvar f in
let floc = loc_of_glob_constr f in
let length = List.length args in
@@ -794,7 +794,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
in
inh_conv_coerce_to_tycon loc env evdref resj tycon
- | GLambda(loc,name,bk,c1,c2) ->
+ | GLambda(name,bk,c1,c2) ->
let tycon' = evd_comb1
(fun evd tycon ->
match tycon with
@@ -816,7 +816,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let resj = judge_of_abstraction env.ExtraEnv.env (orelse_name name name') j j' in
inh_conv_coerce_to_tycon loc env evdref resj tycon
- | GProd(loc,name,bk,c1,c2) ->
+ | GProd(name,bk,c1,c2) ->
let j = pretype_type empty_valcon env evdref lvar c1 in
(* The name specified by ltac is used also to create bindings. So
the substitution must also be applied on variables before they are
@@ -840,7 +840,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
iraise (e, info) in
inh_conv_coerce_to_tycon loc env evdref resj tycon
- | GLetIn(loc,name,c1,t,c2) ->
+ | GLetIn(name,c1,t,c2) ->
let tycon1 =
match t with
| Some t ->
@@ -861,7 +861,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
{ uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
uj_type = subst1 j.uj_val j'.uj_type }
- | GLetTuple (loc,nal,(na,po),c,d) ->
+ | GLetTuple (nal,(na,po),c,d) ->
let cj = pretype empty_tycon env evdref lvar c in
let (IndType (indf,realargs)) =
try find_rectype env.ExtraEnv.env !evdref cj.uj_type
@@ -954,7 +954,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
obj ind p cj.uj_val fj.uj_val
in { uj_val = v; uj_type = ccl })
- | GIf (loc,c,(na,po),b1,b2) ->
+ | GIf (c,(na,po),b1,b2) ->
let cj = pretype empty_tycon env evdref lvar c in
let (IndType (indf,realargs)) =
try find_rectype env.ExtraEnv.env !evdref cj.uj_type
@@ -1022,12 +1022,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let cj = { uj_val = v; uj_type = p } in
inh_conv_coerce_to_tycon loc env evdref cj tycon
- | GCases (loc,sty,po,tml,eqns) ->
+ | GCases (sty,po,tml,eqns) ->
Cases.compile_cases loc sty
((fun vtyc env evdref -> pretype vtyc (make_env env !evdref) evdref lvar),evdref)
tycon env.ExtraEnv.env (* loc *) (po,tml,eqns)
- | GCast (loc,c,k) ->
+ | GCast (c,k) ->
let cj =
match k with
| CastCoerce ->
@@ -1097,7 +1097,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
(* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
- | GHole (loc, knd, naming, None) ->
+ | loc, GHole (knd, naming, None) ->
let rec is_Type c = match EConstr.kind !evdref c with
| Sort s ->
begin match ESorts.kind !evdref s with
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:04:35 +0000