From f258a877d25c1f6a27875f26d9ea1fe0a5fb5b81 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 22 Nov 2019 11:35:04 +0100 Subject: [CS] Allow a variable introduced with Let to be a canonical instance --- .../07-commands-and-options/11164-let-cs.rst | 1 + pretyping/recordops.ml | 77 +++++++++++++--------- pretyping/recordops.mli | 8 ++- test-suite/success/CanonicalStructure.v | 8 +++ vernac/canonical.ml | 8 ++- 5 files changed, 65 insertions(+), 37 deletions(-) create mode 100644 doc/changelog/07-commands-and-options/11164-let-cs.rst diff --git a/doc/changelog/07-commands-and-options/11164-let-cs.rst b/doc/changelog/07-commands-and-options/11164-let-cs.rst new file mode 100644 index 0000000000..b9ecd140e7 --- /dev/null +++ b/doc/changelog/07-commands-and-options/11164-let-cs.rst @@ -0,0 +1 @@ +- A section variable introduces with :g:`Let` can be declared as a :g:`Canonical Structure` (`#11164 `_, by Enrico Tassi). diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 5b416a99f9..53a252f459 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -19,7 +19,7 @@ open CErrors open Util open Pp open Names -open Globnames +open GlobRef open Constr open Mod_subst open Reductionops @@ -80,7 +80,7 @@ let subst_structure subst (id, kl, projs as obj) = (Option.Smart.map (subst_constant subst)) projs in - let id' = subst_constructor subst id in + let id' = Globnames.subst_constructor subst id in if projs' == projs && id' == id then obj else (id',kl,projs') @@ -89,11 +89,11 @@ let lookup_structure indsp = Indmap.find indsp !structure_table let lookup_projections indsp = (lookup_structure indsp).s_PROJ let find_projection_nparams = function - | GlobRef.ConstRef cst -> (Cmap.find cst !projection_table).s_EXPECTEDPARAM + | ConstRef cst -> (Cmap.find cst !projection_table).s_EXPECTEDPARAM | _ -> raise Not_found let find_projection = function - | GlobRef.ConstRef cst -> Cmap.find cst !projection_table + | ConstRef cst -> Cmap.find cst !projection_table | _ -> raise Not_found let is_projection cst = Cmap.mem cst !projection_table @@ -185,27 +185,32 @@ let rec cs_pattern_of_constr env t = | Proj (p, c) -> let { Environ.uj_type = ty } = Typeops.infer env c in let _, params = Inductive.find_rectype env ty in - Const_cs (GlobRef.ConstRef (Projection.constant p)), None, params @ [c] + Const_cs (ConstRef (Projection.constant p)), None, params @ [c] | Sort s -> Sort_cs (Sorts.family s), None, [] - | _ -> Const_cs (global_of_constr t) , None, [] + | _ -> Const_cs (Globnames.global_of_constr t) , None, [] let warn_projection_no_head_constant = CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker" - (fun (sign,env,t,con,proji_sp) -> + (fun (sign,env,t,ref,proji_sp) -> let env = Termops.push_rels_assum sign env in - let con_pp = Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef con) in - let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef proji_sp) in + let con_pp = Nametab.pr_global_env Id.Set.empty ref in + let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in let term_pp = Termops.Internal.print_constr_env env (Evd.from_env env) (EConstr.of_constr t) in strbrk "Projection value has no head constant: " ++ term_pp ++ strbrk " in canonical instance " ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.") (* Intended to always succeed *) -let compute_canonical_projections env ~warn (con,ind) = - let o_CTX = Environ.constant_context env con in - let u = Univ.make_abstract_instance o_CTX in - let o_DEF = mkConstU (con, u) in - let c = Environ.constant_value_in env (con,u) in +let compute_canonical_projections env ~warn (gref,ind) = + let o_CTX = Environ.universes_of_global env gref in + let o_DEF, c = + match gref with + | ConstRef con -> + let u = Univ.make_abstract_instance o_CTX in + mkConstU (con, u), Environ.constant_value_in env (con,u) + | VarRef id -> + mkVar id, Option.get (Environ.named_body id env) + | ConstructRef _ | IndRef _ -> assert false in let sign,t = Reductionops.splay_lam env (Evd.from_env env) (EConstr.of_constr c) in let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in let t = EConstr.Unsafe.to_constr t in @@ -223,11 +228,11 @@ let compute_canonical_projections env ~warn (con,ind) = Option.cata (fun proji_sp -> match cs_pattern_of_constr nenv t with | patt, o_INJ, o_TCOMPS -> - ((GlobRef.ConstRef proji_sp, (patt, t)), + ((ConstRef proji_sp, (patt, t)), { o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS }) :: acc | exception Not_found -> - if warn then warn_projection_no_head_constant (sign, env, t, con, proji_sp); + if warn then warn_projection_no_head_constant (sign, env, t, gref, proji_sp); acc ) acc spopt else acc @@ -263,12 +268,17 @@ let register_canonical_structure ~warn env sigma o = warn_redundant_canonical_projection (hd_val, prj, new_can_s, old_can_s) ) -let subst_canonical_structure subst (cst,ind as obj) = +type cs = GlobRef.t * inductive + +let subst_canonical_structure subst (gref,ind as obj) = (* invariant: cst is an evaluable reference. Thus we can take *) (* the first component of subst_con. *) - let cst' = subst_constant subst cst in - let ind' = subst_ind subst ind in - if cst' == cst && ind' == ind then obj else (cst',ind') + match gref with + | ConstRef cst -> + let cst' = subst_constant subst cst in + let ind' = subst_ind subst ind in + if cst' == cst && ind' == ind then obj else (ConstRef cst',ind') + | _ -> assert false (*s High-level declaration of a canonical structure *) @@ -279,15 +289,20 @@ let error_not_structure ref description = description)) let check_and_decompose_canonical_structure env sigma ref = - let sp = + let vc = match ref with - GlobRef.ConstRef sp -> sp - | _ -> error_not_structure ref (str "Expected an instance of a record or structure.") + | ConstRef sp -> + let u = Univ.make_abstract_instance (Environ.constant_context env sp) in + begin match Environ.constant_opt_value_in env (sp, u) with + | Some vc -> vc + | None -> error_not_structure ref (str "Could not find its value in the global environment.") end + | VarRef id -> + begin match Environ.named_body id env with + | Some b -> b + | None -> error_not_structure ref (str "Could not find its value in the global environment.") end + | IndRef _ | ConstructRef _ -> + error_not_structure ref (str "Expected an instance of a record or structure.") in - let u = Univ.make_abstract_instance (Environ.constant_context env sp) in - let vc = match Environ.constant_opt_value_in env (sp, u) with - | Some vc -> vc - | None -> error_not_structure ref (str "Could not find its value in the global environment.") in let body = snd (splay_lam env sigma (EConstr.of_constr vc)) in let body = EConstr.Unsafe.to_constr body in let f,args = match kind body with @@ -305,7 +320,7 @@ let check_and_decompose_canonical_structure env sigma ref = let ntrue_projs = List.count (fun { pk_true_proj } -> pk_true_proj) s.s_PROJKIND in if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then error_not_structure ref (str "Got too few arguments to the record or structure constructor."); - (sp,indsp) + (ref,indsp) let lookup_canonical_conversion (proj,pat) = assoc_pat pat (GlobRef.Map.find proj !object_table) @@ -313,13 +328,13 @@ let lookup_canonical_conversion (proj,pat) = let decompose_projection sigma c args = match EConstr.kind sigma c with | Const (c, u) -> - let n = find_projection_nparams (GlobRef.ConstRef c) in + let n = find_projection_nparams (ConstRef c) in (* Check if there is some canonical projection attached to this structure *) - let _ = GlobRef.Map.find (GlobRef.ConstRef c) !object_table in + let _ = GlobRef.Map.find (ConstRef c) !object_table in let arg = Stack.nth args n in arg | Proj (p, c) -> - let _ = GlobRef.Map.find (GlobRef.ConstRef (Projection.constant p)) !object_table in + let _ = GlobRef.Map.find (ConstRef (Projection.constant p)) !object_table in c | _ -> raise Not_found diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index e8b0d771aa..e8450323f4 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -86,13 +86,15 @@ val cs_pattern_of_constr : Environ.env -> constr -> cs_pattern * int option * co val pr_cs_pattern : cs_pattern -> Pp.t +type cs = GlobRef.t * inductive + val lookup_canonical_conversion : (GlobRef.t * cs_pattern) -> constr * obj_typ val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map -> - Constant.t * inductive -> unit -val subst_canonical_structure : Mod_subst.substitution -> Constant.t * inductive -> Constant.t * inductive + cs -> unit +val subst_canonical_structure : Mod_subst.substitution -> cs -> cs val is_open_canonical_projection : Environ.env -> Evd.evar_map -> Reductionops.state -> bool val canonical_projections : unit -> ((GlobRef.t * cs_pattern) * obj_typ) list -val check_and_decompose_canonical_structure : Environ.env -> Evd.evar_map -> GlobRef.t -> Constant.t * inductive +val check_and_decompose_canonical_structure : Environ.env -> Evd.evar_map -> GlobRef.t -> cs diff --git a/test-suite/success/CanonicalStructure.v b/test-suite/success/CanonicalStructure.v index e6d674c1e6..bedb79d4d4 100644 --- a/test-suite/success/CanonicalStructure.v +++ b/test-suite/success/CanonicalStructure.v @@ -51,3 +51,11 @@ Fail Check (refl_equal _ : l _ = x2). Check s0. Check s1. Check s2. + +Section Y. + Let s3 := MKL x3. + Canonical Structure s3. + Check (refl_equal _ : l _ = x3). +End Y. +Fail Check (refl_equal _ : l _ = x3). +Fail Check s3. diff --git a/vernac/canonical.ml b/vernac/canonical.ml index 141b02ef63..e41610b532 100644 --- a/vernac/canonical.ml +++ b/vernac/canonical.ml @@ -21,10 +21,12 @@ let cache_canonical_structure (_, (o,_)) = let sigma = Evd.from_env env in register_canonical_structure ~warn:true env sigma o -let discharge_canonical_structure (_,(x, local)) = - if local then None else Some (x, local) +let discharge_canonical_structure (_,((gref, _ as x), local)) = + if local || (Globnames.isVarRef gref && Lib.is_in_section gref) then None + else Some (x, local) -let inCanonStruc : (Constant.t * inductive) * bool -> obj = + +let inCanonStruc : (GlobRef.t * inductive) * bool -> obj = declare_object {(default_object "CANONICAL-STRUCTURE") with open_function = open_canonical_structure; cache_function = cache_canonical_structure; -- cgit v1.2.3 From 559c4c068120cf7fd24728df001ca5b631eb3879 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 22 Nov 2019 15:10:16 +0100 Subject: [Attributes] accept #[canonical] (Let|Definition) --- doc/sphinx/language/gallina-extensions.rst | 3 +++ doc/sphinx/language/gallina-specification-language.rst | 11 +++++++++++ test-suite/success/CanonicalStructure.v | 11 +++++++++++ vernac/attributes.ml | 4 +++- vernac/attributes.mli | 3 ++- vernac/g_vernac.mlg | 2 +- vernac/vernacentries.ml | 17 +++++++++++------ 7 files changed, 42 insertions(+), 9 deletions(-) diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 8caa289a47..05e4cf1346 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1994,6 +1994,8 @@ Deactivation of implicit arguments for parsing to be given as if no arguments were implicit. By symmetry, this also affects printing. +.. _canonical-structure-declaration: + Canonical structures ~~~~~~~~~~~~~~~~~~~~ @@ -2004,6 +2006,7 @@ value. The complete documentation of canonical structures can be found in :ref:`canonicalstructures`; here only a simple example is given. .. cmd:: {? Local | #[local] } Canonical {? Structure } @qualid + :name: Canonical Structure This command declares :token:`qualid` as a canonical instance of a structure (a record). When the :g:`#[local]` attribute is given the effect diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 3cc101d06b..ac34fc707a 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1691,6 +1691,17 @@ variety of commands: :n:`@string__1` is the actual notation, :n:`@string__2` is the version number, :n:`@string__3` is the note. +``canonical`` + This attribute can decorate a :cmd:`Definition` or :cmd:`Let` command. + It is equivalent to having a :cmd:`Canonical Structure` declaration just + after the command. + + This attirbute can take the value ``false`` when decorating a record field + declaration with the effect of preventing the field from being involved in + the inference of canonical instances. + + See also :ref:`canonical-structure-declaration`. + .. example:: .. coqtop:: all reset warn diff --git a/test-suite/success/CanonicalStructure.v b/test-suite/success/CanonicalStructure.v index bedb79d4d4..88702a6e80 100644 --- a/test-suite/success/CanonicalStructure.v +++ b/test-suite/success/CanonicalStructure.v @@ -59,3 +59,14 @@ Section Y. End Y. Fail Check (refl_equal _ : l _ = x3). Fail Check s3. + +Section V. + #[canonical] Let s3 := MKL x3. + Check (refl_equal _ : l _ = x3). +End V. + +Section W. + #[canonical, local] Definition s2' := MKL x2. + Check (refl_equal _ : l _ = x2). +End W. +Fail Check (refl_equal _ : l _ = x2). diff --git a/vernac/attributes.ml b/vernac/attributes.ml index b7a3b002bd..68d2c3a00d 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -234,5 +234,7 @@ let only_polymorphism atts = parse polymorphic atts let vernac_polymorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagEmpty] let vernac_monomorphic_flag = ukey, VernacFlagList ["monomorphic", VernacFlagEmpty] -let canonical = +let canonical_field = enable_attribute ~key:"canonical" ~default:(fun () -> true) +let canonical_instance = + enable_attribute ~key:"canonical" ~default:(fun () -> false) diff --git a/vernac/attributes.mli b/vernac/attributes.mli index 34ff15ca7d..0074db66d3 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -48,7 +48,8 @@ val program : bool attribute val template : bool option attribute val locality : bool option attribute val deprecation : Deprecation.t option attribute -val canonical : bool attribute +val canonical_field : bool attribute +val canonical_instance : bool attribute val program_mode_option_name : string list (** For internal use when messing with the global option. *) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 436648c163..975da64529 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -471,7 +471,7 @@ GRAMMAR EXTEND Gram [ [ attr = LIST0 quoted_attributes ; bd = record_binder; rf_priority = OPT [ "|"; n = natural -> { n } ]; rf_notation = decl_notation -> { - let rf_canonical = attr |> List.flatten |> parse canonical in + let rf_canonical = attr |> List.flatten |> parse canonical_field in let rf_subclass, rf_decl = bd in rf_decl, { rf_subclass ; rf_priority ; rf_notation ; rf_canonical } } ] ] ; diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 604d1b28ff..0acc2dd07c 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -63,14 +63,15 @@ module DefAttributes = struct polymorphic : bool; program : bool; deprecated : Deprecation.t option; + canonical_instance : bool; } let parse f = let open Attributes in - let ((locality, deprecated), polymorphic), program = - parse Notations.(locality ++ deprecation ++ polymorphic ++ program) f + let (((locality, deprecated), polymorphic), program), canonical_instance = + parse Notations.(locality ++ deprecation ++ polymorphic ++ program ++ canonical_instance) f in - { polymorphic; program; locality; deprecated } + { polymorphic; program; locality; deprecated; canonical_instance } end let module_locality = Attributes.Notations.(locality >>= fun l -> return (make_module_locality l)) @@ -522,13 +523,17 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms = in start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl -let vernac_definition_hook ~local ~poly = let open Decls in function +let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in function | Coercion -> Some (ComCoercion.add_coercion_hook ~poly) | CanonicalStructure -> Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref))) | SubClass -> Some (ComCoercion.add_subclass_hook ~poly) +| Definition when canonical_instance -> + Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref))) +| Let when canonical_instance -> + Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure dref))) | _ -> None let fresh_name_for_anonymous_theorem () = @@ -551,7 +556,7 @@ let vernac_definition_name lid local = let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t = let open DefAttributes in let local = enforce_locality_exp atts.locality discharge in - let hook = vernac_definition_hook ~local:atts.locality ~poly:atts.polymorphic kind in + let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic kind in let program_mode = atts.program in let poly = atts.polymorphic in let name = vernac_definition_name lid local in @@ -560,7 +565,7 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t = let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt = let open DefAttributes in let scope = enforce_locality_exp atts.locality discharge in - let hook = vernac_definition_hook ~local:atts.locality ~poly:atts.polymorphic kind in + let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic kind in let program_mode = atts.program in let name = vernac_definition_name lid scope in let red_option = match red_option with -- cgit v1.2.3 From 0a4715831a9b1a4a140594af923c7dc03e04060d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 24 Dec 2019 09:18:17 +0100 Subject: [recordops] do not open GlobRef --- pretyping/recordops.ml | 33 ++++++++++++++++----------------- 1 file changed, 16 insertions(+), 17 deletions(-) diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 53a252f459..f722b9f1c7 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -19,7 +19,6 @@ open CErrors open Util open Pp open Names -open GlobRef open Constr open Mod_subst open Reductionops @@ -89,11 +88,11 @@ let lookup_structure indsp = Indmap.find indsp !structure_table let lookup_projections indsp = (lookup_structure indsp).s_PROJ let find_projection_nparams = function - | ConstRef cst -> (Cmap.find cst !projection_table).s_EXPECTEDPARAM + | GlobRef.ConstRef cst -> (Cmap.find cst !projection_table).s_EXPECTEDPARAM | _ -> raise Not_found let find_projection = function - | ConstRef cst -> Cmap.find cst !projection_table + | GlobRef.ConstRef cst -> Cmap.find cst !projection_table | _ -> raise Not_found let is_projection cst = Cmap.mem cst !projection_table @@ -185,7 +184,7 @@ let rec cs_pattern_of_constr env t = | Proj (p, c) -> let { Environ.uj_type = ty } = Typeops.infer env c in let _, params = Inductive.find_rectype env ty in - Const_cs (ConstRef (Projection.constant p)), None, params @ [c] + Const_cs (GlobRef.ConstRef (Projection.constant p)), None, params @ [c] | Sort s -> Sort_cs (Sorts.family s), None, [] | _ -> Const_cs (Globnames.global_of_constr t) , None, [] @@ -194,7 +193,7 @@ let warn_projection_no_head_constant = (fun (sign,env,t,ref,proji_sp) -> let env = Termops.push_rels_assum sign env in let con_pp = Nametab.pr_global_env Id.Set.empty ref in - let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in + let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef proji_sp) in let term_pp = Termops.Internal.print_constr_env env (Evd.from_env env) (EConstr.of_constr t) in strbrk "Projection value has no head constant: " ++ term_pp ++ strbrk " in canonical instance " @@ -205,12 +204,12 @@ let compute_canonical_projections env ~warn (gref,ind) = let o_CTX = Environ.universes_of_global env gref in let o_DEF, c = match gref with - | ConstRef con -> + | GlobRef.ConstRef con -> let u = Univ.make_abstract_instance o_CTX in mkConstU (con, u), Environ.constant_value_in env (con,u) - | VarRef id -> + | GlobRef.VarRef id -> mkVar id, Option.get (Environ.named_body id env) - | ConstructRef _ | IndRef _ -> assert false in + | GlobRef.ConstructRef _ | GlobRef.IndRef _ -> assert false in let sign,t = Reductionops.splay_lam env (Evd.from_env env) (EConstr.of_constr c) in let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in let t = EConstr.Unsafe.to_constr t in @@ -228,7 +227,7 @@ let compute_canonical_projections env ~warn (gref,ind) = Option.cata (fun proji_sp -> match cs_pattern_of_constr nenv t with | patt, o_INJ, o_TCOMPS -> - ((ConstRef proji_sp, (patt, t)), + ((GlobRef.ConstRef proji_sp, (patt, t)), { o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS }) :: acc | exception Not_found -> @@ -274,10 +273,10 @@ let subst_canonical_structure subst (gref,ind as obj) = (* invariant: cst is an evaluable reference. Thus we can take *) (* the first component of subst_con. *) match gref with - | ConstRef cst -> + | GlobRef.ConstRef cst -> let cst' = subst_constant subst cst in let ind' = subst_ind subst ind in - if cst' == cst && ind' == ind then obj else (ConstRef cst',ind') + if cst' == cst && ind' == ind then obj else (GlobRef.ConstRef cst',ind') | _ -> assert false (*s High-level declaration of a canonical structure *) @@ -291,16 +290,16 @@ let error_not_structure ref description = let check_and_decompose_canonical_structure env sigma ref = let vc = match ref with - | ConstRef sp -> + | GlobRef.ConstRef sp -> let u = Univ.make_abstract_instance (Environ.constant_context env sp) in begin match Environ.constant_opt_value_in env (sp, u) with | Some vc -> vc | None -> error_not_structure ref (str "Could not find its value in the global environment.") end - | VarRef id -> + | GlobRef.VarRef id -> begin match Environ.named_body id env with | Some b -> b | None -> error_not_structure ref (str "Could not find its value in the global environment.") end - | IndRef _ | ConstructRef _ -> + | GlobRef.IndRef _ | GlobRef.ConstructRef _ -> error_not_structure ref (str "Expected an instance of a record or structure.") in let body = snd (splay_lam env sigma (EConstr.of_constr vc)) in @@ -328,13 +327,13 @@ let lookup_canonical_conversion (proj,pat) = let decompose_projection sigma c args = match EConstr.kind sigma c with | Const (c, u) -> - let n = find_projection_nparams (ConstRef c) in + let n = find_projection_nparams (GlobRef.ConstRef c) in (* Check if there is some canonical projection attached to this structure *) - let _ = GlobRef.Map.find (ConstRef c) !object_table in + let _ = GlobRef.Map.find (GlobRef.ConstRef c) !object_table in let arg = Stack.nth args n in arg | Proj (p, c) -> - let _ = GlobRef.Map.find (ConstRef (Projection.constant p)) !object_table in + let _ = GlobRef.Map.find (GlobRef.ConstRef (Projection.constant p)) !object_table in c | _ -> raise Not_found -- cgit v1.2.3