aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/build/windows/makecoq_mingw.sh2
-rw-r--r--doc/sphinx/language/gallina-specification-language.rst27
-rw-r--r--doc/sphinx/proof-engine/ltac.rst1
-rw-r--r--plugins/ltac/evar_tactics.ml2
-rw-r--r--plugins/ltac/tacinterp.ml14
-rw-r--r--plugins/ssr/ssrfwd.ml4
-rw-r--r--plugins/ssr/ssrtacticals.ml4
-rw-r--r--tactics/tactics.ml28
-rw-r--r--tactics/tactics.mli2
9 files changed, 70 insertions, 14 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 8a49b97dac..2a29b0d3b6 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -878,7 +878,7 @@ function make_num {
function make_findlib {
make_ocaml
- if build_prep https://opam.ocaml.org/archives ocamlfind.1.8.0+opam tar.gz 1 ; then
+ if build_prep https://opam.ocaml.org/1.2.2/archives ocamlfind.1.8.0+opam tar.gz 1 ; then
logn configure ./configure -bindir "$PREFIXOCAML\\bin" -sitelib "$PREFIXOCAML\\libocaml\\site-lib" -config "$PREFIXOCAML\\etc\\findlib.conf"
# Note: findlib doesn't support -j 8, so don't pass MAKE_OPT
log2 make all
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 075235a8e2..ad7b5c82fd 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -216,6 +216,11 @@ numbers (see :ref:`datatypes`).
Negative integers are not at the same level as :token:`num`, for this
would make precedence unnatural.
+.. index::
+ single: Set (sort)
+ single: Prop
+ single: Type
+
Sorts
-----
@@ -262,6 +267,8 @@ fun and forall gets identical. Moreover, parentheses can be omitted in
the case of a single sequence of bindings sharing the same type (e.g.:
:g:`fun (x y z : A) => t` can be shortened in :g:`fun x y z : A => t`).
+.. index:: fun ... => ...
+
Abstractions
------------
@@ -282,6 +289,8 @@ a let-binder occurs in
the list of binders, it is expanded to a let-in definition (see
Section :ref:`let-in`).
+.. index:: forall
+
Products
--------
@@ -320,6 +329,11 @@ The notation :n:`(@ident := @term)` for arguments is used for making
explicit the value of implicit arguments (see
Section :ref:`explicit-applications`).
+.. index::
+ single: ... : ... (type cast)
+ single: ... <: ...
+ single: ... <<: ...
+
Type cast
---------
@@ -329,6 +343,11 @@ the type of :token:`term` to be :token:`type`.
:n:`@term <: @type` locally sets up the virtual machine for checking that
:token:`term` has type :token:`type`.
+:n:`@term <<: @type` uses native compilation for checking that :token:`term`
+has type :token:`type`.
+
+.. index:: _
+
Inferable subterms
------------------
@@ -336,6 +355,8 @@ Expressions often contain redundant pieces of information. Subterms that can be
automatically inferred by Coq can be replaced by the symbol ``_`` and Coq will
guess the missing piece of information.
+.. index:: let ... := ... (term)
+
.. _let-in:
Let-in definitions
@@ -347,6 +368,8 @@ denotes the local binding of :token:`term` to the variable
definition of functions: :n:`let @ident {+ @binder} := @term in @term’`
stands for :n:`let @ident := fun {+ @binder} => @term in @term’`.
+.. index:: match ... with ...
+
Definition by case analysis
---------------------------
@@ -467,6 +490,10 @@ There are specific notations for case analysis on types with one or two
constructors: ``if … then … else …`` and ``let (…,…) := … in …`` (see
Sections :ref:`if-then-else` and :ref:`irrefutable-patterns`).
+.. index::
+ single: fix
+ single: cofix
+
Recursive functions
-------------------
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 70d46e034a..1fc267488c 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -717,6 +717,7 @@ Local definitions
Local definitions can be done as follows:
.. tacn:: let @ident__1 := @expr__1 {* with @ident__i := @expr__i} in @expr
+ :name: let ... := ...
each :n:`@expr__i` is evaluated to :n:`v__i`, then, :n:`@expr` is evaluated
by substituting :n:`v__i` to each occurrence of :n:`@ident__i`, for
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 84f13d2131..73490a2dfd 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -94,7 +94,7 @@ let let_evar name typ =
in
let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Namegen.IntroFresh id) typ in
Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
- (Tactics.letin_tac None (Name.Name id) evar None Locusops.nowhere)
+ (Tactics.pose_tac (Name.Name id) evar)
end
let hget_evar n =
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index f4313a8fa3..71da6c7667 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1664,16 +1664,18 @@ and interp_atomic ist tac : unit Proofview.tactic =
(* We try to fully-typecheck the term *)
let flags = open_constr_use_classes_flags () in
let (sigma,c_interp) = interp_open_constr ~flags ist env sigma c in
- let let_tac b na c cl eqpat =
- let id = Option.default (make IntroAnonymous) eqpat in
- let with_eq = if b then None else Some (true,id) in
- Tactics.letin_tac with_eq na c None cl
- in
let na = interp_name ist env sigma na in
+ let let_tac =
+ if b then Tactics.pose_tac na c_interp
+ else
+ let id = Option.default (make IntroAnonymous) eqpat in
+ let with_eq = Some (true, id) in
+ Tactics.letin_tac with_eq na c_interp None Locusops.nowhere
+ in
Tacticals.New.tclWITHHOLES ev
(name_atomic ~env
(TacLetTac(ev,na,c_interp,clp,b,eqpat))
- (let_tac b na c_interp clp eqpat)) sigma
+ let_tac) sigma
else
(* We try to keep the pattern structure as much as possible *)
let let_pat_tac b na c cl eqpat =
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index e367cd32d6..f67cf20e49 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -25,9 +25,7 @@ module RelDecl = Context.Rel.Declaration
(** 8. Forward chaining tactics (pose, set, have, suffice, wlog) *)
(** Defined identifier *)
-
-let settac id c = Tactics.letin_tac None (Name id) c None
-let posetac id cl = Proofview.V82.of_tactic (settac id cl Locusops.nowhere)
+let posetac id cl = Proofview.V82.of_tactic (Tactics.pose_tac (Name id) cl)
let ssrposetac (id, (_, t)) gl =
let ist, t =
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 83581f3416..f12f9fac0f 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -14,7 +14,6 @@ open Names
open Constr
open Termops
open Tacmach
-open Locusops
open Ssrast
open Ssrcommon
@@ -82,8 +81,7 @@ let pf_clauseids gl gens clseq =
let hidden_clseq = function InHyps | InHypsSeq | InAllHyps -> true | _ -> false
-let settac id c = Tactics.letin_tac None (Name id) c None
-let posetac id cl = Proofview.V82.of_tactic (settac id cl nowhere)
+let posetac id cl = Proofview.V82.of_tactic (Tactics.pose_tac (Name id) cl)
let hidetacs clseq idhide cl0 =
if not (hidden_clseq clseq) then [] else
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d536204ec3..95d545b046 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2690,6 +2690,34 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
let (sigma, x) = new_evar newenv sigma ~principal:true ~store ccl in
(sigma, mkNamedLetIn id c t x)
+let pose_tac na c =
+ Proofview.Goal.enter begin fun gl ->
+ let sigma = Proofview.Goal.sigma gl in
+ let env = Proofview.Goal.env gl in
+ let hyps = named_context_val env in
+ let concl = Proofview.Goal.concl gl in
+ let t = typ_of env sigma c in
+ let (sigma, t) = Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma t in
+ let id = match na with
+ | Name id ->
+ let () = if mem_named_context_val id hyps then
+ user_err (str "Variable " ++ Id.print id ++ str " is already declared.")
+ in
+ id
+ | Anonymous ->
+ let id = id_of_name_using_hdchar env sigma t Anonymous in
+ next_ident_away_in_goal id (ids_of_named_context_val hyps)
+ in
+ Proofview.Unsafe.tclEVARS sigma <*>
+ Refine.refine ~typecheck:false begin fun sigma ->
+ let nhyps = EConstr.push_named_context_val (NamedDecl.LocalDef (id, c, t)) hyps in
+ let (sigma, ev) = Evarutil.new_pure_evar nhyps sigma concl in
+ let inst = Array.map_of_list (fun d -> mkVar (get_id d)) (named_context env) in
+ let body = mkEvar (ev, Array.append [|mkRel 1|] inst) in
+ (sigma, mkLetIn (Name id, c, t, body))
+ end
+ end
+
let letin_tac with_eq id c ty occs =
Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 57f20d2ff2..c088e404b0 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -390,6 +390,8 @@ val cut : types -> unit Proofview.tactic
(** {6 Tactics for adding local definitions. } *)
+val pose_tac : Name.t -> constr -> unit Proofview.tactic
+
val letin_tac : (bool * intro_pattern_naming) option ->
Name.t -> constr -> types option -> clause -> unit Proofview.tactic
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 00:00:22 +0000