aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/ltac2.md61
-rw-r--r--src/dune10
-rw-r--r--src/tac2core.ml6
-rw-r--r--src/tac2entries.ml4
-rw-r--r--src/tac2ffi.ml2
-rw-r--r--src/tac2intern.ml2
-rw-r--r--src/tac2match.ml2
-rw-r--r--src/tac2print.ml8
-rw-r--r--src/tac2quote.ml2
9 files changed, 81 insertions, 16 deletions
diff --git a/doc/ltac2.md b/doc/ltac2.md
index 9ba227c285..3cee0ac494 100644
--- a/doc/ltac2.md
+++ b/doc/ltac2.md
@@ -17,13 +17,68 @@ Following the need of users that start developing huge projects relying
critically on Ltac, we believe that we should offer a proper modern language
that features at least the following:
-- at least informal, predictible semantics
+- at least informal, predictable semantics
- a typing system
- standard programming facilities (i.e. datatypes)
This document describes the implementation of such a language. The
implementation of Ltac as of Coq 8.7 will be referred to as Ltac1.
+# Contents
+
+<!-- markdown-toc start - Don't edit this section. Run M-x markdown-toc-refresh-toc -->
+**Table of Contents**
+
+- [Summary](#summary)
+- [Contents](#contents)
+- [General design](#general-design)
+- [ML component](#ml-component)
+ - [Overview](#overview)
+ - [Type Syntax](#type-syntax)
+ - [Type declarations](#type-declarations)
+ - [Term Syntax](#term-syntax)
+ - [Ltac Definitions](#ltac-definitions)
+ - [Reduction](#reduction)
+ - [Typing](#typing)
+ - [Effects](#effects)
+ - [Standard IO](#standard-io)
+ - [Fatal errors](#fatal-errors)
+ - [Backtrack](#backtrack)
+ - [Goals](#goals)
+- [Meta-programming](#meta-programming)
+ - [Overview](#overview-1)
+ - [Generic Syntax for Quotations](#generic-syntax-for-quotations)
+ - [Built-in quotations](#built-in-quotations)
+ - [Strict vs. non-strict mode](#strict-vs-non-strict-mode)
+ - [Term Antiquotations](#term-antiquotations)
+ - [Syntax](#syntax)
+ - [Semantics](#semantics)
+ - [Static semantics](#static-semantics)
+ - [Dynamic semantics](#dynamic-semantics)
+ - [Trivial Term Antiquotations](#trivial-term-antiquotations)
+ - [Match over terms](#match-over-terms)
+ - [Match over goals](#match-over-goals)
+- [Notations](#notations)
+ - [Scopes](#scopes)
+ - [Notations](#notations-1)
+ - [Abbreviations](#abbreviations)
+- [Evaluation](#evaluation)
+- [Debug](#debug)
+- [Compatibility layer with Ltac1](#compatibility-layer-with-ltac1)
+ - [Ltac1 from Ltac2](#ltac1-from-ltac2)
+ - [Ltac2 from Ltac1](#ltac2-from-ltac1)
+- [Transition from Ltac1](#transition-from-ltac1)
+ - [Syntax changes](#syntax-changes)
+ - [Tactic delay](#tactic-delay)
+ - [Variable binding](#variable-binding)
+ - [In Ltac expressions](#in-ltac-expressions)
+ - [In quotations](#in-quotations)
+ - [Exception catching](#exception-catching)
+- [TODO](#todo)
+
+<!-- markdown-toc end -->
+
+
# General design
There are various alternatives to Ltac1, such that Mtac or Rtac for instance.
@@ -388,7 +443,7 @@ represent several goals, including none. Thus, there is no such thing as
It is natural to do the same in Ltac2, but we must provide a way to get access
to a given goal. This is the role of the `enter` primitive, that applies a
-tactic to each currently focussed goal in turn.
+tactic to each currently focused goal in turn.
```
val enter : (unit -> unit) -> unit
@@ -634,7 +689,7 @@ bindings, so that there will be a syntax error if one of the bound variables
starts with an uppercase character.
The semantics of this construction is otherwise the same as the corresponding
-one from Ltac1, except that it requires the goal to be focussed.
+one from Ltac1, except that it requires the goal to be focused.
## Match over goals
diff --git a/src/dune b/src/dune
new file mode 100644
index 0000000000..b0140aa809
--- /dev/null
+++ b/src/dune
@@ -0,0 +1,10 @@
+(library
+ (name ltac2)
+ (public_name coq.plugins.ltac2)
+ (modules_without_implementation tac2expr tac2qexpr tac2types)
+ (libraries coq.plugins.firstorder))
+
+(rule
+ (targets g_ltac2.ml)
+ (deps (:pp-file g_ltac2.ml4) )
+ (action (run coqp5 -loc loc -impl %{pp-file} -o %{targets})))
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 6ff353ce30..7384652216 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -20,8 +20,8 @@ open Proofview.Notations
module Value = Tac2ffi
open Value
-let std_core n = KerName.make2 Tac2env.std_prefix (Label.of_id (Id.of_string_soft n))
-let coq_core n = KerName.make2 Tac2env.coq_prefix (Label.of_id (Id.of_string_soft n))
+let std_core n = KerName.make Tac2env.std_prefix (Label.of_id (Id.of_string_soft n))
+let coq_core n = KerName.make Tac2env.coq_prefix (Label.of_id (Id.of_string_soft n))
module Core =
struct
@@ -781,7 +781,7 @@ let () = define1 "progress" closure begin fun f ->
end
let () = define2 "abstract" (option ident) closure begin fun id f ->
- Tactics.tclABSTRACT id (Proofview.tclIGNORE (thaw f)) >>= fun () ->
+ Abstract.tclABSTRACT id (Proofview.tclIGNORE (thaw f)) >>= fun () ->
return v_unit
end
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index ec10dea777..bba4680a72 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -805,7 +805,7 @@ let pr_frame = function
let () = register_handler begin function
| Tac2interp.LtacError (kn, args) ->
- let t_exn = KerName.make2 Tac2env.coq_prefix (Label.make "exn") in
+ let t_exn = KerName.make Tac2env.coq_prefix (Label.make "exn") in
let v = Tac2ffi.of_open (kn, args) in
let t = GTypRef (Other t_exn, []) in
let c = Tac2print.pr_valexpr (Global.env ()) Evd.empty v t in
@@ -897,7 +897,7 @@ let register_prim_alg name params def =
let def = { typdef_local = false; typdef_expr = def } in
ignore (Lib.add_leaf id (inTypDef def))
-let coq_def n = KerName.make2 Tac2env.coq_prefix (Label.make n)
+let coq_def n = KerName.make Tac2env.coq_prefix (Label.make n)
let def_unit = {
typdef_local = false;
diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index a719970a57..df1857c3e7 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -229,7 +229,7 @@ let internal_err =
let coq_prefix =
MPfile (DirPath.make (List.map Id.of_string ["Init"; "Ltac2"]))
in
- KerName.make2 coq_prefix (Label.of_id (Id.of_string "Internal"))
+ KerName.make coq_prefix (Label.of_id (Id.of_string "Internal"))
(** FIXME: handle backtrace in Ltac2 exceptions *)
let of_exn c = match fst c with
diff --git a/src/tac2intern.ml b/src/tac2intern.ml
index ff8fb4c0f4..fe615853ce 100644
--- a/src/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -19,7 +19,7 @@ open Tac2expr
(** Hardwired types and constants *)
-let coq_type n = KerName.make2 Tac2env.coq_prefix (Label.make n)
+let coq_type n = KerName.make Tac2env.coq_prefix (Label.make n)
let t_int = coq_type "int"
let t_string = coq_type "string"
diff --git a/src/tac2match.ml b/src/tac2match.ml
index a3140eabea..c9e549d47e 100644
--- a/src/tac2match.ml
+++ b/src/tac2match.ml
@@ -181,7 +181,7 @@ module PatternMatching (E:StaticEnvironment) = struct
pattern_match_term pat (NamedDecl.get_type decl) >>= fun ctx ->
return (id, ctx)
- let hyp_match_body_and_type bodypat typepat hyps =
+ let _hyp_match_body_and_type bodypat typepat hyps =
pick hyps >>= function
| LocalDef (id,body,hyp) ->
pattern_match_term bodypat body >>= fun ctx_body ->
diff --git a/src/tac2print.ml b/src/tac2print.ml
index 0fea07ee3a..0b20cf9f58 100644
--- a/src/tac2print.ml
+++ b/src/tac2print.ml
@@ -22,7 +22,7 @@ let change_kn_label kn id =
let paren p = hov 2 (str "(" ++ p ++ str ")")
let t_list =
- KerName.make2 Tac2env.coq_prefix (Label.of_id (Id.of_string "list"))
+ KerName.make Tac2env.coq_prefix (Label.of_id (Id.of_string "list"))
(** Type printing *)
@@ -35,7 +35,7 @@ type typ_level =
| T0
let t_unit =
- KerName.make2 Tac2env.coq_prefix (Label.of_id (Id.of_string "unit"))
+ KerName.make Tac2env.coq_prefix (Label.of_id (Id.of_string "unit"))
let pr_typref kn =
Libnames.pr_qualid (Tac2env.shortest_qualid_of_type kn)
@@ -435,7 +435,7 @@ and pr_val_list env sigma args tpe =
str "[" ++ prlist_with_sep pr_semicolon pr args ++ str "]"
let register_init n f =
- let kn = KerName.make2 Tac2env.coq_prefix (Label.make n) in
+ let kn = KerName.make Tac2env.coq_prefix (Label.make n) in
register_val_printer kn { val_printer = fun env sigma v _ -> f env sigma v }
let () = register_init "int" begin fun _ _ n ->
@@ -476,7 +476,7 @@ let () = register_init "err" begin fun _ _ e ->
end
let () =
- let kn = KerName.make2 Tac2env.coq_prefix (Label.make "array") in
+ let kn = KerName.make Tac2env.coq_prefix (Label.make "array") in
let val_printer env sigma v arg = match arg with
| [arg] ->
let (_, v) = to_block v in
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index 1d742afd83..3bddfe7594 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -32,7 +32,7 @@ let control_prefix = prefix_gen "Control"
let pattern_prefix = prefix_gen "Pattern"
let array_prefix = prefix_gen "Array"
-let kername prefix n = KerName.make2 prefix (Label.of_id (Id.of_string_soft n))
+let kername prefix n = KerName.make prefix (Label.of_id (Id.of_string_soft n))
let std_core n = kername Tac2env.std_prefix n
let coq_core n = kername Tac2env.coq_prefix n
let control_core n = kername control_prefix n
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 21:48:22 +0000