aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/dune2
-rw-r--r--engine/eConstr.mli2
2 files changed, 3 insertions, 1 deletions
diff --git a/engine/dune b/engine/dune
index e2b7ab9c87..00db94389b 100644
--- a/engine/dune
+++ b/engine/dune
@@ -1,6 +1,6 @@
(library
(name engine)
(synopsis "Coq's Tactic Engine")
- (public_name coq.engine)
+ (public_name coq-core.engine)
(wrapped false)
(libraries library))
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 0d038e9a67..162d189136 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -365,6 +365,8 @@ val to_rel_decl : Evd.evar_map -> (t, types) Context.Rel.Declaration.pt -> (Cons
val of_case_invert : Constr.case_invert -> case_invert
+val of_constr_array : Constr.t array -> t array
+
(** {5 Unsafe operations} *)
module Unsafe :