aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrextern.ml12
-rw-r--r--interp/constrintern.ml4
-rw-r--r--intf/evar_kinds.mli5
-rw-r--r--intf/glob_term.mli2
-rw-r--r--pretyping/glob_ops.ml9
-rw-r--r--pretyping/patternops.ml11
-rw-r--r--pretyping/pretyping.ml4
-rw-r--r--tactics/hipattern.ml2
8 files changed, 19 insertions, 30 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index bdbfd8c27..59b8b4e5b 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -654,11 +654,9 @@ let rec extern inctx scopes vars r =
| GEvar (loc,n,l) ->
extern_evar loc n (List.map (on_snd (extern false scopes vars)) l)
- | GPatVar (loc,kind) ->
- if !print_meta_as_hole then CHole (loc, None, Misctypes.IntroAnonymous, None) else
- (match kind with
- | Evar_kinds.SecondOrderPatVar n -> CPatVar (loc,n)
- | Evar_kinds.FirstOrderPatVar n -> CEvar (loc,n,[]))
+ | GPatVar (loc,(b,n)) ->
+ if !print_meta_as_hole then CHole (loc, None, Misctypes.IntroAnonymous, None) else
+ if b then CPatVar (loc,n) else CEvar (loc,n,[])
| GApp (loc,f,args) ->
(match f with
@@ -1031,13 +1029,13 @@ let rec glob_of_pat env sigma = function
with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in
GVar (loc,id)
| PMeta None -> GHole (loc,Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None)
- | PMeta (Some n) -> GPatVar (loc,Evar_kinds.FirstOrderPatVar n)
+ | PMeta (Some n) -> GPatVar (loc,(false,n))
| PProj (p,c) -> GApp (loc,GRef (loc, ConstRef (Projection.constant p),None),
[glob_of_pat env sigma c])
| PApp (f,args) ->
GApp (loc,glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args)
| PSoApp (n,args) ->
- GApp (loc,GPatVar (loc,Evar_kinds.SecondOrderPatVar n),
+ GApp (loc,GPatVar (loc,(true,n)),
List.map (glob_of_pat env sigma) args)
| PProd (na,t,c) ->
GProd (loc,na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ea1802ccf..94924374a 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1748,9 +1748,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
GHole (loc, k, naming, solve)
(* Parsing pattern variables *)
| CPatVar (loc, n) when pattern_mode ->
- GPatVar (loc, Evar_kinds.SecondOrderPatVar n)
+ GPatVar (loc, (true,n))
| CEvar (loc, n, []) when pattern_mode ->
- GPatVar (loc, Evar_kinds.FirstOrderPatVar n)
+ GPatVar (loc, (false,n))
(* end *)
(* Parsing existential variables *)
| CEvar (loc, n, l) ->
diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli
index 75dad2e91..470ad2a23 100644
--- a/intf/evar_kinds.mli
+++ b/intf/evar_kinds.mli
@@ -8,7 +8,6 @@
open Names
open Globnames
-open Misctypes
(** The kinds of existential variable *)
@@ -17,8 +16,6 @@ open Misctypes
type obligation_definition_status = Define of bool | Expand
-type matching_var_kind = FirstOrderPatVar of patvar | SecondOrderPatVar of patvar
-
type t =
| ImplicitArg of global_reference * (int * Id.t option)
* bool (** Force inference *)
@@ -30,6 +27,6 @@ type t =
| TomatchTypeParameter of inductive * int
| GoalEvar
| ImpossibleCase
- | MatchingVar of matching_var_kind
+ | MatchingVar of bool * Id.t
| VarInstance of Id.t
| SubEvar of Constr.existential_key
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index ba4a47a36..ced5a8b44 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -38,7 +38,7 @@ type glob_constr =
(** An identifier that cannot be regarded as "GRef".
Bound variables are typically represented this way. *)
| GEvar of Loc.t * existential_name * (Id.t * glob_constr) list
- | GPatVar of Loc.t * Evar_kinds.matching_var_kind (** Used for patterns only *)
+ | GPatVar of Loc.t * (bool * patvar) (** Used for patterns only *)
| GApp of Loc.t * glob_constr * glob_constr list
| GLambda of Loc.t * Name.t * binding_kind * glob_constr * glob_constr
| GProd of Loc.t * Name.t * binding_kind * glob_constr * glob_constr
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 7fb539fb5..ebbfa195f 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -12,7 +12,6 @@ open Nameops
open Globnames
open Misctypes
open Glob_term
-open Evar_kinds
(* Untyped intermediate terms, after ASTs and before constr. *)
@@ -62,18 +61,14 @@ let cast_type_eq eq t1 t2 = match t1, t2 with
| CastNative t1, CastNative t2 -> eq t1 t2
| _ -> false
-let matching_var_kind_eq k1 k2 = match k1, k2 with
-| FirstOrderPatVar ido1, FirstOrderPatVar ido2 -> Id.equal ido1 ido2
-| SecondOrderPatVar id1, SecondOrderPatVar id2 -> Id.equal id1 id2
-| _ -> 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) ->
Id.equal id1 id2 &&
List.equal instance_eq arg1 arg2
-| GPatVar (_, k1), GPatVar (_, k2) -> matching_var_kind_eq k1 k2
+| GPatVar (_, (b1, pat1)), GPatVar (_, (b2, pat2)) ->
+ (b1 : bool) == b2 && Id.equal pat1 pat2
| 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) ->
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index b310da9a3..b16d04495 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -145,7 +145,7 @@ let pattern_of_constr env sigma t =
match kind_of_term f with
| Evar (evk,args) ->
(match snd (Evd.evar_source evk sigma) with
- Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar id) -> Some id
+ Evar_kinds.MatchingVar (true,id) -> Some id
| _ -> None)
| _ -> None
with
@@ -158,11 +158,10 @@ let pattern_of_constr env sigma t =
pattern_of_constr env (EConstr.Unsafe.to_constr (Retyping.expand_projection env sigma p (EConstr.of_constr c) []))
| Evar (evk,ctxt) ->
(match snd (Evd.evar_source evk sigma) with
- | Evar_kinds.MatchingVar (Evar_kinds.FirstOrderPatVar id) ->
- PMeta (Some id)
+ | Evar_kinds.MatchingVar (b,id) ->
+ assert (not b); PMeta (Some id)
| Evar_kinds.GoalEvar ->
PEvar (evk,Array.map (pattern_of_constr env) ctxt)
- | Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false
| _ ->
PMeta None)
| Case (ci,p,a,br) ->
@@ -329,12 +328,12 @@ let rec pat_of_raw metas vars = function
| GVar (_,id) ->
(try PRel (List.index Name.equal (Name id) vars)
with Not_found -> PVar id)
- | GPatVar (_,Evar_kinds.FirstOrderPatVar n) ->
+ | GPatVar (_,(false,n)) ->
metas := n::!metas; PMeta (Some n)
| GRef (_,gr,_) ->
PRef (canonical_gr gr)
(* Hack to avoid rewriting a complete interpretation of patterns *)
- | GApp (_, GPatVar (_,Evar_kinds.SecondOrderPatVar n), cl) ->
+ | GApp (_, GPatVar (_,(true,n)), cl) ->
metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl)
| GApp (_,c,cl) ->
PApp (pat_of_raw metas vars c,
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 6c490045c..ae87cd8c0 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -596,13 +596,13 @@ 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,kind) ->
+ | GPatVar (loc,(someta,n)) ->
let env = ltac_interp_name_env k0 lvar env !evdref in
let ty =
match tycon with
| Some ty -> ty
| None -> new_type_evar env evdref loc in
- let k = Evar_kinds.MatchingVar kind in
+ 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) ->
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 257c092d7..851554b83 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -261,7 +261,7 @@ let mkGProd id c1 c2 =
let mkGArrow c1 c2 =
GProd (Loc.ghost, Anonymous, Explicit, c1, c2)
let mkGVar id = GVar (Loc.ghost, Id.of_string id)
-let mkGPatVar id = GPatVar(Loc.ghost, Evar_kinds.FirstOrderPatVar (Id.of_string id))
+let mkGPatVar id = GPatVar(Loc.ghost, (false, Id.of_string id))
let mkGRef r = GRef (Loc.ghost, Lazy.force r, None)
let mkGAppRef r args = mkGApp (mkGRef r) args
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 20:45:52 +0000