aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.common2
-rw-r--r--dev/db1
-rw-r--r--dev/top_printers.ml19
-rw-r--r--doc/refman/CanonicalStructures.tex376
-rw-r--r--doc/refman/RefMan-ext.tex9
-rw-r--r--doc/refman/Reference-Manual.tex1
-rw-r--r--doc/refman/biblio.bib36
-rw-r--r--grammar/argextend.ml43
-rw-r--r--grammar/q_coqast.ml43
-rw-r--r--interp/constrarg.ml9
-rw-r--r--interp/constrarg.mli4
-rw-r--r--lib/genarg.ml9
-rw-r--r--lib/genarg.mli3
-rw-r--r--parsing/g_tactic.ml45
-rw-r--r--parsing/pcoq.ml44
-rw-r--r--parsing/pcoq.mli1
-rw-r--r--pretyping/evarutil.ml10
-rw-r--r--pretyping/evd.ml15
-rw-r--r--pretyping/evd.mli1
-rw-r--r--printing/pptactic.ml11
-rw-r--r--proofs/goal.ml7
-rw-r--r--proofs/goal.mli4
-rw-r--r--proofs/redexpr.ml6
-rw-r--r--tactics/extraargs.ml416
-rw-r--r--tactics/extraargs.mli7
-rw-r--r--tactics/extratactics.ml427
-rw-r--r--tactics/extratactics.mli2
-rw-r--r--tactics/tacintern.ml9
-rw-r--r--tactics/tacinterp.ml24
-rw-r--r--tactics/tacsubst.ml10
30 files changed, 536 insertions, 98 deletions
diff --git a/Makefile.common b/Makefile.common
index 8aaf8fceb..d967f3f6e 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -120,7 +120,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \
RefMan-tacex.v.tex RefMan-syn.v.tex \
RefMan-oth.v.tex RefMan-ltac.v.tex \
RefMan-decl.v.tex RefMan-pro.v.tex RefMan-sch.v.tex \
- Cases.v.tex Coercion.v.tex Extraction.v.tex \
+ Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \
Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \
Setoid.v.tex Helm.tex Classes.v.tex )
diff --git a/dev/db b/dev/db
index 10926be08..88cd9b057 100644
--- a/dev/db
+++ b/dev/db
@@ -39,3 +39,4 @@ install_printer Top_printers.prsubst
install_printer Top_printers.prdelta
install_printer Top_printers.ppfconstr
install_printer Top_printers.ppgenarginfo
+install_printer Top_printers.ppist
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 3d90d25cf..c2cbfae16 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -65,9 +65,12 @@ let ppintset l = pp (prset int (Int.Set.elements l))
let ppidset l = pp (prset pr_id (Id.Set.elements l))
let prset' pr l = str "[" ++ hov 0 (prlist_with_sep pr_comma pr l) ++ str "]"
-let ppidmap pr l =
+
+let pridmap pr l =
let pr (id,b) = pr_id id ++ str "=>" ++ pr id b in
- pp (prset' pr (Id.Map.fold (fun a b l -> (a,b)::l) l []))
+ prset' pr (Id.Map.fold (fun a b l -> (a,b)::l) l [])
+
+let ppidmap pr l = pp (pridmap pr l)
let ppevarsubst = ppidmap (fun id0 -> prset (fun (c,copt,id) ->
hov 0
@@ -355,14 +358,20 @@ let pp_argument_type t = pp (pr_argument_type t)
let pp_generic_argument arg =
pp(str"<genarg:"++pr_argument_type(genarg_tag arg)++str">")
-let ppgenarginfo arg =
+let prgenarginfo arg =
let tpe = pr_argument_type (genarg_tag arg) in
let pr_gtac _ x = Pptactic.pr_glob_tactic (Global.env()) x in
try
let data = Pptactic.pr_top_generic pr_constr pr_lconstr pr_gtac pr_constr_pattern arg in
- pp (str "<genarg:" ++ tpe ++ str " := [ " ++ data ++ str " ] >")
+ str "<genarg:" ++ tpe ++ str " := [ " ++ data ++ str " ] >"
with _any ->
- pp (str "<genarg:" ++ tpe ++ str ">")
+ str "<genarg:" ++ tpe ++ str ">"
+
+let ppgenarginfo arg = pp (prgenarginfo arg)
+
+let ppist ist =
+ let pr id arg = prgenarginfo arg in
+ pp (pridmap pr ist.Geninterp.lfun)
(**********************************************************************)
(* Vernac-level debugging commands *)
diff --git a/doc/refman/CanonicalStructures.tex b/doc/refman/CanonicalStructures.tex
new file mode 100644
index 000000000..fab660711
--- /dev/null
+++ b/doc/refman/CanonicalStructures.tex
@@ -0,0 +1,376 @@
+\achapter{Canonical Structures}
+\aauthor{Assia Mahboubi and Enrico Tassi}
+
+\label{CS-full}
+\index{Canonical Structures!presentation}
+
+This chapter explains the basics of Canonical Structure and how thy can be used
+to overload notations and build a hierarchy of algebraic structures.
+The examples are taken from~\cite{CSwcu}. We invite the interested reader
+to refer to this paper for all the details that are omitted here for brevity.
+The interested reader shall also find in~\cite{CSlessadhoc} a detailed
+description of another, complementary, use of Canonical Structures:
+advanced proof search. This latter papers also presents many techniques one
+can employ to tune the inference of Canonical Structures.
+
+\section{Notation overloading}
+
+We build an infix notation $==$ for a comparison predicate. Such notation
+will be overloaded, and its meaning will depend on the types of the terms
+that are compared.
+
+\begin{coq_eval}
+Require Import Arith.
+\end{coq_eval}
+
+\begin{coq_example}
+Module EQ.
+ Record class (T : Type) := Class { cmp : T -> T -> Prop }.
+ Structure type := Pack { obj : Type; class_of : class obj }.
+ Definition op (e : type) : obj e -> obj e -> Prop :=
+ let 'Pack _ (Class _ the_cmp) := e in the_cmp.
+ Check op.
+ Arguments op {e} x y : simpl never.
+ Arguments Class {T} cmp.
+ Module theory.
+ Notation "x == y" := (op x y) (at level 70).
+ End theory.
+End EQ.
+\end{coq_example}
+
+We use Coq modules as name spaces. This allows to follow the same pattern
+and naming convention for the rest of the chapter. The base name space
+contains the definitions of the algebraic structure. To keep the example
+small, the algebraic structure $EQ.type$ we are defining is very simplistic,
+and characterizes terms on which a binary relation is defined, without
+requiring such relation to validate any property.
+The inner $theory$ module contains the overloaded notation $==$ and
+will eventually contain lemmas holding on all the instances of the
+algebraic structure (in this case there are no lemmas).
+
+Note that in practice the user may want to declare $EQ.obj$ as a coercion,
+but we will not do that here.
+
+The following line tests that, when we assume a type $e$ that is in the
+$EQ$ class, then we can relates two of its objects with $==$.
+
+\begin{coq_example}
+Import EQ.theory.
+Check forall (e : EQ.type) (a b : EQ.obj e), a == b.
+\end{coq_example}
+
+Still, no concrete type is in the $EQ$ class. We amend that by equipping $nat$
+with a comparison relation.
+
+\begin{coq_example}
+Fail Check 3 == 3.
+Definition nat_eq (x y : nat) := nat_compare x y = Eq.
+Definition nat_EQcl : EQ.class nat := EQ.Class nat_eq.
+Canonical Structure nat_EQty : EQ.type := EQ.Pack nat nat_EQcl.
+Check 3 == 3.
+Eval compute in 3 == 4.
+\end{coq_example}
+
+This last test shows that Coq is now not only able to typecheck $3==3$, but
+also that the infix relation was bound to the $nat\_eq$ relation. This
+relation is selected whenever $==$ is used on terms of type $nat$. This
+can be read in the line declaring the canonical structure $nat\_EQty$,
+where the first argument to $Pack$ is the key and its second argument
+a group of canonical values associated to the key. In this case we associate
+to $nat$ only one canonical value (since its class, $nat\_EQcl$ has just one
+member). The use of the projection $op$ requires its argument to be in
+the class $EQ$, and uses such a member (function) to actually compare
+its arguments.
+
+Similarly, we could equip any other type with a comparison relation, and
+use the $==$ notation on terms of this type.
+
+\subsection{Derived Canonical Structures}
+
+We know how to use $==$ on base types, like $nat$, $bool$, $Z$.
+Here we show how to deal with type constructors, i.e. how to make the
+following example work:
+
+\begin{coq_example}
+Fail Check forall (e : EQ.type) (a b : EQ.obj e), (a,b) == (a,b).
+\end{coq_example}
+
+The error message is telling that Coq has no idea on how to compare
+pairs of objects. The following construction is telling Coq exactly how to do
+that.
+
+\begin{coq_example}
+Definition pair_eq (e1 e2 : EQ.type) (x y : EQ.obj e1 * EQ.obj e2) :=
+ fst x == fst y /\ snd x == snd y.
+Definition pair_EQcl e1 e2 := EQ.Class (pair_eq e1 e2).
+Canonical Structure pair_EQty (e1 e2 : EQ.type) : EQ.type :=
+ EQ.Pack (EQ.obj e1 * EQ.obj e2) (pair_EQcl e1 e2).
+Check forall (e : EQ.type) (a b : EQ.obj e), (a,b) == (a,b).
+Check forall n m : nat, (3,4) == (n,m).
+\end{coq_example}
+
+Thanks to the $pair\_EQty$ declaration, Coq is able to build a comparison
+relation for pairs whenever it is able to build a comparison relation
+for each component of the pair. The declaration associates to the key
+$*$ (the type constructor of pairs) the canonical comparison relation
+$pair\_eq$ whenever the type constructor $*$ is applied to two types
+being themselves in the $EQ$ class.
+
+\section{Hierarchy of structures}
+
+To get to an interesting example we need another base class to be available.
+We choose the class of types that are equipped with an order relation,
+to which we associate the infix $<=$ notation.
+
+\begin{coq_example}
+Module LE.
+ Record class T := Class { cmp : T -> T -> Prop }.
+ Structure type := Pack { obj : Type; class_of : class obj }.
+ Definition op (e : type) : obj e -> obj e -> Prop :=
+ let 'Pack _ (Class _ f) := e in f.
+ Arguments op {_} x y : simpl never.
+ Arguments Class {T} cmp.
+ Module theory.
+ Notation "x <= y" := (op x y) (at level 70).
+ End theory.
+End LE.
+\end{coq_example}
+
+As before we register a canonical $LE$ class for $nat$.
+
+\begin{coq_example}
+Import LE.theory.
+Definition nat_le x y := nat_compare x y <> Gt.
+Definition nat_LEcl : LE.class nat := LE.Class nat_le.
+Canonical Structure nat_LEty : LE.type := LE.Pack nat nat_LEcl.
+\end{coq_example}
+
+And we enable Coq to relate pair of terms with $<=$.
+
+\begin{coq_example}
+Definition pair_le e1 e2 (x y : LE.obj e1 * LE.obj e2) :=
+ fst x <= fst y /\ snd x <= snd y.
+Definition pair_LEcl e1 e2 := LE.Class (pair_le e1 e2).
+Canonical Structure pair_LEty (e1 e2 : LE.type) : LE.type :=
+ LE.Pack (LE.obj e1 * LE.obj e2) (pair_LEcl e1 e2).
+Check (3,4,5) <= (3,4,5).
+\end{coq_example}
+
+At the current stage we can use $==$ and $<=$ on concrete types,
+like tuples of natural numbers, but we can't develop an algebraic
+theory over the types that are equipped with both relations.
+
+\begin{coq_example}
+Check 2 <= 3 /\ 2 == 2.
+Fail Check forall (e : EQ.type) (x y : EQ.obj e), x <= y -> y <= x -> x == y.
+Fail Check forall (e : LE.type) (x y : LE.obj e), x <= y -> y <= x -> x == y.
+\end{coq_example}
+
+We need to define a new class that inherits from both $EQ$ and $LE$.
+
+\begin{coq_example}
+Module LEQ.
+ Record mixin (e : EQ.type) (le : EQ.obj e -> EQ.obj e -> Prop) :=
+ Mixin { compat : forall x y : EQ.obj e, le x y /\ le y x <-> x == y }.
+ Record class T := Class {
+ EQ_class : EQ.class T;
+ LE_class : LE.class T;
+ extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }.
+ Structure type := _Pack { obj : Type; class_of : class obj }.
+ Arguments Mixin {e le} _.
+ Arguments Class {T} _ _ _.
+\end{coq_example}
+
+The $mixin$ component of the $LEQ$ class contains all the extra content
+we are adding to $EQ$ and $LE$. In particular it contains the requirement
+that the two relations we are combining are compatible.
+
+Unfortunately there is still an obstacle to developing the algebraic theory
+of this new class.
+
+\begin{coq_example}
+ Module theory.
+ Fail Check forall (le : type) (n m : obj le), n <= m -> n <= m -> n == m.
+\end{coq_example}
+
+The problem is that the two classes $LE$ and $LEQ$ are not yet related by
+a subclass relation. In other words Coq does not see that an object
+of the $LEQ$ class is also an object of the $LE$ class.
+
+The following two constructions tell Coq how to canonically build
+the $LE.type$ and $EQ.type$ structure given an $LEQ.type$ structure
+on the same type.
+
+\begin{coq_example}
+ Definition to_EQ (e : type) : EQ.type :=
+ EQ.Pack (obj e) (EQ_class _ (class_of e)).
+ Canonical Structure to_EQ.
+ Definition to_LE (e : type) : LE.type :=
+ LE.Pack (obj e) (LE_class _ (class_of e)).
+ Canonical Structure to_LE.
+\end{coq_example}
+We can now formulate out first theorem on the objects of the $LEQ$ structure.
+\begin{coq_example}
+ Lemma lele_eq (e : type) (x y : obj e) : x <= y -> y <= x -> x == y.
+ now intros; apply (compat _ _ (extra _ (class_of e)) x y); split. Qed.
+ Arguments lele_eq {e} x y _ _.
+ End theory.
+End LEQ.
+Import LEQ.theory.
+Check lele_eq.
+\end{coq_example}
+
+Of course one would like to apply results proved in the algebraic
+setting to any concrete instate of the algebraic structure.
+
+\begin{coq_example}
+Example test_algebraic (n m : nat) : n <= m -> m <= n -> n == m.
+ Fail apply (lele_eq n m). Abort.
+Example test_algebraic2 (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) :
+ n <= m -> m <= n -> n == m.
+ Fail apply (lele_eq n m). Abort.
+\end{coq_example}
+
+Again one has to tell Coq that the type $nat$ is in the $LEQ$ class, and how
+the type constructor $*$ interacts with the $LEQ$ class. In the following
+proofs are omitted for brevity.
+
+\begin{coq_example}
+Lemma nat_LEQ_compat (n m : nat) : n <= m /\ m <= n <-> n == m.
+\end{coq_example}
+\begin{coq_eval}
+
+split.
+ unfold EQ.op; unfold LE.op; simpl; unfold nat_le; unfold nat_eq.
+ case (nat_compare_spec n m); [ reflexivity | | now intros _ [H _]; case H ].
+ now intro H; apply nat_compare_gt in H; rewrite -> H; intros [_ K]; case K.
+unfold EQ.op; unfold LE.op; simpl; unfold nat_le; unfold nat_eq.
+case (nat_compare_spec n m); [ | intros H1 H2; discriminate H2 .. ].
+intro H; rewrite H; intros _; split; [ intro H1; discriminate H1 | ].
+case (nat_compare_eq_iff m m); intros _ H1.
+now rewrite H1; auto; intro H2; discriminate H2.
+Qed.
+\end{coq_eval}
+\begin{coq_example}
+Definition nat_LEQmx := LEQ.Mixin nat_LEQ_compat.
+Lemma pair_LEQ_compat (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) :
+n <= m /\ m <= n <-> n == m.
+\end{coq_example}
+\begin{coq_eval}
+
+case n; case m; unfold EQ.op; unfold LE.op; simpl.
+intros n1 n2 m1 m2; split; [ intros [[Le1 Le2] [Ge1 Ge2]] | intros [H1 H2] ].
+ now split; apply lele_eq.
+case (LEQ.compat _ _ (LEQ.extra _ (LEQ.class_of l1)) m1 n1).
+case (LEQ.compat _ _ (LEQ.extra _ (LEQ.class_of l2)) m2 n2).
+intros _ H3 _ H4; apply H3 in H2; apply H4 in H1; clear H3 H4.
+now case H1; case H2; split; split.
+Qed.
+\end{coq_eval}
+\begin{coq_example}
+Definition pair_LEQmx l1 l2 := LEQ.Mixin (pair_LEQ_compat l1 l2).
+\end{coq_example}
+
+The following script registers an $LEQ$ class for $nat$ and for the
+type constructor $*$. It also tests that they work as expected.
+
+Unfortunately, these declarations are very verbose. In the following
+subsection we show how to make these declaration more compact.
+
+\begin{coq_example}
+Module Add_instance_attempt.
+ Canonical Structure nat_LEQty : LEQ.type :=
+ LEQ._Pack nat (LEQ.Class nat_EQcl nat_LEcl nat_LEQmx).
+ Canonical Structure pair_LEQty (l1 l2 : LEQ.type) : LEQ.type :=
+ LEQ._Pack (LEQ.obj l1 * LEQ.obj l2)
+ (LEQ.Class
+ (EQ.class_of (pair_EQty (to_EQ l1) (to_EQ l2)))
+ (LE.class_of (pair_LEty (to_LE l1) (to_LE l2)))
+ (pair_LEQmx l1 l2)).
+ Example test_algebraic (n m : nat) : n <= m -> m <= n -> n == m.
+ now apply (lele_eq n m). Qed.
+ Example test_algebraic2 (n m : nat * nat) : n <= m -> m <= n -> n == m.
+ now apply (lele_eq n m). Qed.
+End Add_instance_attempt.
+\end{coq_example}
+
+Note that no direct proof of $n <= m -> m <= n -> n == m$ is provided by the
+user for $n$ and $m$ of type $nat * nat$. What the user provides is a proof of
+this statement for $n$ and $m$ of type $nat$ and a proof that the pair
+constructor preserves this property. The combination of these two facts is a
+simple form of proof search that Coq performs automatically while inferring
+canonical structures.
+
+\subsection{Compact declaration of Canonical Structures}
+
+We need some infrastructure for that.
+
+\begin{coq_example}
+Module infrastructure.
+ Require Import Strings.String.
+ Inductive phantom {T : Type} (t : T) : Type := Phantom.
+ Definition unify {T1 T2} (t1 : T1) (t2 : T2) (s : option string) := phantom t1 -> phantom t2.
+ Definition id {T} {t : T} (x : phantom t) := x.
+ Notation "[find v | t1 ~ t2 ] p" := (fun v (_ : unify t1 t2 None) => p) (at level 50, v ident, only parsing).
+ Notation "[find v | t1 ~ t2 | s ] p" := (fun v (_ : unify t1 t2 (Some s)) => p) (at level 50, v ident, only parsing).
+ Notation "'Error : t : s" := (unify _ t (Some s)) (at level 50, format "''Error' : t : s").
+ Open Scope string_scope.
+End infrastructure.
+\end{coq_example}
+
+To explain the notation $[find v | t1 \textasciitilde t2]$ lets pick one
+of its instances: $[find e | EQ.obj e \textasciitilde T | "is not an EQ.type" ]$.
+It should be read as: ``find a class e such that its objects have type T
+or fail with message "T is not an EQ.type"''.
+
+The other utilities are used to ask Coq to solve a specific unification
+problem, that will in turn require the inference of some canonical
+structures. They are explained in mode details in~\cite{CSwcu}.
+
+We now have all we need to create a compact ``packager'' to declare
+instances of the $LEQ$ class.
+
+\begin{coq_example}
+Import infrastructure.
+Definition packager T e0 le0 (m0 : LEQ.mixin e0 le0) :=
+ [find e | EQ.obj e ~ T | "is not an EQ.type" ]
+ [find o | LE.obj o ~ T | "is not an LE.type" ]
+ [find ce | EQ.class_of e ~ ce ]
+ [find co | LE.class_of o ~ co ]
+ [find m | m ~ m0 | "is not the right mixin" ]
+ LEQ._Pack T (LEQ.Class ce co m).
+Notation Pack T m := (packager T _ _ m _ id _ id _ id _ id _ id).
+\end{coq_example}
+
+The object $Pack$ takes a type $T$ (the key) and a mixin $m$. It infers all
+the other pieces of the class $LEQ$ and declares them as canonical values
+associated to the $T$ key. All in all, the only new piece of information
+we add in the $LEQ$ class is the mixin, all the rest is already canonical
+for $T$ and hence can be inferred by Coq.
+
+$Pack$ is a notation, hence it is not type checked at the time of its
+declaration. It will be type checked when it is used, an in that case
+$T$ is going to be a concrete type. The odd arguments $\_$ and $id$ we
+pass to the
+packager represent respectively the classes to be inferred (like $e$, $o$, etc) and a token ($id$) to force their inference. Again, for all the details the
+reader can refer to~\cite{CSwcu}.
+
+The declaration of canonical instances can now be way more compact:
+
+\begin{coq_example}
+Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx.
+Canonical Structure pair_LEQty (l1 l2 : LEQ.type) :=
+ Eval hnf in Pack (LEQ.obj l1 * LEQ.obj l2) (pair_LEQmx l1 l2).
+\end{coq_example}
+
+Error messages are also quite intelligible (if one skips to the end of
+the message).
+
+\begin{coq_example}
+Fail Canonical Structure err := Eval hnf in Pack bool nat_LEQmx.
+\end{coq_example}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% End:
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index f5ad9d913..c5cf41473 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1598,8 +1598,13 @@ arguments, use:
\comindex{Canonical Structure}}
A canonical structure is an instance of a record/structure type that
-can be used to solve equations involving implicit arguments. Assume
-that {\qualid} denotes an object $(Build\_struc~ c_1~ \ldots~ c_n)$ in the
+can be used to solve unification problems involving a projection
+applied to an unknown structure instance (an implicit argument) and
+a value. The complete documentation of canonical structures can be found
+in Chapter~\ref{CS-full}, here only a simple example is given.
+
+Assume that {\qualid} denotes an object $(Build\_struc~ c_1~ \ldots~ c_n)$ in
+the
structure {\em struct} of which the fields are $x_1$, ...,
$x_n$. Assume that {\qualid} is declared as a canonical structure
using the command
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 4380f5442..7b6c8ba3b 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -111,6 +111,7 @@ Options A and B of the licence are {\em not} elected.}
\include{AddRefMan-pre}%
\include{Cases.v}%
\include{Coercion.v}%
+\include{CanonicalStructures.v}%
\include{Classes.v}%
%%SUPPRIME \include{Natural.v}%
\include{Omega.v}%
diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index 3715c4c79..a2895cfcf 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -1291,3 +1291,39 @@ Languages},
pages = "102--114",
year = "1992",
}
+
+@inproceedings{CSwcu,
+ hal_id = {hal-00816703},
+ url = {http://hal.inria.fr/hal-00816703},
+ title = {{Canonical Structures for the working Coq user}},
+ author = {Mahboubi, Assia and Tassi, Enrico},
+ booktitle = {{ITP 2013, 4th Conference on Interactive Theorem Proving}},
+ publisher = {Springer},
+ pages = {19-34},
+ address = {Rennes, France},
+ volume = {7998},
+ editor = {Sandrine Blazy and Christine Paulin and David Pichardie },
+ series = {LNCS },
+ doi = {10.1007/978-3-642-39634-2\_5 },
+ year = {2013},
+}
+
+@article{CSlessadhoc,
+ author = {Gonthier, Georges and Ziliani, Beta and Nanevski, Aleksandar and Dreyer, Derek},
+ title = {How to Make Ad Hoc Proof Automation Less Ad Hoc},
+ journal = {SIGPLAN Not.},
+ issue_date = {September 2011},
+ volume = {46},
+ number = {9},
+ month = sep,
+ year = {2011},
+ issn = {0362-1340},
+ pages = {163--175},
+ numpages = {13},
+ url = {http://doi.acm.org/10.1145/2034574.2034798},
+ doi = {10.1145/2034574.2034798},
+ acmid = {2034798},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {canonical structures, coq, custom proof automation, hoare type theory, interactive theorem proving, tactics, type classes},
+}
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index d884a10cb..934b9b117 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -33,13 +33,12 @@ let rec make_wit loc = function
| IntOrVarArgType -> <:expr< Constrarg.wit_int_or_var >>
| IdentArgType b -> <:expr< Constrarg.wit_ident_gen $mlexpr_of_bool b$ >>
| VarArgType -> <:expr< Constrarg.wit_var >>
- | RefArgType -> <:expr< Constrarg.wit_ref >>
| QuantHypArgType -> <:expr< Constrarg.wit_quant_hyp >>
| GenArgType -> <:expr< Constrarg.wit_genarg >>
| ConstrArgType -> <:expr< Constrarg.wit_constr >>
| ConstrMayEvalArgType -> <:expr< Constrarg.wit_constr_may_eval >>
| RedExprArgType -> <:expr< Constrarg.wit_red_expr >>
- | OpenConstrArgType b -> <:expr< Constrarg.wit_open_constr_gen $mlexpr_of_bool b$ >>
+ | OpenConstrArgType -> <:expr< Constrarg.wit_open_constr >>
| ConstrWithBindingsArgType -> <:expr< Constrarg.wit_constr_with_bindings >>
| BindingsArgType -> <:expr< Constrarg.wit_bindings >>
| ListArgType t -> <:expr< Genarg.wit_list $make_wit loc t$ >>
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 02c00e3f0..3e11bf5a8 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -203,11 +203,10 @@ let mlexpr_of_red_expr = function
let rec mlexpr_of_argtype loc = function
| Genarg.IntOrVarArgType -> <:expr< Genarg.IntOrVarArgType >>
- | Genarg.RefArgType -> <:expr< Genarg.RefArgType >>
| Genarg.IdentArgType b -> <:expr< Genarg.IdentArgType $mlexpr_of_bool b$ >>
| Genarg.VarArgType -> <:expr< Genarg.VarArgType >>
| Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >>
- | Genarg.OpenConstrArgType b -> <:expr< Genarg.OpenConstrArgType $mlexpr_of_bool b$ >>
+ | Genarg.OpenConstrArgType -> <:expr< Genarg.OpenConstrArgType >>
| Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >>
| Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >>
| Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >>
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 16af7c308..4f20dd560 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -47,7 +47,7 @@ let wit_pattern_ident = wit_ident_gen false
let wit_var = unsafe_of_type VarArgType
-let wit_ref = unsafe_of_type RefArgType
+let wit_ref = Genarg.make0 None "ref"
let wit_quant_hyp = unsafe_of_type QuantHypArgType
@@ -60,11 +60,7 @@ let wit_constr = unsafe_of_type ConstrArgType
let wit_constr_may_eval = unsafe_of_type ConstrMayEvalArgType
-let wit_open_constr_gen b = unsafe_of_type (OpenConstrArgType b)
-
-let wit_open_constr = wit_open_constr_gen false
-
-let wit_casted_open_constr = wit_open_constr_gen true
+let wit_open_constr = unsafe_of_type OpenConstrArgType
let wit_constr_with_bindings = unsafe_of_type ConstrWithBindingsArgType
@@ -75,6 +71,7 @@ let wit_red_expr = unsafe_of_type RedExprArgType
(** Register location *)
let () =
+ register_name0 wit_ref "Constrarg.wit_ref";
register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern";
register_name0 wit_tactic "Constrarg.wit_tactic";
register_name0 wit_sort "Constrarg.wit_sort";
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index 1233e165f..b83c20065 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -57,12 +57,8 @@ val wit_constr_may_eval :
(glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval,
constr) genarg_type
-val wit_open_constr_gen : bool -> (open_constr_expr, open_glob_constr, open_constr) genarg_type
-
val wit_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type
-val wit_casted_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type
-
val wit_constr_with_bindings :
(constr_expr with_bindings,
glob_constr_and_expr with_bindings,
diff --git a/lib/genarg.ml b/lib/genarg.ml
index 98287d184..6520669fa 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -14,13 +14,12 @@ type argument_type =
| IntOrVarArgType
| IdentArgType of bool
| VarArgType
- | RefArgType
(* Specific types *)
| GenArgType
| ConstrArgType
| ConstrMayEvalArgType
| QuantHypArgType
- | OpenConstrArgType of bool
+ | OpenConstrArgType
| ConstrWithBindingsArgType
| BindingsArgType
| RedExprArgType
@@ -33,12 +32,11 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
| IntOrVarArgType, IntOrVarArgType -> true
| IdentArgType b1, IdentArgType b2 -> (b1 : bool) == b2
| VarArgType, VarArgType -> true
-| RefArgType, RefArgType -> true
| GenArgType, GenArgType -> true
| ConstrArgType, ConstrArgType -> true
| ConstrMayEvalArgType, ConstrMayEvalArgType -> true
| QuantHypArgType, QuantHypArgType -> true
-| OpenConstrArgType b1, OpenConstrArgType b2 -> (b1 : bool) == b2
+| OpenConstrArgType, OpenConstrArgType -> true
| ConstrWithBindingsArgType, ConstrWithBindingsArgType -> true
| BindingsArgType, BindingsArgType -> true
| RedExprArgType, RedExprArgType -> true
@@ -54,12 +52,11 @@ let rec pr_argument_type = function
| IdentArgType true -> str "ident"
| IdentArgType false -> str "pattern_ident"
| VarArgType -> str "var"
-| RefArgType -> str "ref"
| GenArgType -> str "genarg"
| ConstrArgType -> str "constr"
| ConstrMayEvalArgType -> str "constr_may_eval"
| QuantHypArgType -> str "qhyp"
-| OpenConstrArgType _ -> str "open_constr"
+| OpenConstrArgType -> str "open_constr"
| ConstrWithBindingsArgType -> str "constr_with_bindings"
| BindingsArgType -> str "bindings"
| RedExprArgType -> str "redexp"
diff --git a/lib/genarg.mli b/lib/genarg.mli
index e2654fcf5..51c261742 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -193,13 +193,12 @@ type argument_type =
| IntOrVarArgType
| IdentArgType of bool
| VarArgType
- | RefArgType
(** Specific types *)
| GenArgType
| ConstrArgType
| ConstrMayEvalArgType
| QuantHypArgType
- | OpenConstrArgType of bool
+ | OpenConstrArgType
| ConstrWithBindingsArgType
| BindingsArgType
| RedExprArgType
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index eb483c50c..93afb3d5a 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -215,7 +215,7 @@ let merge_occurrences loc cl = function
GEXTEND Gram
GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
- bindings red_expr int_or_var open_constr casted_open_constr
+ bindings red_expr int_or_var open_constr
simple_intropattern;
int_or_var:
@@ -236,9 +236,6 @@ GEXTEND Gram
open_constr:
[ [ c = constr -> ((),c) ] ]
;
- casted_open_constr:
- [ [ c = constr -> ((),c) ] ]
- ;
induction_arg:
[ [ n = natural -> ElimOnAnonHyp n
| c = constr_with_bindings -> induction_arg_of_constr c
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 79228e946..d25efa72a 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -377,9 +377,7 @@ module Tactic =
(* Entries that can be refered via the string -> Gram.entry table *)
(* Typically for tactic user extensions *)
let open_constr =
- make_gen_entry utactic (rawwit (wit_open_constr_gen false)) "open_constr"
- let casted_open_constr =
- make_gen_entry utactic (rawwit (wit_open_constr_gen true)) "casted_open_constr"
+ make_gen_entry utactic (rawwit wit_open_constr) "open_constr"
let constr_with_bindings =
make_gen_entry utactic (rawwit wit_constr_with_bindings) "constr_with_bindings"
let bindings =
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index bbb71a170..56282f2f6 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -213,7 +213,6 @@ module Tactic :
sig
open Glob_term
val open_constr : open_constr_expr Gram.entry
- val casted_open_constr : open_constr_expr Gram.entry
val constr_with_bindings : constr_expr with_bindings Gram.entry
val bindings : constr_expr bindings Gram.entry
val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 08643a1d9..780da888e 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -336,7 +336,15 @@ let push_rel_context_to_named_context env typ =
let (subst, vsubst, _, env) =
Context.fold_rel_context
(fun (na,c,t) (subst, vsubst, avoid, env) ->
- let id = next_ident_away (id_of_name_using_hdchar env t na) avoid in
+ let id =
+ (* ppedrot: we want to infer nicer names for the refine tactic, but
+ keeping at the same time backward compatibility in other code
+ using this function. For now, we only attempt to preserve the
+ old behaviour of Program, but ultimately, one should do something
+ about this whole name generation problem. *)
+ if Flags.is_program_mode () then next_name_away na avoid
+ else next_ident_away (id_of_name_using_hdchar env t na) avoid
+ in
match extract_if_neq id na with
| Some id0 when not (is_section_variable id0) ->
(* spiwack: if [id<>id0], rather than introducing a new
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 5537d87d0..5870a22b7 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -222,15 +222,6 @@ let eq_evar_info ei1 ei2 =
exception NotInstantiatedEvar
(* Note: let-in contributes to the instance *)
-let make_evar_instance sign args =
- let rec instrec sign args = match sign, args with
- | [], [] -> []
- | (id,_,_) :: sign, c :: args ->
- if isVarId id c then instrec sign args
- else (id, c) :: instrec sign args
- | [], _ | _, [] -> instance_mismatch ()
- in
- instrec sign args
let make_evar_instance_array info args =
let len = Array.length args in
@@ -251,12 +242,6 @@ let make_evar_instance_array info args =
let filter = Filter.repr (evar_filter info) in
instrec filter (evar_context info) 0
-let instantiate_evar sign c args =
- let inst = make_evar_instance sign args in
- match inst with
- | [] -> c
- | _ -> replace_vars inst c
-
let instantiate_evar_array info c args =
let inst = make_evar_instance_array info args in
match inst with
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index ec16f53b7..58e4cd630 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -218,7 +218,6 @@ val existential_opt_value : evar_map -> existential -> constr option
(** Same as {!existential_value} but returns an option instead of raising an
exception. *)
-val instantiate_evar : named_context -> constr -> constr list -> constr
val instantiate_evar_array : evar_info -> constr -> constr array -> constr
val subst_evar_defs_light : substitution -> evar_map -> evar_map
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index e1324c3ee..77f5db3b4 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -148,7 +148,6 @@ let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generi
| IntOrVarArgType -> pr_or_var int (out_gen (rawwit wit_int_or_var) x)
| IdentArgType b -> if_pattern_ident b pr_id (out_gen (rawwit wit_ident) x)
| VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x)
- | RefArgType -> prref (out_gen (rawwit wit_ref) x)
| GenArgType -> pr_raw_generic prc prlc prtac prpat prref (out_gen (rawwit wit_genarg) x)
| ConstrArgType -> prc (out_gen (rawwit wit_constr) x)
| ConstrMayEvalArgType ->
@@ -158,7 +157,7 @@ let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generi
| RedExprArgType ->
pr_red_expr (prc,prlc,pr_or_by_notation prref,prpat)
(out_gen (rawwit wit_red_expr) x)
- | OpenConstrArgType b -> prc (snd (out_gen (rawwit (wit_open_constr_gen b)) x))
+ | OpenConstrArgType -> prc (snd (out_gen (rawwit wit_open_constr) x))
| ConstrWithBindingsArgType ->
pr_with_bindings prc prlc (out_gen (rawwit wit_constr_with_bindings) x)
| BindingsArgType ->
@@ -183,7 +182,6 @@ let rec pr_glb_generic prc prlc prtac prpat x =
| IntOrVarArgType -> pr_or_var int (out_gen (glbwit wit_int_or_var) x)
| IdentArgType b -> if_pattern_ident b pr_id (out_gen (glbwit wit_ident) x)
| VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x)
- | RefArgType -> pr_or_var (pr_located pr_global) (out_gen (glbwit wit_ref) x)
| GenArgType -> pr_glb_generic prc prlc prtac prpat (out_gen (glbwit wit_genarg) x)
| ConstrArgType -> prc (out_gen (glbwit wit_constr) x)
| ConstrMayEvalArgType ->
@@ -196,7 +194,7 @@ let rec pr_glb_generic prc prlc prtac prpat x =
pr_red_expr
(prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference),prpat)
(out_gen (glbwit wit_red_expr) x)
- | OpenConstrArgType b -> prc (snd (out_gen (glbwit (wit_open_constr_gen b)) x))
+ | OpenConstrArgType -> prc (snd (out_gen (glbwit wit_open_constr) x))
| ConstrWithBindingsArgType ->
pr_with_bindings prc prlc (out_gen (glbwit wit_constr_with_bindings) x)
| BindingsArgType ->
@@ -219,7 +217,6 @@ let rec pr_top_generic prc prlc prtac prpat x =
| IntOrVarArgType -> pr_or_var int (out_gen (topwit wit_int_or_var) x)
| IdentArgType b -> if_pattern_ident b pr_id (out_gen (topwit wit_ident) x)
| VarArgType -> pr_id (out_gen (topwit wit_var) x)
- | RefArgType -> pr_global (out_gen (topwit wit_ref) x)
| GenArgType -> pr_top_generic prc prlc prtac prpat (out_gen (topwit wit_genarg) x)
| ConstrArgType -> prc (out_gen (topwit wit_constr) x)
| ConstrMayEvalArgType -> prc (out_gen (topwit wit_constr_may_eval) x)
@@ -227,7 +224,7 @@ let rec pr_top_generic prc prlc prtac prpat x =
| RedExprArgType ->
pr_red_expr (prc,prlc,pr_evaluable_reference,prpat)
(out_gen (topwit wit_red_expr) x)
- | OpenConstrArgType b -> prc (snd (out_gen (topwit (wit_open_constr_gen b)) x))
+ | OpenConstrArgType -> prc (snd (out_gen (topwit wit_open_constr) x))
| ConstrWithBindingsArgType ->
let (c,b) = (out_gen (topwit wit_constr_with_bindings) x).Evd.it in
pr_with_bindings prc prlc (c,b)
@@ -1032,6 +1029,8 @@ let register_uniform_printer wit pr =
Genprint.register_print0 wit pr pr pr
let () =
+ Genprint.register_print0 Constrarg.wit_ref
+ pr_reference (pr_or_var (pr_located pr_global)) pr_global;
Genprint.register_print0 Constrarg.wit_intro_pattern
pr_intro_pattern pr_intro_pattern pr_intro_pattern;
Genprint.register_print0 Constrarg.wit_sort
diff --git a/proofs/goal.ml b/proofs/goal.ml
index ae42acf18..43d7b3579 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -242,7 +242,7 @@ module Refinable = struct
(* spiwack: it is not entirely satisfactory to have this function here. Plus it is
a bit hackish. However it does not seem possible to move it out until
pretyping is defined as some proof procedure. *)
- let constr_of_raw handle check_type resolve_classes rawc = (); fun env rdefs gl info ->
+ let constr_of_raw handle check_type resolve_classes lvar rawc = (); fun env rdefs gl info ->
(* We need to keep trace of what [rdefs] was originally*)
let init_defs = !rdefs in
(* if [check_type] is true, then creates a type constraint for the
@@ -253,9 +253,10 @@ module Refinable = struct
let flags =
if resolve_classes then Pretyping.all_no_fail_flags
else Pretyping.no_classes_no_fail_inference_flags in
- let open_constr =
- Pretyping.understand_tcc_evars ~flags rdefs env ~expected_type:tycon rawc
+ let (sigma, open_constr) =
+ Pretyping.understand_ltac flags !rdefs env lvar tycon rawc
in
+ let () = rdefs := sigma in
let () = update_handle handle init_defs !rdefs in
open_constr
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 1f04ce8c1..013b3199a 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -93,8 +93,8 @@ module Refinable : sig
The principal argument is a [glob_constr] which is then pretyped in the
context of a term, the remaining evars are registered to the handle.
It is the main component of the toplevel refine tactic.*)
- val constr_of_raw :
- handle -> bool -> bool -> Glob_term.glob_constr -> Term.constr sensitive
+ val constr_of_raw : handle -> bool -> bool -> Pretyping.ltac_var_map ->
+ Glob_term.glob_constr -> Term.constr sensitive
(* [constr_of_open_constr h check_type] transforms an open constr into a
goal-sensitive constr, adding the undefined variables to the set of subgoals.
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 69ff1dc51..f71ec440e 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -23,8 +23,10 @@ open Libobject
open Misctypes
(* call by value normalisation function using the virtual machine *)
-let cbv_vm env _ c =
- let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in
+let cbv_vm env sigma c =
+ let ctyp = Retyping.get_type_of env sigma c in
+ if Termops.occur_meta_or_existential c then
+ error "vm_compute does not support existential variables.";
Vnorm.cbv_vm env c ctyp
let cbv_native env _ c =
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index ccc231cf2..c156e869d 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -116,9 +116,23 @@ ARGUMENT EXTEND glob
GLOB_TYPED AS glob_constr_and_expr
GLOB_PRINTED BY pr_gen
- [ lconstr(c) ] -> [ c ]
+ [ constr(c) ] -> [ c ]
END
+ARGUMENT EXTEND lglob
+ PRINTED BY pr_globc
+
+ INTERPRETED BY interp_glob
+ GLOBALIZED BY glob_glob
+ SUBSTITUTED BY subst_glob
+
+ RAW_TYPED AS constr_expr
+ RAW_PRINTED BY pr_gen
+
+ GLOB_TYPED AS glob_constr_and_expr
+ GLOB_PRINTED BY pr_gen
+ [ lconstr(c) ] -> [ c ]
+END
type 'id gen_place= ('id * hyp_location_flag,unit) location
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index 1367f7032..dfc14bddf 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -28,7 +28,14 @@ val wit_glob :
(constr_expr,
Tacexpr.glob_constr_and_expr,
Tacinterp.interp_sign * glob_constr) Genarg.genarg_type
+
+val wit_lglob :
+ (constr_expr,
+ Tacexpr.glob_constr_and_expr,
+ Tacinterp.interp_sign * glob_constr) Genarg.genarg_type
+
val glob : constr_expr Pcoq.Gram.entry
+val lglob : constr_expr Pcoq.Gram.entry
type 'id gen_place= ('id * Locus.hyp_location_flag,unit) location
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index c81e7ce3f..031cbc7c5 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -324,8 +324,31 @@ END
let refine_tac = Tactics.New.refine
+let refine_red_flags =
+ Genredexpr.Lazy {
+ Genredexpr.rBeta=true;
+ rIota=true;
+ rZeta=false;
+ rDelta=false;
+ rConst=[];
+ }
+
+let refine_locs = { Locus.onhyps=None; concl_occs=Locus.AllOccurrences }
+
+let refine_tac (ist, c) =
+ Proofview.Goal.enter (fun gl ->
+ let env = Proofview.Goal.env gl in
+ let constrvars = Tacinterp.extract_ltac_constr_values ist env in
+ let vars = (constrvars, ist.Geninterp.lfun) in
+ let c = Goal.Refinable.make begin fun h ->
+ Goal.Refinable.constr_of_raw h true true vars c
+ end in
+ Proofview.Goal.lift c >>= fun c ->
+ Proofview.tclSENSITIVE (Goal.refine c) <*>
+ Proofview.V82.tactic (reduce refine_red_flags refine_locs))
+
TACTIC EXTEND refine
- [ "refine" casted_open_constr(c) ] -> [ refine_tac c ]
+ [ "refine" glob(c) ] -> [ refine_tac c ]
END
(**********************************************************************)
@@ -408,7 +431,7 @@ END
open Tacticals
TACTIC EXTEND instantiate
- [ "instantiate" "(" integer(i) ":=" glob(c) ")" hloc(hl) ] ->
+ [ "instantiate" "(" integer(i) ":=" lglob(c) ")" hloc(hl) ] ->
[ Proofview.V82.tactic (instantiate i c hl) ]
| [ "instantiate" ] -> [ Proofview.V82.tactic (tclNORMEVAR) ]
END
diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli
index 7a0fabe1f..2b28a6547 100644
--- a/tactics/extratactics.mli
+++ b/tactics/extratactics.mli
@@ -11,6 +11,6 @@ open Proof_type
val discrHyp : Names.Id.t -> unit Proofview.tactic
val injHyp : Names.Id.t -> unit Proofview.tactic
-val refine_tac : Evd.open_constr -> unit Proofview.tactic
+(* val refine_tac : Evd.open_constr -> unit Proofview.tactic *)
val onSomeWithHoles : ('a option -> unit Proofview.tactic) -> 'a Evd.sigma option -> unit Proofview.tactic
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 261e8583e..59bad5808 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -722,8 +722,6 @@ and intern_genarg ist x =
(intern_ident lf ist (out_gen (rawwit (wit_ident_gen b)) x))
| VarArgType ->
in_gen (glbwit wit_var) (intern_hyp ist (out_gen (rawwit wit_var) x))
- | RefArgType ->
- in_gen (glbwit wit_ref) (intern_global_reference ist (out_gen (rawwit wit_ref) x))
| GenArgType ->
in_gen (glbwit wit_genarg) (intern_genarg ist (out_gen (rawwit wit_genarg) x))
| ConstrArgType ->
@@ -736,9 +734,9 @@ and intern_genarg ist x =
(intern_quantified_hypothesis ist (out_gen (rawwit wit_quant_hyp) x))
| RedExprArgType ->
in_gen (glbwit wit_red_expr) (intern_red_expr ist (out_gen (rawwit wit_red_expr) x))
- | OpenConstrArgType b ->
- in_gen (glbwit (wit_open_constr_gen b))
- ((),intern_constr ist (snd (out_gen (rawwit (wit_open_constr_gen b)) x)))
+ | OpenConstrArgType ->
+ in_gen (glbwit wit_open_constr)
+ ((),intern_constr ist (snd (out_gen (rawwit wit_open_constr) x)))
| ConstrWithBindingsArgType ->
in_gen (glbwit wit_constr_with_bindings)
(intern_constr_with_bindings ist (out_gen (rawwit wit_constr_with_bindings) x))
@@ -800,6 +798,7 @@ let () =
Genintern.register_intern0 wit_intro_pattern intern_intro_pattern
let () =
+ Genintern.register_intern0 wit_ref (lift intern_global_reference);
Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg);
Genintern.register_intern0 wit_sort (fun ist s -> (ist, s))
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 0821423b5..e5f69378f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -144,7 +144,7 @@ let pr_inspect env expr result =
let pp_result =
if has_type result (topwit wit_tacvalue) then
match to_tacvalue result with
- | VRTactic _ -> str "a VRTactic"
+ | VRTactic -> str "a VRTactic"
| VFun (_, il, ul, b) ->
let pp_body = Pptactic.pr_glob_tactic env b in
let pr_sep () = str ", " in
@@ -1322,8 +1322,6 @@ and interp_genarg ist env sigma concl gl x =
(interp_fresh_ident ist env (out_gen (glbwit (wit_ident_gen b)) x))
| VarArgType ->
in_gen (topwit wit_var) (interp_hyp ist env (out_gen (glbwit wit_var) x))
- | RefArgType ->
- in_gen (topwit wit_ref) (interp_reference ist env (out_gen (glbwit wit_ref) x))
| GenArgType ->
in_gen (topwit wit_genarg) (interp_genarg (out_gen (glbwit wit_genarg) x))
| ConstrArgType ->
@@ -1346,13 +1344,12 @@ and interp_genarg ist env sigma concl gl x =
in
evdref := sigma;
in_gen (topwit wit_red_expr) r_interp
- | OpenConstrArgType casted ->
- let expected_type =
- if casted then OfType concl else WithoutTypeConstraint in
- in_gen (topwit (wit_open_constr_gen casted))
+ | OpenConstrArgType ->
+ let expected_type = WithoutTypeConstraint in
+ in_gen (topwit wit_open_constr)
(interp_open_constr ~expected_type
ist env !evdref
- (snd (out_gen (glbwit (wit_open_constr_gen casted)) x)))
+ (snd (out_gen (glbwit wit_open_constr) x)))
| ConstrWithBindingsArgType ->
in_gen (topwit wit_constr_with_bindings)
(pack_sigma (interp_constr_with_bindings ist env !evdref
@@ -1973,17 +1970,12 @@ and interp_atomic ist tac =
end
| VarArgType ->
Proofview.Goal.return (mk_hyp_value ist env (out_gen (glbwit wit_var) x))
- | RefArgType ->
- Proofview.Goal.return (
- Value.of_constr (
- constr_of_global
- (interp_reference ist env (out_gen (glbwit wit_ref) x))))
| GenArgType -> f (out_gen (glbwit wit_genarg) x)
| ConstrArgType ->
Proofview.Goal.return (Tacmach.New.of_old (fun gl -> mk_constr_value ist gl (out_gen (glbwit wit_constr) x)) gl) >>== fun (sigma,v) ->
(Proofview.V82.tclEVARS sigma) <*>
(Proofview.Goal.return v)
- | OpenConstrArgType false ->
+ | OpenConstrArgType ->
Proofview.Goal.return (
Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x))) gl) >>== fun (sigma,v) ->
(Proofview.V82.tclEVARS sigma) <*>
@@ -2043,7 +2035,7 @@ and interp_atomic ist tac =
Proofview.V82.tactic (tclEVARS newsigma) <*>
Proofview.Goal.return v
| QuantHypArgType | RedExprArgType
- | OpenConstrArgType _ | ConstrWithBindingsArgType
+ | ConstrWithBindingsArgType
| BindingsArgType
| OptArgType _ | PairArgType _
-> Proofview.tclZERO (UserError("" , str"This argument type is not supported in tactic notations."))
@@ -2154,6 +2146,8 @@ let () =
declare_uniform wit_pre_ident str
let () =
+ let interp ist gl ref = (project gl, interp_reference ist (pf_env gl) ref) in
+ Geninterp.register_interp0 wit_ref interp;
let interp ist gl pat = (project gl, interp_intro_pattern ist (pf_env gl) pat) in
Geninterp.register_interp0 wit_intro_pattern interp;
let interp ist gl s = (project gl, interp_sort s) in
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 7491c9a8f..206dec104 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -298,9 +298,6 @@ and subst_genarg subst (x:glob_generic_argument) =
| IdentArgType b ->
in_gen (glbwit (wit_ident_gen b)) (out_gen (glbwit (wit_ident_gen b)) x)
| VarArgType -> in_gen (glbwit wit_var) (out_gen (glbwit wit_var) x)
- | RefArgType ->
- in_gen (glbwit wit_ref) (subst_global_reference subst
- (out_gen (glbwit wit_ref) x))
| GenArgType -> in_gen (glbwit wit_genarg) (subst_genarg subst (out_gen (glbwit wit_genarg) x))
| ConstrArgType ->
in_gen (glbwit wit_constr) (subst_glob_constr subst (out_gen (glbwit wit_constr) x))
@@ -312,9 +309,9 @@ and subst_genarg subst (x:glob_generic_argument) =
(out_gen (glbwit wit_quant_hyp) x))
| RedExprArgType ->
in_gen (glbwit wit_red_expr) (subst_redexp subst (out_gen (glbwit wit_red_expr) x))
- | OpenConstrArgType b ->
- in_gen (glbwit (wit_open_constr_gen b))
- ((),subst_glob_constr subst (snd (out_gen (glbwit (wit_open_constr_gen b)) x)))
+ | OpenConstrArgType ->
+ in_gen (glbwit wit_open_constr)
+ ((),subst_glob_constr subst (snd (out_gen (glbwit wit_open_constr) x)))
| ConstrWithBindingsArgType ->
in_gen (glbwit wit_constr_with_bindings)
(subst_glob_with_bindings subst (out_gen (glbwit wit_constr_with_bindings) x))
@@ -330,6 +327,7 @@ and subst_genarg subst (x:glob_generic_argument) =
(** Registering *)
let () =
+ Genintern.register_subst0 wit_ref subst_global_reference;
Genintern.register_subst0 wit_intro_pattern (fun _ v -> v);
Genintern.register_subst0 wit_tactic subst_tactic;
Genintern.register_subst0 wit_sort (fun _ v -> v)
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 19:06:35 +0000