aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--dev/top_printers.ml4
-rw-r--r--interp/constrextern.ml3
-rw-r--r--interp/constrintern.ml58
-rw-r--r--interp/notation.ml2
-rw-r--r--kernel/cbytegen.ml5
-rw-r--r--kernel/closure.ml19
-rw-r--r--kernel/closure.mli7
-rw-r--r--kernel/constr.ml14
-rw-r--r--kernel/constr.mli4
-rw-r--r--kernel/cooking.ml7
-rw-r--r--kernel/environ.ml2
-rw-r--r--kernel/indtypes.ml5
-rw-r--r--kernel/mod_subst.ml12
-rw-r--r--kernel/names.ml28
-rw-r--r--kernel/names.mli20
-rw-r--r--kernel/nativecode.ml3
-rw-r--r--kernel/nativelambda.ml3
-rw-r--r--kernel/reduction.ml16
-rw-r--r--kernel/term.ml2
-rw-r--r--kernel/term.mli4
-rw-r--r--kernel/typeops.ml3
-rw-r--r--kernel/vconv.ml4
-rw-r--r--library/heads.ml2
-rw-r--r--library/universes.ml4
-rw-r--r--plugins/cc/ccalgo.ml15
-rw-r--r--plugins/cc/cctac.ml5
-rw-r--r--plugins/extraction/extraction.ml2
-rw-r--r--plugins/quote/quote.ml4
-rw-r--r--pretyping/cases.ml3
-rw-r--r--pretyping/cbv.ml2
-rw-r--r--pretyping/classops.ml7
-rw-r--r--pretyping/classops.mli2
-rw-r--r--pretyping/coercion.ml2
-rw-r--r--pretyping/constrMatching.ml10
-rw-r--r--pretyping/detyping.ml20
-rw-r--r--pretyping/evarconv.ml33
-rw-r--r--pretyping/indrec.ml5
-rw-r--r--pretyping/namegen.ml4
-rw-r--r--pretyping/nativenorm.ml4
-rw-r--r--pretyping/patternops.ml17
-rw-r--r--pretyping/patternops.mli4
-rw-r--r--pretyping/pretyping.ml4
-rw-r--r--pretyping/reductionops.ml28
-rw-r--r--pretyping/reductionops.mli2
-rw-r--r--pretyping/retyping.ml2
-rw-r--r--pretyping/tacred.ml54
-rw-r--r--pretyping/termops.ml2
-rw-r--r--pretyping/unification.ml41
-rw-r--r--tactics/auto.ml8
-rw-r--r--tactics/btermdn.ml4
-rw-r--r--tactics/tacinterp.ml4
-rw-r--r--tactics/tactics.ml6
-rw-r--r--tactics/term_dnet.ml2
-rw-r--r--test-suite/bugs/opened/3660.v6
-rw-r--r--toplevel/record.ml2
55 files changed, 317 insertions, 218 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 6bf294967..2cbac2175 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -239,7 +239,7 @@ let constr_display csr =
| Construct (((sp,i),j),u) ->
"MutConstruct(("^(string_of_mind sp)^","^(string_of_int i)^"),"
^","^(universes_display u)^(string_of_int j)^")"
- | Proj (p, c) -> "Proj("^(string_of_con p)^","^term_display c ^")"
+ | Proj (p, c) -> "Proj("^(string_of_con (Projection.constant p))^","^term_display c ^")"
| Case (ci,p,c,bl) ->
"MutCase(<abs>,"^(term_display p)^","^(term_display c)^","
^(array_display bl)^")"
@@ -328,7 +328,7 @@ let print_pure_constr csr =
print_string ","; universes_display u;
print_string ")"
| Proj (p,c') -> print_string "Proj(";
- sp_con_display p;
+ sp_con_display (Projection.constant p);
print_string ",";
box_display c';
print_string ")"
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 885b0e6b4..63461c11a 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -983,7 +983,8 @@ let rec glob_of_pat env sigma = function
GVar (loc,id)
| PMeta None -> GHole (loc,Evar_kinds.InternalHole, None)
| PMeta (Some n) -> GPatVar (loc,(false,n))
- | PProj (p,c) -> GApp (loc,GRef (loc, ConstRef p,None),[glob_of_pat env sigma c])
+ | 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) ->
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 56780e240..6b3de2621 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -684,14 +684,6 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
(* [id] a goal variable *)
GVar (loc,id), [], [], []
-let is_projection_ref = function
- | ConstRef r ->
- if Environ.is_projection r (Global.env ()) then
- let pb = Environ.lookup_projection r (Global.env ()) in
- Some (r, pb.Declarations.proj_npars)
- else None
- | _ -> None
-
let proj_impls r impls =
let env = Global.env () in
let f (x, l) = x, projection_implicits env r l in
@@ -710,17 +702,15 @@ let find_appl_head_data c =
| GRef (loc,ref,_) as x ->
let impls = implicits_of_global ref in
let scopes = find_arguments_scope ref in
- let isproj = is_projection_ref ref in
- x, isproj, impls, scopes, []
+ x, impls, scopes, []
| GApp (_,GRef (_,ref,_),l) as x
when l != [] && Flags.version_strictly_greater Flags.V8_2 ->
let n = List.length l in
let impls = implicits_of_global ref in
let scopes = find_arguments_scope ref in
- let isproj = is_projection_ref ref in
- x, isproj, List.map (drop_first_implicits n) impls,
+ x, List.map (drop_first_implicits n) impls,
List.skipn_at_least n scopes,[]
- | x -> x,None,[],[],[]
+ | x -> x,[],[],[]
let error_not_enough_arguments loc =
user_err_loc (loc,"",str "Abbreviation is not applied enough.")
@@ -777,26 +767,24 @@ let intern_applied_reference intern env namedctx lvar us args = function
try intern_qualid loc qid intern env lvar us args
with Not_found -> error_global_not_found_loc loc qid
in
- let x, isproj, imp, scopes, l = find_appl_head_data r in
- let isproj = if projapp then isproj else None in
- (x,imp,scopes,l), isproj, args2
+ let x, imp, scopes, l = find_appl_head_data r in
+ (x,imp,scopes,l), args2
| Ident (loc, id) ->
- try intern_var env lvar namedctx loc id, None, args
+ try intern_var env lvar namedctx loc id, args
with Not_found ->
let qid = qualid_of_ident id in
try
let r, projapp, args2 = intern_non_secvar_qualid loc qid intern env lvar us args in
- let x, isproj, imp, scopes, l = find_appl_head_data r in
- let isproj = if projapp then isproj else None in
- (x,imp,scopes,l), isproj, args2
+ let x, imp, scopes, l = find_appl_head_data r in
+ (x,imp,scopes,l), args2
with Not_found ->
(* Extra allowance for non globalizing functions *)
if !interning_grammar || env.unb then
- (GVar (loc,id), [], [], []), None, args
+ (GVar (loc,id), [], [], []), args
else error_global_not_found_loc loc qid
let interp_reference vars r =
- let (r,_,_,_),_,_ =
+ let (r,_,_,_),_ =
intern_applied_reference (fun _ -> error_not_enough_arguments Loc.ghost)
{ids = Id.Set.empty; unb = false ;
tmp_scope = None; scopes = []; impls = empty_internalization_env} []
@@ -1358,11 +1346,11 @@ let extract_explicit_arg imps args =
let internalize globalenv env allow_patvar lvar c =
let rec intern env = function
| CRef (ref,us) as x ->
- let (c,imp,subscopes,l),isproj,_ =
+ let (c,imp,subscopes,l),_ =
intern_applied_reference intern env (Environ.named_context globalenv)
lvar us [] ref
in
- apply_impargs (None, isproj) c env imp subscopes l (constr_loc x)
+ apply_impargs c env imp subscopes l (constr_loc x)
| CFix (loc, (locid,iddef), dl) ->
let lf = List.map (fun ((_, id),_,_,_,_) -> id) dl in
@@ -1457,7 +1445,7 @@ let internalize globalenv env allow_patvar lvar c =
intern {env with tmp_scope = None;
scopes = find_delimiters_scope loc key :: env.scopes} e
| CAppExpl (loc, (isproj,ref,us), args) ->
- let (f,_,args_scopes,_),isprojf,args =
+ let (f,_,args_scopes,_),args =
let args = List.map (fun a -> (a,None)) args in
intern_applied_reference intern env (Environ.named_context globalenv)
lvar us args ref
@@ -1466,23 +1454,23 @@ let internalize globalenv env allow_patvar lvar c =
GApp (loc, f, intern_args env args_scopes (List.map fst args))
| CApp (loc, (isproj,f), args) ->
- let isproj,f,args = match f with
+ let f,args = match f with
(* Compact notations like "t.(f args') args" *)
- | CApp (_,(Some _ as isproj',f), args') when not (Option.has_some isproj) ->
- isproj',f,args'@args
+ | CApp (_,(Some _,f), args') when not (Option.has_some isproj) ->
+ f,args'@args
(* Don't compact "(f args') args" to resolve implicits separately *)
- | _ -> isproj,f,args in
- let (c,impargs,args_scopes,l),isprojf,args =
+ | _ -> f,args in
+ let (c,impargs,args_scopes,l),args =
match f with
| CRef (ref,us) ->
intern_applied_reference intern env
(Environ.named_context globalenv) lvar us args ref
| CNotation (loc,ntn,([],[],[])) ->
let c = intern_notation intern env lvar loc ntn ([],[],[]) in
- let x, isproj, impl, scopes, l = find_appl_head_data c in
- (x,impl,scopes,l), None, args
- | x -> (intern env f,[],[],[]), None, args in
- apply_impargs (isproj,isprojf) c env impargs args_scopes
+ let x, impl, scopes, l = find_appl_head_data c in
+ (x,impl,scopes,l), args
+ | x -> (intern env f,[],[],[]), args in
+ apply_impargs c env impargs args_scopes
(merge_impargs l args) loc
| CRecord (loc, _, fs) ->
@@ -1719,7 +1707,7 @@ let internalize globalenv env allow_patvar lvar c =
intern_args env subscopes rargs
in aux 1 l subscopes eargs rargs
- and apply_impargs (isproj,isprojf) c env imp subscopes l loc =
+ and apply_impargs c env imp subscopes l loc =
let imp = select_impargs_size (List.length l) imp in
let l = intern_impargs c env imp subscopes l in
smart_gapp c loc l
diff --git a/interp/notation.ml b/interp/notation.ml
index 6cc99ddb4..e765701d4 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -535,7 +535,7 @@ let compute_scope_class t =
let t', _ = decompose_appvect (Reductionops.whd_betaiotazeta Evd.empty t) in
match kind_of_term t' with
| Var _ | Const _ | Ind _ -> ScopeRef (global_of_constr t')
- | Proj (p, c) -> ScopeRef (ConstRef p)
+ | Proj (p, c) -> ScopeRef (ConstRef (Projection.constant p))
| Sort _ -> ScopeSort
| _ -> raise Not_found
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 36a022fd9..6fd1c689f 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -501,11 +501,12 @@ let rec compile_constr reloc c sz cont =
| Evar _ -> invalid_arg "Cbytegen.compile_constr : Evar"
| Proj (p,c) ->
(* compile_const reloc p [|c|] sz cont *)
- let cb = lookup_constant p !global_env in
+ let kn = Projection.constant p in
+ let cb = lookup_constant kn !global_env in
(* TODO: better representation of projections *)
let pb = Option.get cb.const_proj in
let args = Array.make pb.proj_npars mkProp in
- compile_const reloc p Univ.Instance.empty (Array.append args [|c|]) sz cont
+ compile_const reloc kn Univ.Instance.empty (Array.append args [|c|]) sz cont
| Cast(c,_,_) -> compile_constr reloc c sz cont
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 14afcc4db..23861347a 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -88,6 +88,7 @@ module type RedFlagsSig = sig
val red_add_transparent : reds -> transparent_state -> reds
val mkflags : red_kind list -> reds
val red_set : reds -> red_kind -> bool
+ val red_projection : reds -> projection -> bool
end
module RedFlags = (struct
@@ -168,6 +169,10 @@ module RedFlags = (struct
| DELTA -> (* Used for Rel/Var defined in context *)
incr_cnt red.r_delta delta
+ let red_projection red p =
+ if Projection.unfolded p then true
+ else red_set red (fCONST (Projection.constant p))
+
end : RedFlagsSig)
open RedFlags
@@ -338,7 +343,7 @@ and fterm =
| FInd of pinductive
| FConstruct of pconstructor
| FApp of fconstr * fconstr array
- | FProj of constant * fconstr
+ | FProj of projection * fconstr
| FFix of fixpoint * fconstr subs
| FCoFix of cofixpoint * fconstr subs
| FCases of case_info * fconstr * fconstr * fconstr array
@@ -708,7 +713,7 @@ let rec zip m stk rem = match stk with
let t = FCases(ci, p, m, br) in
zip {norm=neutr m.norm; term=t} s rem
| Zproj (i,j,cst) :: s ->
- zip {norm=neutr m.norm; term=FProj (cst,m)} s rem
+ zip {norm=neutr m.norm; term=FProj (Projection.make cst true,m)} s rem
| Zfix(fx,par)::s ->
zip fx par ((Zapp [|m|] :: s) :: rem)
| Zshift(n)::s ->
@@ -876,7 +881,7 @@ let eta_expand_ind_stack env ind m s (f, s') =
(** Try to drop the params, might fail on partially applied constructors. *)
let argss = try_drop_parameters depth pars args in
let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
- term = FProj (p, right) }) projs in
+ term = FProj (Projection.make p true, right) }) projs in
argss, [Zapp hstack]
| _ -> raise Not_found (* disallow eta-exp for non-primitive records *)
@@ -932,11 +937,13 @@ let rec knh info m stk =
| (None, stk') -> (m,stk'))
| FCast(t,_,_) -> knh info t stk
| FProj (p,c) ->
- if red_set info.i_flags (fCONST p) then
+ let unf = Projection.unfolded p in
+ if unf || red_set info.i_flags (fCONST (Projection.constant p)) then
(match try Some (lookup_projection p (info_env info)) with Not_found -> None with
| None -> (m, stk)
| Some pb ->
- knh info c (Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p)
+ knh info c (Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg,
+ Projection.constant p)
:: zupdate m stk))
else (m,stk)
@@ -1033,7 +1040,7 @@ let rec zip_term zfun m stk =
let t = mkCase(ci, zfun p, m, Array.map zfun br) in
zip_term zfun t s
| Zproj(_,_,p)::s ->
- let t = mkProj (p, m) in
+ let t = mkProj (Projection.make p true, m) in
zip_term zfun t s
| Zfix(fx,par)::s ->
let h = mkApp(zip_term zfun (zfun fx) par,[|m|]) in
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 1062d0e61..445fcb7bc 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -64,7 +64,10 @@ module type RedFlagsSig = sig
(** Tests if a reduction kind is set *)
val red_set : reds -> red_kind -> bool
-
+
+ (** This tests if the projection is in unfolded state already or
+ is unfodable due to delta. *)
+ val red_projection : reds -> projection -> bool
end
module RedFlags : RedFlagsSig
@@ -113,7 +116,7 @@ type fterm =
| FInd of inductive puniverses
| FConstruct of constructor puniverses
| FApp of fconstr * fconstr array
- | FProj of constant * fconstr
+ | FProj of projection * fconstr
| FFix of fixpoint * fconstr subs
| FCoFix of cofixpoint * fconstr subs
| FCases of case_info * fconstr * fconstr * fconstr array
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 2a13f938b..912067629 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -85,7 +85,7 @@ type ('constr, 'types) kind_of_term =
| Case of case_info * 'constr * 'constr * 'constr array
| Fix of ('constr, 'types) pfixpoint
| CoFix of ('constr, 'types) pcofixpoint
- | Proj of constant * 'constr
+ | Proj of projection * 'constr
(* constr is the fixpoint of the previous type. Requires option
-rectypes of the Caml compiler to be set *)
type t = (t,t) kind_of_term
@@ -486,7 +486,7 @@ let compare_head_gen eq_universes eq_sorts f t1 t2 =
Int.equal (Array.length l1) (Array.length l2) &&
f c1 c2 && Array.equal f l1 l2
| Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal f l1 l2
- | Proj (p1,c1), Proj (p2,c2) -> eq_constant p1 p2 && f c1 c2
+ | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && f c1 c2
| Const (c1,u1), Const (c2,u2) -> eq_constant c1 c2 && eq_universes true u1 u2
| Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && eq_universes false u1 u2
| Construct (c1,u1), Construct (c2,u2) -> eq_constructor c1 c2 && eq_universes false u1 u2
@@ -523,7 +523,7 @@ let compare_head_gen_leq eq_universes eq_sorts leq_sorts eq leq t1 t2 =
| App (c1,l1), App (c2,l2) ->
Int.equal (Array.length l1) (Array.length l2) &&
eq c1 c2 && Array.equal eq l1 l2
- | Proj (p1,c1), Proj (p2,c2) -> eq_constant p1 p2 && eq c1 c2
+ | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq c1 c2
| Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal eq l1 l2
| Const (c1,u1), Const (c2,u2) -> eq_constant c1 c2 && eq_universes true u1 u2
| Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && eq_universes false u1 u2
@@ -657,7 +657,7 @@ let constr_ord_int f t1 t2 =
| App (Cast(c1,_,_),l1), _ -> f (mkApp (c1,l1)) t2
| _, App (Cast(c2, _,_),l2) -> f t1 (mkApp (c2,l2))
| App (c1,l1), App (c2,l2) -> (f =? (Array.compare f)) c1 c2 l1 l2
- | Proj (p1,c1), Proj (p2,c2) -> (con_ord =? f) p1 p2 c1 c2
+ | Proj (p1,c1), Proj (p2,c2) -> (Projection.compare =? f) p1 p2 c1 c2
| Evar (e1,l1), Evar (e2,l2) ->
(Evar.compare =? (Array.compare f)) e1 e2 l1 l2
| Const (c1,u1), Const (c2,u2) -> con_ord c1 c2
@@ -820,8 +820,8 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
(Evar (e,l), combinesmall 8 (combine (Evar.hash e) hl))
| Proj (p,c) ->
let c, hc = sh_rec c in
- let p' = sh_con p in
- (Proj (p', c), combinesmall 17 (combine (Constant.hash p') hc))
+ let p' = Projection.hashcons p in
+ (Proj (p', c), combinesmall 17 (combine (Projection.hash p') hc))
| Const (c,u) ->
let c' = sh_con c in
let u', hu = sh_instance u in
@@ -906,7 +906,7 @@ let rec hash t =
| App (c,l) ->
combinesmall 7 (combine (hash_term_array l) (hash c))
| Proj (p,c) ->
- combinesmall 17 (combine (Constant.hash p) (hash c))
+ combinesmall 17 (combine (Projection.hash p) (hash c))
| Evar (e,l) ->
combinesmall 8 (combine (Evar.hash e) (hash_term_array l))
| Const (c,u) ->
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 58f248b03..da7ac6a0d 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -103,7 +103,7 @@ val mkConst : constant -> constr
val mkConstU : pconstant -> constr
(** Constructs a projection application *)
-val mkProj : (constant * constr) -> constr
+val mkProj : (projection * constr) -> constr
(** Inductive types *)
@@ -190,7 +190,7 @@ type ('constr, 'types) kind_of_term =
| Case of case_info * 'constr * 'constr * 'constr array
| Fix of ('constr, 'types) pfixpoint
| CoFix of ('constr, 'types) pcofixpoint
- | Proj of constant * 'constr
+ | Proj of projection * 'constr
(** User view of [constr]. For [App], it is ensured there is at
least one argument and the function is not itself an applicative
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 2d316fc1d..5f6aebc4e 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -123,12 +123,13 @@ let expmod_constr cache modlist c =
| Proj (p, c') ->
(try
- let p' = share_univs (ConstRef p) Univ.Instance.empty modlist in
+ let p' = share_univs (ConstRef (Projection.constant p)) Univ.Instance.empty modlist in
+ let make c = Projection.make c (Projection.unfolded p) in
match kind_of_term p' with
- | Const (p',_) -> mkProj (p', substrec c')
+ | Const (p',_) -> mkProj (make p', substrec c')
| App (f, args) ->
(match kind_of_term f with
- | Const (p', _) -> mkProj (p', substrec c')
+ | Const (p', _) -> mkProj (make p', substrec c')
| _ -> assert false)
| _ -> assert false
with Not_found -> map_constr substrec c)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 6b0b0bdba..b331d8da7 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -328,7 +328,7 @@ let template_polymorphic_pconstant (cst,u) env =
else template_polymorphic_constant cst env
let lookup_projection cst env =
- match (lookup_constant cst env).const_proj with
+ match (lookup_constant (Projection.constant cst) env).const_proj with
| Some pb -> pb
| None -> anomaly (Pp.str "lookup_projection: constant is not a projection")
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 4feec40e8..73a23ef05 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -692,14 +692,15 @@ let compute_projections ((kn, _ as ind), u as indsp) n nparamargs params
| Name id ->
let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in
let ty = substl subst (liftn 1 j t) in
- let term = mkProj (kn, mkRel 1) in
+ let term = mkProj (Projection.make kn true, mkRel 1) in
+ let fterm = mkProj (Projection.make kn false, mkRel 1) in
let compat = compat_body ty (j - 1) in
let etab = it_mkLambda_or_LetIn (mkLambda (x, rp, term)) params in
let etat = it_mkProd_or_LetIn (mkProd (x, rp, ty)) params in
let body = { proj_ind = fst ind; proj_npars = nparamargs;
proj_arg = i; proj_type = ty; proj_eta = etab, etat;
proj_body = compat } in
- (i + 1, j + 1, kn :: kns, body :: pbs, term :: subst)
+ (i + 1, j + 1, kn :: kns, body :: pbs, fterm :: subst)
| Anonymous -> raise UndefinableExpansion
in
let (_, _, kns, pbs, subst) = List.fold_right projections ctx (0, 1, [], [], []) in
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index cfe46152e..b65fdb3ac 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -342,13 +342,15 @@ let rec map_kn f f' c =
let func = map_kn f f' in
match kind_of_term c with
| Const kn -> (try snd (f' kn) with No_subst -> c)
- | Proj (kn,t) ->
- let kn' = try fst (f' (kn,Univ.Instance.empty))
- with No_subst -> kn
+ | Proj (p,t) ->
+ let p' =
+ try
+ Projection.map (fun kn -> fst (f' (kn,Univ.Instance.empty))) p
+ with No_subst -> p
in
let t' = func t in
- if kn' == kn && t' == t then c
- else mkProj (kn', t')
+ if p' == p && t' == t then c
+ else mkProj (p', t')
| Ind ((kn,i),u) ->
let kn' = f kn in
if kn'==kn then c else mkIndU ((kn',i),u)
diff --git a/kernel/names.ml b/kernel/names.ml
index c76d95937..5d73bd520 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -782,7 +782,33 @@ let kn_ord = KerName.compare
(** Compatibility layer for [Constant] *)
type constant = Constant.t
-type projection = constant
+
+
+module Projection =
+struct
+ type t = constant * bool
+
+ let make c b = (c, b)
+
+ let constant = fst
+ let unfolded = snd
+ let unfold (c, b as p) = if b then p else (c, true)
+ let equal (c, b) (c', b') = Constant.equal c c' && b == b'
+ let hash (c, b) = (if b then 0 else 1) + Constant.hash c
+ let hashcons (c, b as x) =
+ let c' = hcons_con c in
+ if c' == c then x else (c', b)
+
+ let compare (c, b) (c', b') =
+ if b == b' then Constant.CanOrd.compare c c'
+ else if b then 1 else -1
+
+ let map f (c, b as x) =
+ let c' = f c in
+ if c' == c then x else (c', b)
+end
+
+type projection = Projection.t
let constant_of_kn = Constant.make1
let constant_of_kn_equiv = Constant.make
diff --git a/kernel/names.mli b/kernel/names.mli
index 49a838ae5..893cad09d 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -634,7 +634,25 @@ val kn_ord : kernel_name -> kernel_name -> int
type constant = Constant.t
(** @deprecated Alias type *)
-type projection = constant
+module Projection : sig
+ type t
+
+ val make : constant -> bool -> t
+
+ val constant : t -> constant
+ val unfolded : t -> bool
+ val unfold : t -> t
+
+ val equal : t -> t -> bool
+ val hash : t -> int
+ val hashcons : t -> t
+
+ val compare : t -> t -> int
+
+ val map : (constant -> constant) -> t -> t
+end
+
+type projection = Projection.t
val constant_of_kn_equiv : KerName.t -> KerName.t -> constant
(** @deprecated Same as [Constant.make] *)
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index bd659a471..041751ecf 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1923,7 +1923,8 @@ let rec compile_deps env sigma prefix ~interactive init t =
comp_stack, (mind_updates, const_updates)
| Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind
| Proj (p,c) ->
- compile_deps env sigma prefix ~interactive init (mkApp (mkConst p, [|c|]))
+ let term = mkApp (mkConst (Projection.constant p), [|c|]) in
+ compile_deps env sigma prefix ~interactive init term
| Case (ci, p, c, ac) ->
let mind = fst ci.ci_ind in
let init = compile_mind_deps env prefix ~interactive init mind in
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 34ed33f94..ba45c329f 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -586,7 +586,8 @@ let rec lambda_of_constr env sigma c =
| Construct _ -> lambda_of_app env sigma c empty_args
| Proj (p, c) ->
- mkLapp (Lproj (get_const_prefix !global_env p, p)) [|lambda_of_constr env sigma c|]
+ let kn = Projection.constant p in
+ mkLapp (Lproj (get_const_prefix !global_env kn, kn)) [|lambda_of_constr env sigma c|]
| Case(ci,t,a,branches) ->
let (mind,i as ind) = ci.ci_ind in
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 802d2b67b..9a7146890 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -275,12 +275,14 @@ let in_whnf (t,stk) =
| FLOCKED -> assert false
let unfold_projection infos p c =
- if RedFlags.red_set infos.i_flags (RedFlags.fCONST p) then
- (match try Some (lookup_projection p (info_env infos)) with Not_found -> None with
- | Some pb ->
- let s = Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p) in
- Some (c, s)
- | None -> None)
+ let unf = Projection.unfolded p in
+ if unf || RedFlags.red_set infos.i_flags (RedFlags.fCONST (Projection.constant p)) then
+ (match try Some (lookup_projection p (info_env infos)) with Not_found -> None with
+ | Some pb ->
+ let s = Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg,
+ Projection.constant p) in
+ Some (c, s)
+ | None -> None)
else None
(* Conversion between [lft1]term1 and [lft2]term2 *)
@@ -368,7 +370,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
| Some (def2,s2) ->
eqappr cv_pb l2r infos appr1 (lft2, whd def2 (s2 :: v2)) cuniv
| None ->
- if eq_constant p1 p2 && compare_stack_shape v1 v2 then
+ if Projection.equal p1 p2 && compare_stack_shape v1 v2 then
let u1 = ccnv CONV l2r infos el1 el2 c1 c2 cuniv in
convert_stacks l2r infos lft1 lft2 v1 v2 u1
else (* Two projections in WHNF: unfold *)
diff --git a/kernel/term.ml b/kernel/term.ml
index 3b6b69a28..ab678666f 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -89,7 +89,7 @@ type ('constr, 'types) kind_of_term = ('constr, 'types) Constr.kind_of_term =
| Case of case_info * 'constr * 'constr * 'constr array
| Fix of ('constr, 'types) pfixpoint
| CoFix of ('constr, 'types) pcofixpoint
- | Proj of constant * 'constr
+ | Proj of projection * 'constr
type values = Constr.values
diff --git a/kernel/term.mli b/kernel/term.mli
index 5ff5f9ba1..28ebc41e2 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -86,7 +86,7 @@ type ('constr, 'types) kind_of_term = ('constr, 'types) Constr.kind_of_term =
| Case of case_info * 'constr * 'constr * 'constr array
| Fix of ('constr, 'types) pfixpoint
| CoFix of ('constr, 'types) pcofixpoint
- | Proj of constant * 'constr
+ | Proj of projection * 'constr
type values = Constr.values
@@ -405,7 +405,7 @@ val mkLambda : Name.t * types * constr -> constr
val mkLetIn : Name.t * constr * types * constr -> constr
val mkApp : constr * constr array -> constr
val mkConst : constant -> constr
-val mkProj : (constant * constr) -> constr
+val mkProj : projection * constr -> constr
val mkInd : inductive -> constr
val mkConstruct : constructor -> constr
val mkConstU : constant puniverses -> constr
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index fa7dd105c..5421020d2 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -184,7 +184,8 @@ let judge_of_constant_knowing_parameters env (kn,u as cst) args =
let judge_of_constant env cst =
judge_of_constant_knowing_parameters env cst [||]
-let type_of_projection env (cst,u) =
+let type_of_projection env (p,u) =
+ let cst = Projection.constant p in
let cb = lookup_constant cst env in
match cb.const_proj with
| Some pb ->
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 976380ede..3f9345ff8 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -203,7 +203,9 @@ let rec conv_eq env pb t1 t2 cu =
else raise NotConvertible
| Const c1, Const c2 -> eq_puniverses eq_constant c1 c2 cu
| Proj (p1,c1), Proj (p2,c2) ->
- if eq_constant p1 p2 then conv_eq env pb c1 c2 cu else raise NotConvertible
+ if eq_constant (Projection.constant p1) (Projection.constant p2) then
+ conv_eq env pb c1 c2 cu
+ else raise NotConvertible
| Ind c1, Ind c2 ->
eq_puniverses eq_ind c1 c2 cu
| Construct c1, Construct c2 ->
diff --git a/library/heads.ml b/library/heads.ml
index 31908816b..8b28f0500 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -84,7 +84,7 @@ let kind_of_head env t =
| Meta _ | Evar _ -> NotImmediatelyComputableHead
| App (c,al) -> aux k (Array.to_list al @ l) c b
| Proj (p,c) ->
- (try on_subterm k (c :: l) b (constant_head p)
+ (try on_subterm k (c :: l) b (constant_head (Projection.constant p))
with Not_found -> assert false)
| Case (_,_,c,_) -> aux k [] c true
diff --git a/library/universes.ml b/library/universes.ml
index 7fe4258c2..cc0153311 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -220,7 +220,7 @@ let compare_head_gen_proj env equ eqs eqc' m n =
| Proj (p, c), App (f, args)
| App (f, args), Proj (p, c) ->
(match kind_of_term f with
- | Const (p', u) when eq_constant p p' ->
+ | Const (p', u) when eq_constant (Projection.constant p) p' ->
let pb = Environ.lookup_projection p env in
let npars = pb.Declarations.proj_npars in
if Array.length args == npars + 1 then
@@ -429,7 +429,7 @@ let global_app_of_constr c =
| Ind (i, u) -> (IndRef i, u), None
| Construct (c, u) -> (ConstructRef c, u), None
| Var id -> (VarRef id, Instance.empty), None
- | Proj (p, c) -> (ConstRef p, Instance.empty), Some c
+ | Proj (p, c) -> (ConstRef (Projection.constant p), Instance.empty), Some c
| _ -> raise Not_found
open Declarations
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 50b647e44..5a4a435a5 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -425,15 +425,15 @@ and applist_proj c l =
and applist_projection c l =
match kind_of_term c with
| Const c when Environ.is_projection (fst c) (Global.env()) ->
+ let p = Projection.make (fst c) false in
(match l with
| [] -> (* Expand the projection *)
- let kn = fst c in
let ty,_ = Typeops.type_of_constant (Global.env ()) c in
- let pb = Environ.lookup_projection kn (Global.env()) in
+ let pb = Environ.lookup_projection p (Global.env()) in
let ctx,_ = Term.decompose_prod_n_assum (pb.Declarations.proj_npars + 1) ty in
- it_mkLambda_or_LetIn (mkProj(kn,mkRel 1)) ctx
+ it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx
| hd :: tl ->
- applistc (mkProj (fst c, hd)) tl)
+ applistc (mkProj (p, hd)) tl)
| _ -> applistc c l
let rec canonize_name c =
@@ -456,9 +456,10 @@ let rec canonize_name c =
mkLetIn (na, func b,func t,func ct)
| App (ct,l) ->
mkApp (func ct,Array.smartmap func l)
- | Proj(kn,c) ->
- let canon_const = constant_of_kn (canonical_con kn) in
- (mkProj (canon_const, func c))
+ | Proj(p,c) ->
+ let p' = Projection.map (fun kn ->
+ constant_of_kn (canonical_con kn)) p in
+ (mkProj (p', func c))
| _ -> c
(* rebuild a term from a pattern and a substitution *)
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 45d6a9393..364a71d28 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -78,8 +78,9 @@ let rec decompose_term env sigma t=
let canon_const = constant_of_kn (canonical_con c) in
(Symb (mkConstU (canon_const,u)))
| Proj (p, c) ->
- let canon_const = constant_of_kn (canonical_con p) in
- (Appli (Symb (mkConst canon_const), decompose_term env sigma c))
+ let canon_const kn = constant_of_kn (canonical_con kn) in
+ let p' = Projection.map canon_const p in
+ (Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c))
| _ ->if closed0 t then (Symb t) else raise Not_found
(* decompose equality in members and type *)
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index bbbc9bce7..aa0232d19 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -617,7 +617,7 @@ let rec extract_term env mle mlt c args =
| Construct (cp,u) ->
extract_cons_app env mle mlt cp u args
| Proj (p, c) ->
- extract_cst_app env mle mlt p Univ.Instance.empty (c :: args)
+ extract_cst_app env mle mlt (Projection.constant p) Univ.Instance.empty (c :: args)
| Rel n ->
(* As soon as the expected [mlt] for the head is known, *)
(* we unify it with an fresh copy of the stored type of [Rel n]. *)
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 745e190cb..ed7f18001 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -211,9 +211,9 @@ let compute_rhs bodyi index_of_f =
let i = destRel (Array.last args) in
PMeta (Some (coerce_meta_in i))
| App (f,args) ->
- PApp (snd (pattern_of_constr Evd.empty f), Array.map aux args)
+ PApp (snd (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args)
| Cast (c,_,_) -> aux c
- | _ -> snd (pattern_of_constr Evd.empty c)
+ | _ -> snd (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c)
in
aux bodyi
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 726e64e81..c9c6cecb1 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1283,7 +1283,8 @@ let mk_case pb (ci,pred,c,brs) =
let mib = lookup_mind (fst ci.ci_ind) pb.env in
match mib.mind_record with
| Some (cs, pbs) when Array.length pbs > 0 ->
- Reduction.beta_appvect brs.(0) (Array.map (fun p -> mkProj (p, c)) cs)
+ Reduction.beta_appvect brs.(0)
+ (Array.map (fun p -> mkProj (Projection.make p false, c)) cs)
| _ -> mkCase (ci,pred,c,brs)
(**********************************************************************)
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 4c1e3c3af..d491ded72 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -197,7 +197,7 @@ let rec norm_head info env t stack =
| Cast (ct,_,_) -> norm_head info env ct stack
| Proj (p, c) ->
- let pinfo = Option.get ((Environ.lookup_constant p (info_env info)).Declarations.const_proj) in
+ let pinfo = Environ.lookup_projection p (info_env info) in
norm_head info env c (PROJ (p, pinfo, stack))
(* constants, axioms
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index f754f9f3f..73534210c 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -31,7 +31,7 @@ type cl_typ =
| CL_SECVAR of variable
| CL_CONST of constant
| CL_IND of inductive
- | CL_PROJ of projection
+ | CL_PROJ of constant
type cl_info_typ = {
cl_param : int
@@ -196,7 +196,8 @@ let find_class_type sigma t =
match kind_of_term t' with
| Var id -> CL_SECVAR id, Univ.Instance.empty, args
| Const (sp,u) -> CL_CONST sp, u, args
- | Proj (p, c) -> CL_PROJ p, Univ.Instance.empty, c :: args
+ | Proj (p, c) when not (Projection.unfolded p) ->
+ CL_PROJ (Projection.constant p), Univ.Instance.empty, c :: args
| Ind (ind_sp,u) -> CL_IND ind_sp, u, args
| Prod (_,_,_) -> CL_FUN, Univ.Instance.empty, []
| Sort _ -> CL_SORT, Univ.Instance.empty, []
@@ -406,7 +407,7 @@ let reference_arity_length ref =
let projection_arity_length p =
let len = reference_arity_length (ConstRef p) in
- let pb = Environ.lookup_projection p (Global.env ()) in
+ let pb = Environ.lookup_projection (Projection.make p false) (Global.env ()) in
len - pb.Declarations.proj_npars
let class_params = function
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index e39b2bba4..1db7bbd61 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -19,7 +19,7 @@ type cl_typ =
| CL_SECVAR of variable
| CL_CONST of constant
| CL_IND of inductive
- | CL_PROJ of projection
+ | CL_PROJ of constant
(** Equality over [cl_typ] *)
val cl_typ_eq : cl_typ -> cl_typ -> bool
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 6a48d84ed..0ae873643 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -350,7 +350,7 @@ let apply_coercion env sigma p hj typ_cl =
(if isid then
{ uj_val = ja.uj_val; uj_type = jres.uj_type }
else if isproj then
- { uj_val = mkProj (fst (destConst fv.uj_val), ja.uj_val);
+ { uj_val = mkProj (Projection.make (fst (destConst fv.uj_val)) false, ja.uj_val);
uj_type = jres.uj_type }
else
jres),
diff --git a/pretyping/constrMatching.ml b/pretyping/constrMatching.ml
index 7af639633..b0f1dd920 100644
--- a/pretyping/constrMatching.ml
+++ b/pretyping/constrMatching.ml
@@ -227,10 +227,10 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
| PApp (c1,arg1), App (c2,arg2) ->
(match c1, kind_of_term c2 with
- | PRef (ConstRef r), Proj (pr,c) when not (eq_constant r pr) ->
+ | PRef (ConstRef r), Proj (pr,c) when not (eq_constant r (Projection.constant pr)) ->
raise PatternMatchingFailure
| PProj (pr1,c1), Proj (pr,c) ->
- if eq_constant pr1 pr then
+ if eq_constant (Projection.constant pr1) (Projection.constant pr) then
try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c) arg1 arg2
with Invalid_argument _ -> raise PatternMatchingFailure
else raise PatternMatchingFailure
@@ -241,14 +241,16 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c2) arg1 arg2
with Invalid_argument _ -> raise PatternMatchingFailure)
- | PApp (PRef (ConstRef c1), _), Proj (pr, c2) when not (eq_constant c1 pr) ->
+ | PApp (PRef (ConstRef c1), _), Proj (pr, c2) when not (eq_constant c1
+ (Projection.constant pr)) ->
raise PatternMatchingFailure
| PApp (c, args), Proj (pr, c2) ->
let term = Retyping.expand_projection env sigma pr c2 [] in
sorec stk env subst p term
- | PProj (p1,c1), Proj (p2,c2) when eq_constant p1 p2 ->
+ | PProj (p1,c1), Proj (p2,c2) when
+ eq_constant (Projection.constant p1) (Projection.constant p2) ->
sorec stk env subst c1 c2
| PProd (na1,c1,d1), Prod(na2,c2,d2) ->
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 07540af57..0b0ff2fb5 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -445,12 +445,22 @@ let rec detype flags avoid env sigma t =
| Proj (p,c) ->
if fst flags || !Flags.in_debugger || !Flags.in_toplevel then
(* lax mode, used by debug printers only *)
- GApp (dl, GRef (dl, ConstRef p, None),
+ GApp (dl, GRef (dl, ConstRef (Projection.constant p), None),
[detype flags avoid env sigma c])
- else let ty = Retyping.get_type_of (snd env) sigma c in
- let (ind, args) = Inductive.find_rectype (snd env) ty in
- GApp (dl, GRef (dl, ConstRef p, None),
- List.map (detype flags avoid env sigma) (args @ [c]))
+ else
+ if Projection.unfolded p then
+ (** Print the compatibility match version *)
+ let pb = Environ.lookup_projection p (snd env) in
+ let body = pb.Declarations.proj_body in
+ let ty = Retyping.get_type_of (snd env) sigma c in
+ let (ind, args) = Inductive.find_rectype (snd env) ty in
+ let body' = strip_lam_assum body in
+ detype flags avoid env sigma (substl (c :: List.rev args) body')
+ else
+ let ty = Retyping.get_type_of (snd env) sigma c in
+ let (ind, args) = Inductive.find_rectype (snd env) ty in
+ GApp (dl, GRef (dl, ConstRef (Projection.constant p), None),
+ List.map (detype flags avoid env sigma) (args @ [c]))
| Evar (evk,cl) ->
let id,l =
try Evd.evar_ident evk sigma,
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index e27ee84aa..ddaf69676 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -33,18 +33,24 @@ let _ = Goptions.declare_bool_option {
Goptions.optwrite = (fun a -> debug_unification:=a);
}
-let unfold_projection env p c stk =
+let unfold_projection env ts p c stk =
(match try Some (lookup_projection p env) with Not_found -> None with
| Some pb ->
+ let cst = Projection.constant p in
let unfold () =
- let s = Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p) in
+ let s = Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg,
+ Projection.constant p) in
Some (c, s :: stk)
in
- (match ReductionBehaviour.get (Globnames.ConstRef p) with
- | None -> unfold ()
- | Some (recargs, nargs, flags) ->
- if (List.mem `ReductionNeverUnfold flags) then None
- else unfold ())
+ if Projection.unfolded p then unfold ()
+ else
+ if is_transparent_constant ts cst then
+ (match ReductionBehaviour.get (Globnames.ConstRef cst) with
+ | None -> unfold ()
+ | Some (recargs, nargs, flags) ->
+ if (List.mem `ReductionNeverUnfold flags) then None
+ else unfold ())
+ else None
| None -> None)
let eval_flexible_term ts env c stk =
@@ -64,10 +70,7 @@ let eval_flexible_term ts env c stk =
with Not_found -> None)
| LetIn (_,b,_,c) -> Some (subst1 b c, stk)
| Lambda _ -> Some (c, stk)
- | Proj (p, c) ->
- if is_transparent_constant ts p
- then unfold_projection env p c stk
- else None
+ | Proj (p, c) -> unfold_projection env ts p c stk
| _ -> assert false
type flex_kind_of_term =
@@ -527,7 +530,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
in
ise_try evd [f1; f2]
- | Proj (p, c), Proj (p', c') when eq_constant p p' ->
+ | Proj (p, c), Proj (p', c') when Projection.equal p p' ->
let f1 i =
ise_and i
[(fun i -> evar_conv_x ts env i CONV c c');
@@ -539,7 +542,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
in
ise_try evd [f1; f2]
- | Proj (p, t), Const (p',_) when eq_constant p p' ->
+ | Proj (p, t), Const (p',_) when eq_constant (Projection.constant p) p' ->
let f1 i =
let pb = Environ.lookup_projection p env in
(match Stack.strip_n_app pb.Declarations.proj_npars sk2' with
@@ -554,7 +557,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
in evar_eqappr_x ts env i pbty out1 out2
in ise_try evd [f1;f2]
- | Const (p',_), Proj (p, t) when eq_constant p p' ->
+ | Const (p',_), Proj (p, t) when eq_constant (Projection.constant p) p' ->
let f1 i =
let pb = Environ.lookup_projection p env in
(match Stack.strip_n_app pb.Declarations.proj_npars sk1' with
@@ -801,7 +804,7 @@ and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
let l1' = Stack.tail pars sk1 in
let l2' =
let term = Stack.zip (term2,sk2) in
- List.map (fun p -> mkProj (p, term)) (Array.to_list projs)
+ List.map (fun p -> mkProj (Projection.make p false, term)) (Array.to_list projs)
in
exact_ise_stack2 env evd (evar_conv_x (fst ts, false)) l1'
(Stack.append_app_list l2' Stack.empty)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 9f460d08f..6e32d70c0 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -104,7 +104,8 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
| None -> mkCase (ci, lift ndepar p, mkRel 1,
Termops.rel_vect ndepar k)
| Some ps ->
- let term = mkApp (mkRel 2, Array.map (fun p -> mkProj (p, mkRel 1)) ps) in
+ let term = mkApp (mkRel 2,
+ Array.map (fun p -> mkProj (Projection.make p true, mkRel 1)) ps) in
if dep then
let ty = mkApp (mkRel 3, [| mkRel 1 |]) in
mkCast (term, DEFAULTcast, ty)
@@ -390,7 +391,7 @@ let mis_make_indrec env sigma listdepkind mib u =
let n, subst =
List.fold_right (fun (na,b,t) (i, subst) ->
if b == None then
- let t = mkProj (ps.(i), mkRel 1) in
+ let t = mkProj (Projection.make ps.(i) true, mkRel 1) in
(i + 1, t :: subst)
else (i, mkRel 0 :: subst))
ctx (0, [])
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index 245c7f943..a6c0149a4 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -83,7 +83,7 @@ let head_name c = (* Find the head constant of a constr if any *)
match kind_of_term c with
| Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c)
| Cast (c,_,_) | App (c,_) -> hdrec c
- | Proj (kn,_) -> Some (Label.to_id (con_label kn))
+ | Proj (kn,_) -> Some (Label.to_id (con_label (Projection.constant kn)))
| Const _ | Ind _ | Construct _ | Var _ ->
Some (basename_of_global (global_of_constr c))
| Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
@@ -104,7 +104,7 @@ let hdchar env c =
match kind_of_term c with
| Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c) -> hdrec (k+1) c
| Cast (c,_,_) | App (c,_) -> hdrec k c
- | Proj (kn,_)
+ | Proj (kn,_) -> lowercase_first_char (Label.to_id (con_label (Projection.constant kn)))
| Const (kn,_) -> lowercase_first_char (Label.to_id (con_label kn))
| Ind (x,_) -> lowercase_first_char (basename_of_global (IndRef x))
| Construct (x,_) -> lowercase_first_char (basename_of_global (ConstructRef x))
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 829fa106c..60db95e25 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -268,7 +268,7 @@ and nf_atom env atom =
| Aevar (ev,_) -> mkEvar ev
| Aproj(p,c) ->
let c = nf_accu env c in
- mkProj(p,c)
+ mkProj(Projection.make p false,c)
| _ -> fst (nf_atom_type env atom)
and nf_atom_type env atom =
@@ -342,7 +342,7 @@ and nf_atom_type env atom =
| Aproj(p,c) ->
let c,tc = nf_accu_type env c in
let cj = make_judge c tc in
- let uj = Typeops.judge_of_projection env p cj in
+ let uj = Typeops.judge_of_projection env (Projection.make p true) cj in
uj.uj_val, uj.uj_type
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 01317ba25..9b7726692 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -106,7 +106,7 @@ let rec head_pattern_bound t =
| PCase (_,p,c,br) -> head_pattern_bound c
| PRef r -> r
| PVar id -> VarRef id
- | PProj (p,c) -> ConstRef p
+ | PProj (p,c) -> ConstRef (Projection.constant p)
| PEvar _ | PRel _ | PMeta _ | PSoApp _ | PSort _ | PFix _
-> raise BoundPattern
(* Perhaps they were arguments, but we don't beta-reduce *)
@@ -120,7 +120,7 @@ let head_of_constr_reference c = match kind_of_term c with
| Var id -> VarRef id
| _ -> anomaly (Pp.str "Not a rigid reference")
-let pattern_of_constr sigma t =
+let pattern_of_constr env sigma t =
let ctx = ref [] in
let rec pattern_of_constr t =
match kind_of_term t with
@@ -150,7 +150,8 @@ let pattern_of_constr sigma t =
| Const (sp,u) -> PRef (ConstRef (constant_of_kn(canonical_con sp)))
| Ind (sp,u) -> PRef (canonical_gr (IndRef sp))
| Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp))
- | Proj (p, c) -> PProj (constant_of_kn(canonical_con p), pattern_of_constr c)
+ | Proj (p, c) -> PProj (Projection.map (fun kn -> constant_of_kn(canonical_con kn)) p,
+ pattern_of_constr c)
| Evar (evk,ctxt as ev) ->
(match snd (Evd.evar_source evk sigma) with
| Evar_kinds.MatchingVar (b,id) ->
@@ -203,7 +204,7 @@ let error_instantiate_pattern id l =
++ strbrk " in pattern because the term refers to " ++ pr_enum pr_id l
++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.")
-let instantiate_pattern sigma lvar c =
+let instantiate_pattern env sigma lvar c =
let rec aux vars = function
| PVar id as x ->
(try
@@ -215,7 +216,7 @@ let instantiate_pattern sigma lvar c =
ctx
in
let c = substl inst c in
- snd (pattern_of_constr sigma c)
+ snd (pattern_of_constr env sigma c)
with Not_found (* List.index failed *) ->
let vars =
List.map_filter (function Name id -> Some id | _ -> None) vars in
@@ -240,13 +241,13 @@ let rec subst_pattern subst pat =
| PRef ref ->
let ref',t = subst_global subst ref in
if ref' == ref then pat else
- snd (pattern_of_constr Evd.empty t)
+ snd (pattern_of_constr (Global.env()) Evd.empty t)
| PVar _
| PEvar _
| PRel _ -> pat
| PProj (p,c) ->
- let p',t = subst_global subst (ConstRef p) in
- let p' = destConstRef p' in
+ let p' = Projection.map (fun p ->
+ destConstRef (fst (subst_global subst (ConstRef p)))) p in
let c' = subst_pattern subst c in
if p' == p && c' == c then pat else
PProj(p',c')
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index cfe71510a..382357a8d 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -39,7 +39,7 @@ val head_of_constr_reference : Term.constr -> global_reference
a pattern; currently, no destructor (Cases, Fix, Cofix) and no
existential variable are allowed in [c] *)
-val pattern_of_constr : Evd.evar_map -> constr -> named_context * constr_pattern
+val pattern_of_constr : Environ.env -> Evd.evar_map -> constr -> named_context * constr_pattern
(** [pattern_of_glob_constr l c] translates a term [c] with metavariables into
a pattern; variables bound in [l] are replaced by the pattern to which they
@@ -48,7 +48,7 @@ val pattern_of_constr : Evd.evar_map -> constr -> named_context * constr_pattern
val pattern_of_glob_constr : glob_constr ->
patvar list * constr_pattern
-val instantiate_pattern :
+val instantiate_pattern : Environ.env ->
Evd.evar_map -> extended_patvar_map ->
constr_pattern -> constr_pattern
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 5c18297c0..8c4dbfd98 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -566,6 +566,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
let app_f =
match kind_of_term fj.uj_val with
| Const (p, u) when Environ.is_projection p env ->
+ let p = Projection.make p false in
let pb = Environ.lookup_projection p env in
let npars = pb.Declarations.proj_npars in
fun n ->
@@ -705,7 +706,8 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
let rec aux n k names l =
match names, l with
| na :: names, ((_, None, t) :: l) ->
- (na, Some (lift (cs.cs_nargs - n) (mkProj (ps.(cs.cs_nargs - k), cj.uj_val))), t)
+ let proj = Projection.make ps.(cs.cs_nargs - k) false in
+ (na, Some (lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val))), t)
:: aux (n+1) (k + 1) names l
| na :: names, ((_, c, t) :: l) ->
(na, c, t) :: aux (n+1) k names l
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 4c9fc4dc5..fb66923a6 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -208,7 +208,7 @@ sig
type 'a member =
| App of 'a app_node
| Case of case_info * 'a * 'a array * Cst_stack.t
- | Proj of int * int * projection
+ | Proj of int * int * constant
| Fix of fixpoint * 'a t * Cst_stack.t
| Cst of 'a cst_member * int * int list * 'a t * Cst_stack.t
| Shift of int
@@ -262,7 +262,7 @@ struct
type 'a member =
| App of 'a app_node
| Case of Term.case_info * 'a * 'a array * Cst_stack.t
- | Proj of int * int * projection
+ | Proj of int * int * constant
| Fix of fixpoint * 'a t * Cst_stack.t
| Cst of 'a cst_member * int * int list * 'a t * Cst_stack.t
| Shift of int
@@ -302,7 +302,7 @@ struct
if Univ.Instance.is_empty u then Constant.print c
else str"(" ++ Constant.print c ++ str ", " ++ Univ.Instance.pr u ++ str")"
| Cst_proj (p, c) ->
- pr_c c ++ str".(" ++ Constant.print p ++ str")"
+ pr_c c ++ str".(" ++ Constant.print (Projection.constant p) ++ str")"
let empty = []
let is_empty = CList.is_empty
@@ -329,7 +329,7 @@ struct
| Cst_const (c1,u1), Cst_const (c2, u2) ->
Constant.equal c1 c2 && Univ.Instance.equal u1 u2
| Cst_proj (p1,c1), Cst_proj (p2,c2) ->
- Constant.equal p1 p2 && f (c1,lft1) (c2,lft2)
+ Projection.equal p1 p2 && f (c1,lft1) (c2,lft2)
| _, _ -> false
in
let rec equal_rec sk1 lft1 sk2 lft2 =
@@ -347,7 +347,7 @@ struct
then equal_rec s1 lft1 s2 lft2
else None
| (Proj (n1,m1,p)::s1, Proj(n2,m2,p2)::s2) ->
- if Int.equal n1 n2 && Int.equal m1 m2 && Names.Constant.CanOrd.equal p p2
+ if Int.equal n1 n2 && Int.equal m1 m2 && Constant.equal p p2
then equal_rec s1 lft1 s2 lft2
else None
| Fix (f1,s1,_) :: s1', Fix (f2,s2,_) :: s2' ->
@@ -537,7 +537,7 @@ struct
| f, (Cst (cst,_,_,params,_)::s) ->
zip ~refold (constr_of_cst_member cst (params @ (append_app [|f|] s)))
| f, (Shift n::s) -> zip ~refold (lift n f, s)
- | f, (Proj (n,m,p)::s) -> zip ~refold (mkProj (p,f),s)
+ | f, (Proj (n,m,p)::s) -> zip ~refold (mkProj (Projection.make p true,f),s)
| _, (Update _::_) -> assert false
end
@@ -829,13 +829,14 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
| Some (bef,arg,s') ->
whrec Cst_stack.empty (arg,Stack.Cst(Stack.Cst_const const,curr,remains,bef,cst_l)::s')
)
- | Proj (p, c) when Closure.RedFlags.red_set flags (Closure.RedFlags.fCONST p) ->
+ | Proj (p, c) when Closure.RedFlags.red_projection flags p ->
(let pb = lookup_projection p env in
+ let kn = Projection.constant p in
let npars = pb.Declarations.proj_npars
and arg = pb.Declarations.proj_arg in
- match ReductionBehaviour.get (Globnames.ConstRef p) with
+ match ReductionBehaviour.get (Globnames.ConstRef kn) with
| None ->
- let stack' = (c, Stack.Proj (npars, arg, p) :: stack) in
+ let stack' = (c, Stack.Proj (npars, arg, kn) :: stack) in
whrec Cst_stack.empty(* cst_l *) stack'
| Some (recargs, nargs, flags) ->
if (List.mem `ReductionNeverUnfold flags
@@ -850,7 +851,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
|[] -> (* if nargs has been specified *)
(* CAUTION : the constant is NEVER refold
(even when it hides a (co)fix) *)
- let stack' = (c, Stack.Proj (npars, arg, p) :: stack) in
+ let stack' = (c, Stack.Proj (npars, arg, kn) :: stack) in
whrec Cst_stack.empty(* cst_l *) stack'
| curr::remains ->
if curr == 0 then (* Try to reduce the record argument *)
@@ -931,7 +932,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
match Stack.strip_n_app 0 stack with
| None -> assert false
| Some (_,arg,s'') ->
- whrec Cst_stack.empty (arg, Stack.Proj (npars,narg,p) :: s''))
+ whrec Cst_stack.empty (arg, Stack.Proj (npars,narg,Projection.constant p) :: s''))
| next :: remains' -> match Stack.strip_n_app (next-curr-1) s'' with
| None -> fold ()
| Some (bef,arg,s''') ->
@@ -984,9 +985,10 @@ let local_whd_state_gen flags sigma =
| _ -> s)
| _ -> s)
- | Proj (p,c) when Closure.RedFlags.red_set flags (Closure.RedFlags.fCONST p) ->
+ | Proj (p,c) when Closure.RedFlags.red_projection flags p ->
(let pb = lookup_projection p (Global.env ()) in
- whrec (c, Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p)
+ whrec (c, Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg,
+ Projection.constant p)
:: stack))
| Case (ci,p,d,lf) ->
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 6672c7fa7..9a9b34751 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -57,7 +57,7 @@ module Stack : sig
type 'a member =
| App of 'a app_node
| Case of case_info * 'a * 'a array * Cst_stack.t
- | Proj of int * int * projection
+ | Proj of int * int * constant
| Fix of fixpoint * 'a t * Cst_stack.t
| Cst of 'a cst_member * int (** current foccussed arg *) * int list (** remaining args *)
* 'a t * Cst_stack.t
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 3374da327..b16cf75f5 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -245,5 +245,5 @@ let sorts_of_context env evc ctxt =
let expand_projection env sigma pr c args =
let ty = get_type_of env sigma c in
let (i,u), ind_args = Inductive.find_rectype env ty in
- mkApp (mkConstU (pr,u),
+ mkApp (mkConstU (Projection.constant pr,u),
Array.of_list (ind_args @ (c :: args)))
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 0088563fa..a2584571d 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -585,7 +585,7 @@ let reduce_proj env sigma whfun whfun' c =
(match kind_of_term constr with
| Construct _ ->
let proj_narg =
- let pb = Option.get ((lookup_constant proj env).Declarations.const_proj) in
+ let pb = lookup_projection proj env in
pb.Declarations.proj_npars + pb.Declarations.proj_arg
in List.nth cargs proj_narg
| _ -> raise Redelimination)
@@ -738,24 +738,26 @@ and whd_simpl_stack env sigma =
| Proj (p, c) ->
(try
- if is_evaluable env (EvalConstRef p) then
- let pb = Option.get ((lookup_constant p env).Declarations.const_proj) in
- (match ReductionBehaviour.get (ConstRef p) with
- | Some (l, n, f) when List.mem `ReductionNeverUnfold f -> (* simpl never *) s'
- | Some (l, n, f) when not (List.is_empty l) ->
- let l' = List.map_filter (fun i ->
- let idx = (i - (pb.Declarations.proj_npars + 1)) in
- if idx < 0 then None else Some idx) l in
- let stack = reduce_params env sigma stack l' in
- (match reduce_projection env sigma pb
- (whd_construct_stack env sigma c) stack
- with
- | Reduced s' -> redrec (applist s')
- | NotReducible -> s')
- | _ ->
- match reduce_projection env sigma pb (whd_construct_stack env sigma c) stack with
- | Reduced s' -> redrec (applist s')
- | NotReducible -> s')
+ let unf = Projection.unfolded p in
+ if unf || is_evaluable env (EvalConstRef (Projection.constant p)) then
+ let pb = lookup_projection p env in
+ (match unf, ReductionBehaviour.get (ConstRef (Projection.constant p)) with
+ | false, Some (l, n, f) when List.mem `ReductionNeverUnfold f ->
+ (* simpl never *) s'
+ | false, Some (l, n, f) when not (List.is_empty l) ->
+ let l' = List.map_filter (fun i ->
+ let idx = (i - (pb.Declarations.proj_npars + 1)) in
+ if idx < 0 then None else Some idx) l in
+ let stack = reduce_params env sigma stack l' in
+ (match reduce_projection env sigma pb
+ (whd_construct_stack env sigma c) stack
+ with
+ | Reduced s' -> redrec (applist s')
+ | NotReducible -> s')
+ | _ ->
+ match reduce_projection env sigma pb (whd_construct_stack env sigma c) stack with
+ | Reduced s' -> redrec (applist s')
+ | NotReducible -> s')
else s'
with Redelimination -> s')
@@ -826,12 +828,10 @@ let try_red_product env sigma c =
| Construct _ -> c
| _ -> redrec env c
in
- (match match_eval_proj env p with
- | Some pb ->
- (match reduce_projection env sigma pb (whd_betaiotazeta_stack sigma c') [] with
- | Reduced s -> simpfun (applist s)
- | NotReducible -> raise Redelimination)
- | None -> raise Redelimination)
+ let pb = lookup_projection p env in
+ (match reduce_projection env sigma pb (whd_betaiotazeta_stack sigma c') [] with
+ | Reduced s -> simpfun (applist s)
+ | NotReducible -> raise Redelimination)
| _ ->
(match match_eval_ref env x with
| Some (ref, u) ->
@@ -920,7 +920,7 @@ let whd_simpl_orelse_delta_but_fix env sigma c =
| CoFix _ | Fix _ -> s'
| Proj (p,c) when
(match kind_of_term constr with
- | Const (c', _) -> eq_constant p c'
+ | Const (c', _) -> eq_constant (Projection.constant p) c'
| _ -> false) ->
let pb = Environ.lookup_projection p env in
if List.length stack <= pb.Declarations.proj_npars then
@@ -947,7 +947,7 @@ let simpl env sigma c = strong whd_simpl env sigma c
let matches_head env sigma c t =
match kind_of_term t with
| App (f,_) -> ConstrMatching.matches env sigma c f
- | Proj (p, _) -> ConstrMatching.matches env sigma c (mkConst p)
+ | Proj (p, _) -> ConstrMatching.matches env sigma c (mkConst (Projection.constant p))
| _ -> raise ConstrMatching.PatternMatchingFailure
let is_pattern_meta = function Pattern.PMeta _ -> true | _ -> false
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index c1347c9b4..d6926dac3 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -79,7 +79,7 @@ let rec pr_constr c = match kind_of_term c with
| Ind ((sp,i),u) -> str"Ind(" ++ pr_puniverses (pr_mind sp ++ str"," ++ int i) u ++ str")"
| Construct (((sp,i),j),u) ->
str"Constr(" ++ pr_puniverses (pr_mind sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")"
- | Proj (p,c) -> str"Proj(" ++ pr_con p ++ str"," ++ pr_constr c ++ str")"
+ | Proj (p,c) -> str"Proj(" ++ pr_con (Projection.constant p) ++ str"," ++ bool (Projection.unfolded p) ++ pr_constr c ++ str")"
| Case (ci,p,c,bl) -> v 0
(hv 0 (str"<"++pr_constr p++str">"++ cut() ++ str"Case " ++
pr_constr c ++ str"of") ++ cut() ++
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 3f7f238c4..050103542 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -370,7 +370,7 @@ let use_metas_pattern_unification flags nb l =
type key =
| IsKey of Closure.table_key
- | IsProj of constant * constr
+ | IsProj of projection * constr
let expand_table_key env = function
| ConstKey cst -> constant_opt_value_in env cst
@@ -380,7 +380,8 @@ let expand_table_key env = function
let unfold_projection env p stk =
(match try Some (lookup_projection p env) with Not_found -> None with
| Some pb ->
- let s = Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p) in
+ let s = Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg,
+ Projection.constant p) in
s :: stk
| None -> assert false)
@@ -405,7 +406,8 @@ let key_of env b flags f =
| Var id when is_transparent env (VarKey id) &&
Id.Pred.mem id (fst flags.modulo_delta) ->
Some (IsKey (VarKey id))
- | Proj (p, c) when Cpred.mem p (snd flags.modulo_delta) ->
+ | Proj (p, c) when Projection.unfolded p
+ || Cpred.mem (Projection.constant p) (snd flags.modulo_delta) ->
Some (IsProj (p, c))
| _ -> None
@@ -417,7 +419,7 @@ let translate_key = function
let translate_key = function
| IsKey k -> translate_key k
- | IsProj (c, _) -> ConstKey c
+ | IsProj (c, _) -> ConstKey (Projection.constant c)
let oracle_order env cf1 cf2 =
match cf1 with
@@ -430,8 +432,10 @@ let oracle_order env cf1 cf2 =
| None -> Some true
| Some k2 ->
match k1, k2 with
- | IsProj (p, _), IsKey (ConstKey (p',_)) when eq_constant p p' -> Some false
- | IsKey (ConstKey (p,_)), IsProj (p', _) when eq_constant p p' -> Some true
+ | IsProj (p, _), IsKey (ConstKey (p',_))
+ when eq_constant (Projection.constant p) p' -> Some false
+ | IsKey (ConstKey (p,_)), IsProj (p', _)
+ when eq_constant p (Projection.constant p') -> Some true
| _ ->
Some (Conv_oracle.oracle_order (Environ.oracle env) false
(translate_key k1) (translate_key k2))
@@ -508,7 +512,7 @@ let eta_constructor_app env f l1 term =
| Some (projs, _) ->
let pars = mib.Declarations.mind_nparams in
let l1' = Array.sub l1 pars (Array.length l1 - pars) in
- let l2 = Array.map (fun p -> mkProj (p, term)) projs in
+ let l2 = Array.map (fun p -> mkProj (Projection.make p false, term)) projs in
l1', l2
| _ -> assert false)
| _ -> assert false
@@ -666,11 +670,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
| Some l ->
solve_pattern_eqn_array curenvnb f2 l cM substn)
- | App (f1,l1), App (f2,l2) ->
- unify_app curenvnb pb b substn cM f1 l1 cN f2 l2
-
| Proj (p1,c1), Proj (p2,c2) ->
- if eq_constant p1 p2 then
+ if eq_constant (Projection.constant p1) (Projection.constant p2) then
try
let substn = unirec_rec curenvnb CONV true wt substn c1 c2 in
try (* Force unification of the types to fill in parameters *)
@@ -679,6 +680,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
unify_0_with_initial_metas substn true env cv_pb
{ flags with modulo_conv_on_closed_terms = Some full_transparent_state;
modulo_delta = full_transparent_state;
+ modulo_eta = true;
modulo_betaiota = true }
ty1 ty2
with RetypeError _ -> substn
@@ -687,6 +689,23 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
else
unify_not_same_head curenvnb pb b wt substn cM cN
+ | App (f1, l1), Proj (p', c) when isConst f1 &&
+ eq_constant (fst (destConst f1)) (Projection.constant p') ->
+ expand curenvnb pb b false substn cM f1 l1 cN cN [||]
+
+ | Proj (p', c), App (f1, l1) when isConst f1 &&
+ eq_constant (fst (destConst f1)) (Projection.constant p') ->
+ expand curenvnb pb b false substn cM f1 l1 cN cN [||]
+
+ | App (f1,l1), App (f2,l2) ->
+ (match kind_of_term f1, kind_of_term f2 with
+ | Const (p, u), Proj (p', c) when eq_constant p (Projection.constant p') ->
+ expand curenvnb pb b false substn cM f1 l1 cN f2 l2
+ | Proj (p', _), Const (p, _) when eq_constant p (Projection.constant p') ->
+ expand curenvnb pb b false substn cM f1 l1 cN f2 l2
+ | _ ->
+ unify_app curenvnb pb b substn cM f1 l1 cN f2 l2)
+
| _ ->
unify_not_same_head curenvnb pb b wt substn cM cN
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 6fa4342d3..564e111e0 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -198,7 +198,7 @@ let strip_params env c =
(match cb.Declarations.const_proj with
| Some pb ->
let n = pb.Declarations.proj_npars in
- mkApp (mkProj (p, args.(n)),
+ mkApp (mkProj (Projection.make p false, args.(n)),
Array.sub args (n+1) (Array.length args - (n + 1)))
| None -> c)
| _ -> c)
@@ -585,7 +585,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
match kind_of_term cty with
| Prod _ -> failwith "make_exact_entry"
| _ ->
- let pat = snd (Patternops.pattern_of_constr sigma cty) in
+ let pat = snd (Patternops.pattern_of_constr env sigma cty) in
let hd =
try head_pattern_bound pat
with BoundPattern -> failwith "make_exact_entry"
@@ -604,7 +604,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
let sigma' = Evd.merge_context_set univ_flexible dummy_goal.sigma ctx in
let ce = mk_clenv_from { dummy_goal with sigma = sigma' } (c,cty) in
let c' = clenv_type (* ~reduce:false *) ce in
- let pat = snd (Patternops.pattern_of_constr sigma c') in
+ let pat = snd (Patternops.pattern_of_constr env sigma c') in
let hd =
try head_pattern_bound pat
with BoundPattern -> failwith "make_apply_entry" in
@@ -701,7 +701,7 @@ let make_trivial env sigma poly ?(name=PathAny) r =
let ce = mk_clenv_from dummy_goal (c,t) in
(Some hd, { pri=1;
poly = poly;
- pat = Some (snd (Patternops.pattern_of_constr sigma (clenv_type ce)));
+ pat = Some (snd (Patternops.pattern_of_constr env sigma (clenv_type ce)));
name = name;
code=Res_pf_THEN_trivial_fail(c,t,ctx) })
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 5fbc6f5b2..ef813744e 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -33,7 +33,7 @@ type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything
let decomp_pat =
let rec decrec acc = function
| PApp (f,args) -> decrec (Array.to_list args @ acc) f
- | PProj (p, c) -> (PRef (ConstRef p), c :: acc)
+ | PProj (p, c) -> (PRef (ConstRef (Projection.constant p)), c :: acc)
| c -> (c,acc)
in
decrec []
@@ -41,7 +41,7 @@ let decomp_pat =
let decomp =
let rec decrec acc c = match kind_of_term c with
| App (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f
- | Proj (p, c) -> (mkConst p, c :: acc)
+ | Proj (p, c) -> (mkConst (Projection.constant p), c :: acc)
| Cast (c1,_,_) -> decrec acc c1
| _ -> (c,acc)
in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e25a862dd..991eac57e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -584,7 +584,7 @@ let interp_pure_open_constr ist =
let interp_typed_pattern ist env sigma (c,_) =
let sigma, c =
interp_gen WithoutTypeConstraint ist true pure_open_constr_flags env sigma c in
- pattern_of_constr sigma c
+ pattern_of_constr env sigma c
(* Interprets a constr expression casted by the current goal *)
let pf_interp_casted_constr ist gl c =
@@ -986,7 +986,7 @@ let eval_pattern lfun ist env sigma (_,pat as c) =
if use_types then
snd (interp_typed_pattern ist env sigma c)
else
- instantiate_pattern sigma lfun pat
+ instantiate_pattern env sigma lfun pat
let read_pattern lfun ist env sigma = function
| Subterm (b,ido,c) -> Subterm (b,ido,eval_pattern lfun ist env sigma c)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 23b649809..69a72db4f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -124,7 +124,7 @@ let head_constr_bound t =
let hd,args = decompose_app ccl in
match kind_of_term hd with
| Const _ | Ind _ | Construct _ | Var _ -> hd
- | Proj (p, _) -> mkConst p
+ | Proj (p, _) -> mkConst (Projection.constant p)
| _ -> raise Bound
let head_constr c =
@@ -139,7 +139,7 @@ let decompose_app_bound t =
| Ind (i,u) -> IndRef i, args
| Construct (c,u) -> ConstructRef c, args
| Var id -> VarRef id, args
- | Proj (p, c) -> ConstRef p, Array.cons c args
+ | Proj (p, c) -> ConstRef (Projection.constant p), Array.cons c args
| _ -> raise Bound
(******************************************)
@@ -1172,7 +1172,7 @@ let make_projection env sigma params cstr sign elim i n c u =
let args = extended_rel_vect 0 sign in
let proj =
if Environ.is_projection proj env then
- mkProj (proj, mkApp (c, args))
+ mkProj (Projection.make proj false, mkApp (c, args))
else
mkApp (mkConstU (proj,u), Array.append (Array.of_list params)
[|mkApp (c, args)|])
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index f8d7a197b..9826ecdff 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -288,7 +288,7 @@ struct
Array.fold_left (fun c a -> Term (DApp (c,a)))
(pat_of_constr f) (Array.map pat_of_constr ca)
| Proj (p,c) ->
- Term (DApp (Term (DRef (ConstRef p)), pat_of_constr c))
+ Term (DApp (Term (DRef (ConstRef (Projection.constant p))), pat_of_constr c))
and ctx_of_constr ctx c = match kind_of_term c with
| Prod (_,t,c) -> ctx_of_constr (Term(DCons((pat_of_constr t,None),ctx))) c
diff --git a/test-suite/bugs/opened/3660.v b/test-suite/bugs/opened/3660.v
index f962e1f04..ed8964ce1 100644
--- a/test-suite/bugs/opened/3660.v
+++ b/test-suite/bugs/opened/3660.v
@@ -18,10 +18,10 @@ admit.
Defined.
Local Open Scope equiv_scope.
Axiom equiv_path : forall (A B : Type) (p : A = B), A <~> B.
+
Goal forall (C D : hSet), IsEquiv (fun x : C = D => (equiv_path C D (ap setT x))).
intros.
change (IsEquiv (equiv_path C D o @ap _ _ setT C D)).
apply @isequiv_compose; [ | admit ].
- solve [ apply isequiv_ap_setT ].
- Undo.
- Fail typeclasses eauto.
+ Set Typeclasses Debug.
+ typeclasses eauto.
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 177aa1cd6..7694869a5 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -266,7 +266,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
(** Already defined in the kernel silently *)
let kn = destConstRef (Nametab.locate (Libnames.qualid_of_ident fid)) in
Declare.definition_message fid;
- kn, mkProj (kn,mkRel 1)
+ kn, mkProj (Projection.make kn false,mkRel 1)
else
let ccl = subst_projection fid subst ti in
let body = match optci with