Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions docs/development.md
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@
- Debug: Helpers for debug logging
- Hipcore: core language and spec AST and pure functions for manipulating it
- Hipcore_typed: core language and spec AST with type annotations
- Hipcore_common: libraries and definitions common to both the untyped and typed ASTs
- Provers: prover back ends which translate Hipcore types into SMT
- Hipprover: code which depends on calls to an external prover, e.g. normalization
- Ocamlfrontend: OCaml parser
Expand Down
1 change: 1 addition & 0 deletions lib/heifer-parsing/core_lang.ml
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ open Types
exception Foo of string

let rec get_tactic e =
let open Hipcore_common.Tactics in

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I am not sure whether this tactic is still relevant. But we can keep it there.

match e with
| { pexp_desc = Pexp_ident { txt = Lident "unfold_right"; _ }; _ } ->
[Unfold_right]
Expand Down
1 change: 1 addition & 0 deletions lib/heifer-parsing/core_lang_typed.ml
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ open Typedhip
exception Foo of string

let rec get_tactic e =
let open Hipcore_common.Tactics in
let open Parsetree in
match e with
| { pexp_desc = Pexp_ident { txt = Lident "unfold_right"; _ }; _ } ->
Expand Down
96 changes: 0 additions & 96 deletions lib/hipcore/common.ml

This file was deleted.

4 changes: 2 additions & 2 deletions lib/hipcore/dune
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(library
(name hipcore)
(public_name heifer.hipcore)
(modules subst pretty common hiptypes syntax variables types)
(libraries debug unionFind str ocaml_compiler utils)
(modules subst pretty hiptypes syntax variables types untyped_core_ast)
(libraries debug unionFind str ocaml_compiler utils hipcore_common)
(inline_tests)
(preprocess (pps ppx_expect ppx_deriving.std visitors.ppx)))
Loading