Evarconv API using EConstr.

1 files changed, 11 insertions, 0 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index 356312e2f6..26b22be4e4 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1068,6 +1068,17 @@ let dependency_closure env sigma sign hyps =
         sign in
     List.rev lh
 
+let global_app_of_constr sigma c =
+  let open Univ in
+  let open Globnames in
+  match EConstr.kind sigma c with
+  | Const (c, u) -> (ConstRef c, u), None
+  | 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 (Projection.constant p), Instance.empty), Some c
+  | _ -> raise Not_found
+
 (* Combinators on judgments *)
 
 let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type }