aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrextern.ml5
-rw-r--r--interp/constrintern.ml2
-rw-r--r--interp/reserve.ml2
-rw-r--r--parsing/termast.ml5
-rw-r--r--pretyping/pattern.ml6
-rw-r--r--pretyping/pattern.mli2
-rw-r--r--pretyping/pretyping.ml6
-rw-r--r--pretyping/rawterm.ml6
-rw-r--r--pretyping/rawterm.mli2
9 files changed, 17 insertions, 19 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 337c888a4..64aedf741 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1331,7 +1331,7 @@ let rec extern inctx scopes vars r =
| RVar (loc,id) -> CRef (Ident (loc,v7_to_v8_id id))
- | REvar (loc,n) -> extern_evar loc n
+ | REvar (loc,n,_) -> (* we drop args *) extern_evar loc n
| RPatVar (loc,n) -> if !print_meta_as_hole then CHole loc else CPatVar (loc,n)
@@ -1342,7 +1342,6 @@ let rec extern inctx scopes vars r =
else
(f,args) in
(match f with
- | REvar (loc,ev) -> extern_evar loc ev (* we drop args *)
| RRef (rloc,ref) ->
let subscopes = Symbols.find_arguments_scope ref in
let args =
@@ -1558,7 +1557,7 @@ let extern_constr at_top env t =
let rec raw_of_pat tenv env = function
| PRef ref -> RRef (loc,ref)
| PVar id -> RVar (loc,id)
- | PEvar n -> REvar (loc,n)
+ | PEvar (n,l) -> REvar (loc,n,Some (array_map_to_list (raw_of_pat tenv env) l))
| PRel n ->
let id = try match lookup_name_of_rel n env with
| Name id -> id
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 0f68f0314..84be73849 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -699,7 +699,7 @@ let internalise sigma env allow_soapp lvar c =
| CPatVar (loc, _) ->
raise (InternalisationError (loc,NegativeMetavariable))
| CEvar (loc, n) ->
- REvar (loc, n)
+ REvar (loc, n, None)
| CSort (loc, s) ->
RSort(loc,s)
| CCast (loc, c1, c2) ->
diff --git a/interp/reserve.ml b/interp/reserve.ml
index dc7393c67..8b759b6aa 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -62,7 +62,7 @@ let rec unloc = function
| RSort (_,x) -> RSort (dummy_loc,x)
| RHole (_,x) -> RHole (dummy_loc,x)
| RRef (_,x) -> RRef (dummy_loc,x)
- | REvar (_,x) -> REvar (dummy_loc,x)
+ | REvar (_,x,l) -> REvar (dummy_loc,x,l)
| RPatVar (_,x) -> RPatVar (dummy_loc,x)
| RDynamic (_,x) -> RDynamic (dummy_loc,x)
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 3174898c4..0e8b84f74 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -194,7 +194,7 @@ let ast_of_app impl f args =
let rec ast_of_raw = function
| RRef (_,ref) -> ast_of_ref ref
| RVar (_,id) -> ast_of_ident id
- | REvar (_,n) -> ast_of_existential_ref n
+ | REvar (_,n,_) -> (* we drop args *) ast_of_existential_ref n
| RPatVar (_,(_,n)) -> ope("META",[ast_of_ident n])
| RApp (_,f,args) ->
let (f,args) =
@@ -202,7 +202,6 @@ let rec ast_of_raw = function
let astf = ast_of_raw f in
let astargs = List.map ast_of_raw args in
(match f with
- | REvar (_,ev) -> ast_of_existential_ref ev (* we drop args *)
| RRef (_,ref) -> ast_of_app (implicits_of_global ref) astf astargs
| _ -> ast_of_app [] astf astargs)
@@ -368,7 +367,7 @@ let rec ast_of_pattern tenv env = function
| PVar id -> ast_of_ident id
- | PEvar n -> ast_of_existential_ref n
+ | PEvar (n,_) -> ast_of_existential_ref n
| PRel n ->
(try match lookup_name_of_rel n env with
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index f453e911e..f5c3b2c03 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -34,7 +34,7 @@ let patvar_of_int_v7 n = Names.id_of_string ("?" ^ string_of_int n)
type constr_pattern =
| PRef of global_reference
| PVar of identifier
- | PEvar of existential_key
+ | PEvar of existential_key * constr_pattern array
| PRel of int
| PApp of constr_pattern * constr_pattern array
| PSoApp of patvar * constr_pattern list
@@ -176,9 +176,7 @@ let rec pattern_of_constr t =
| Const sp -> PRef (ConstRef sp)
| Ind sp -> PRef (IndRef sp)
| Construct sp -> PRef (ConstructRef sp)
- | Evar (n,ctxt) ->
- if ctxt = [||] then PEvar n
- else PApp (PEvar n, Array.map pattern_of_constr ctxt)
+ | Evar (n,ctxt) -> PEvar (n,Array.map pattern_of_constr ctxt)
| Case (ci,p,a,br) ->
PCase ((Some ci.ci_ind,ci.ci_pp_info.style),
Some (pattern_of_constr p),pattern_of_constr a,
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index f05a08659..7a3b9127d 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -33,7 +33,7 @@ val patvar_of_int_v7 : int -> patvar
type constr_pattern =
| PRef of global_reference
| PVar of identifier
- | PEvar of existential_key
+ | PEvar of existential_key * constr_pattern array
| PRel of int
| PApp of constr_pattern * constr_pattern array
| PSoApp of patvar * constr_pattern list
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e8965659e..f8fcc9b9e 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -223,11 +223,13 @@ let rec pretype tycon env isevars lvar = function
(pretype_id loc env lvar id)
tycon
- | REvar (loc, ev) ->
+ | REvar (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 = (Evd.map (evars_of isevars) ev).evar_hyps in
- let args = instance_from_named_context hyps in
+ let args = match instopt with
+ | None -> instance_from_named_context hyps
+ | Some inst -> failwith "Evar subtitutions not implemented" in
let c = mkEvar (ev, args) in
let j = (Retyping.get_judgment_of env (evars_of isevars) c) in
inh_conv_coerce_to_tycon loc env isevars j tycon
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index f11caa566..78425e107 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -61,7 +61,7 @@ type hole_kind =
type rawconstr =
| RRef of (loc * global_reference)
| RVar of (loc * identifier)
- | REvar of loc * existential_key
+ | REvar of loc * existential_key * rawconstr list option
| RPatVar of loc * (bool * patvar) (* Used for patterns only *)
| RApp of loc * rawconstr * rawconstr list
| RLambda of loc * name * rawconstr * rawconstr
@@ -153,7 +153,7 @@ let map_rawconstr_with_binders_loc loc g f e = function
| RSort (_,x) -> RSort (loc,x)
| RHole (_,x) -> RHole (loc,x)
| RRef (_,x) -> RRef (loc,x)
- | REvar (_,x) -> REvar (loc,x)
+ | REvar (_,x,l) -> REvar (loc,x,l)
| RPatVar (_,x) -> RPatVar (loc,x)
| RDynamic (_,x) -> RDynamic (loc,x)
*)
@@ -300,7 +300,7 @@ let rec subst_raw subst raw =
let loc_of_rawconstr = function
| RRef (loc,_) -> loc
| RVar (loc,_) -> loc
- | REvar (loc,_) -> loc
+ | REvar (loc,_,_) -> loc
| RPatVar (loc,_) -> loc
| RApp (loc,_,_) -> loc
| RLambda (loc,_,_,_) -> loc
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 993b7e84a..651530c94 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -59,7 +59,7 @@ type hole_kind =
type rawconstr =
| RRef of (loc * global_reference)
| RVar of (loc * identifier)
- | REvar of loc * existential_key
+ | REvar of loc * existential_key * rawconstr list option
| RPatVar of loc * (bool * patvar) (* Used for patterns only *)
| RApp of loc * rawconstr * rawconstr list
| RLambda of loc * name * rawconstr * rawconstr
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 18:33:49 +0000