aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-11-12 01:52:15 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-02-14 17:28:48 +0100
commit771be16883c8c47828f278ce49545716918764c4 (patch)
treef3c0427596d447677c54c23455fcfbe7e3337b49 /engine
parent45562afa065aadc207dca4e904e309d835cb66ef (diff)
Hipattern API using EConstr.
Diffstat (limited to 'engine')
-rw-r--r--engine/termops.ml9
-rw-r--r--engine/termops.mli2
2 files changed, 11 insertions, 0 deletions
diff --git a/engine/termops.ml b/engine/termops.ml
index 5581b1656..59dbb73f5 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -829,6 +829,15 @@ let global_of_constr sigma c =
| Var id -> VarRef id, Univ.Instance.empty
| _ -> raise Not_found
+let is_global sigma c t =
+ let open Globnames 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 isGlobalRef sigma c =
match EConstr.kind sigma c with
| Const _ | Ind _ | Construct _ | Var _ -> true
diff --git a/engine/termops.mli b/engine/termops.mli
index 02e8dfeae..abc9caa98 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -268,6 +268,8 @@ val is_section_variable : Id.t -> bool
val global_of_constr : Evd.evar_map -> EConstr.constr -> Globnames.global_reference puniverses
+val is_global : Evd.evar_map -> Globnames.global_reference -> EConstr.constr -> bool
+
val isGlobalRef : Evd.evar_map -> EConstr.t -> bool
val is_template_polymorphic : env -> Evd.evar_map -> EConstr.t -> bool