diff options
Diffstat (limited to 'library/heads.ml')
| -rw-r--r-- | library/heads.ml | 25 |
1 files changed, 14 insertions, 11 deletions
diff --git a/library/heads.ml b/library/heads.ml index 02465f22..198672a0 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -1,14 +1,16 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util open Names -open Term +open Constr open Vars open Mod_subst open Environ @@ -25,7 +27,7 @@ open Context.Named.Declaration the evaluation of [phi(0)] and the head of [h] is declared unknown). *) type rigid_head_kind = -| RigidParameter of constant (* a Const without body *) +| RigidParameter of Constant.t (* a Const without body *) | RigidVar of variable (* a Var without body *) | RigidType (* an inductive, a product or a sort *) @@ -57,7 +59,7 @@ let variable_head id = Evalrefmap.find (EvalVarRef id) !head_map let constant_head cst = Evalrefmap.find (EvalConstRef cst) !head_map let kind_of_head env t = - let rec aux k l t b = match kind_of_term (Reduction.whd_betaiotazeta env t) with + let rec aux k l t b = match kind (Reduction.whd_betaiotazeta env t) with | Rel n when n > k -> NotImmediatelyComputableHead | Rel n -> FlexibleHead (k,k+1-n,List.length l,b) | Var id -> @@ -72,7 +74,8 @@ let kind_of_head env t = with Not_found -> CErrors.anomaly Pp.(str "constant not found in kind_of_head: " ++ - str (Names.Constant.to_string cst))) + Names.Constant.print cst ++ + str ".")) | Construct _ | CoFix _ -> if b then NotImmediatelyComputableHead else ConstructorHead | Sort _ | Ind _ | Prod _ -> RigidHead RigidType @@ -127,11 +130,11 @@ let compute_head = function let is_Def = function Declarations.Def _ -> true | _ -> false in let body = if cb.Declarations.const_proj = None && is_Def cb.Declarations.const_body - then Declareops.body_of_constant (Environ.opaque_tables env) cb else None + then Global.body_of_constant cst else None in (match body with | None -> RigidHead (RigidParameter cst) - | Some c -> kind_of_head env c) + | Some (c, _) -> kind_of_head env c) | EvalVarRef id -> (match Global.lookup_named id with | LocalDef (_,c,_) when not (Decls.variable_opacity id) -> @@ -155,7 +158,7 @@ let cache_head o = let subst_head_approximation subst = function | RigidHead (RigidParameter cst) as k -> let cst,c = subst_con_kn subst cst in - if isConst c && eq_constant (fst (destConst c)) cst then + if isConst c && Constant.equal (fst (destConst c)) cst then (* A change of the prefix of the constant *) k else |