diff options
Diffstat (limited to 'engine/termops.ml')
| -rw-r--r-- | engine/termops.ml | 18 |
1 files changed, 4 insertions, 14 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index a65b8275e6..16f2a87c1e 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -1066,19 +1066,9 @@ let global_of_constr sigma c = | Var id -> VarRef id, EConstr.EInstance.empty | _ -> raise Not_found -let is_global sigma c t = - let open GlobRef in - match c, EConstr.kind sigma t with - | ConstRef c, Const (c', _) -> Constant.equal c c' - | IndRef i, Ind (i', _) -> eq_ind i i' - | ConstructRef i, Construct (i', _) -> eq_constructor i i' - | VarRef id, Var id' -> Id.equal id id' - | _ -> false +let is_global = EConstr.isRefX -let isGlobalRef sigma c = - match EConstr.kind sigma c with - | Const _ | Ind _ | Construct _ | Var _ -> true - | _ -> false +let isGlobalRef = EConstr.isRef let is_template_polymorphic_ind env sigma f = match EConstr.kind sigma f with |