Update documentation and document the "obligations" flag

doc/equations.tex

@@ -18,6 +18,7 @@
 \def\texttau{\ensuremath{\tau}}
 \def\textDelta{\ensuremath{\Delta}}
 \def\textGamma{\ensuremath{\Gamma}}
+\def\textforall{\ensuremath{\forall}}
 
 \setlength{\coqdocbaseindent}{1em}
 
@@ -56,7 +57,7 @@ \chapter*{Introduction}
 \cite{equationsreloaded}. This manual provides a documentation of the plugin
 commands (\autoref{cha:manual}) followed by a tutorial using basic
 examples (\autoref{cha:gentle-intro}).  More elaborate examples are
-available at \url{http://mattam82.github.io/Coq-Equations/examples}.
+available at \url{http://rocq-prover.github.io/equations/examples}.
 
 This manual describes version \eqnversion of the package.
 
@@ -75,7 +76,7 @@ \section*{Installation}
 \texttt{coq-hott} package before \Equations.
 
 The development version and detailed installation instructions are available at
-\url{http://mattam82.github.io/Coq-Equations}.
+\url{https://rocq-prover.github.io/equations}.
 
 \doparttoc
 \parttoc
@@ -91,13 +92,13 @@ \chapter{A gentle introduction to Equations}
 The source of this chapter that can be run in Coq with Equations
 installed is available at:
 
-\url{https://raw.githubusercontent.com/mattam82/Coq-Equations/main/doc/equations_intro.v}
+\url{https://raw.githubusercontent.com/rocq-prover/equations/main/doc/equations_intro.v}
 
 \input{equations_intro}
 
 \paragraph{Going further}
 
-More examples are available at \url{http://mattam82.github.io/Coq-Equations/examples}
+More examples are available at \url{https://rocq-prover.github.io/equations/examples}
 
 \bibliography{biblio}
 \addcontentsline{toc}{chapter}{Bibliography}

doc/equations_intro.v

@@ -331,7 +331,7 @@ Arguments Vector.cons {A} a {n} v : rename.
 
 Abbreviation vector := Vector.t.
 Abbreviation Vnil := Vector.nil.
-Abbreviationy Vcons := Vector.cons.
+Abbreviation Vcons := Vector.cons.
 
 Equations vmap {A B} (f : A -> B) {n} (v : vector A n) :
   vector B n :=
@@ -483,6 +483,7 @@ Check well_founded_t_subterm : forall A, WellFounded (t_subterm A).
     packed vector type. *)
 
 Module UnzipVect.
+Section UnzipVectSec.
   Context {A B : Type}.
 
   (** We can use the packed relation to do well-founded recursion on the vector.
@@ -499,6 +500,7 @@ Module UnzipVect.
   unzip (Vector.cons (pair x y) v) with unzip v := {
   | pair xs ys := (Vector.cons x xs, Vector.cons y ys) }.
 
+End UnzipVectSec.
 End UnzipVect.
 
 (** For the diagonal, it is easier to give [n] as the decreasing argument
@@ -573,4 +575,7 @@ End KAxiom.
     the graph and elimination principle for the function, and the propositional 
     equalities of the definition. Note that `eliminator=yes` forces `equations=yes`.
 
+  - [obligations] for using the obligation system to resolve obligations/holes.
+    (also depending on the global `Equations Obligations` flag).
+
 *)

doc/manual.tex

@@ -11,19 +11,19 @@ \subsection{Syntax of programs}
 \def\userref#1#2{\coqdockw{with}~#1~\textcoloneq~#2}
 \def\var#1{\coqdocvar{#1}}
 \def\figdefs{\begin{array}{llcl}
-  \texttt{term}, \texttt{type} & t, ~τ & \Coloneqq &
-  \coqdocvar{x} `| \lambda \coqdocvar{x} : \tau, t, R `| ∀ \coqdocvar{x} :
+  \texttt{term}, \texttt{type} & t, ~\tau & \Coloneqq &
+  \coqdocvar{x} `| \lambda \coqdocvar{x} : \tau, t, R `| \forall \coqdocvar{x} :
                                                     \tau, \tau' `|
   \mathbf{\lambda}\texttt{\{}\,\vecplus{\vec{up} \coloneqq t}\texttt{\}}
    \cdots \\
   \texttt{binding} & d & \Coloneqq & \texttt{(}\coqdocvar{x}~\texttt{:}~\tau\texttt{)} `|
   \texttt{(}\coqdocvar{x}~\textcoloneq~t~\texttt{:}~\tau\texttt{)} \\
-  \texttt{context} & Γ, Δ & \Coloneqq & \vec{d} \\
+  \texttt{context} & \textGamma, \textDelta & \Coloneqq & \vec{d} \\
   \texttt{programs} & progs & \Coloneqq & prog~\overrightarrow{mutual} \texttt{.} \\
   \texttt{mutual programs} & mutual & \Coloneqq & \coqdockw{with}~p `| where \\
   \texttt{where clause} & where & \Coloneqq & \coqdockw{where}~p `| \coqdockw{where}~not\\
   \texttt{notation} & not & \Coloneqq & \texttt{''}string\texttt{''}~\textcoloneq~t~(\texttt{:}~scope)?\\
-  \texttt{program} & p, prog & \Coloneqq & \coqdoccst{f}(\texttt{@\{} univ\_decl \texttt{\}})?~Γ~\texttt{:}~τ~(\coqdockw{by}~\textit{annot})?~\textcoloneq~clauses \\
+  \texttt{program} & p, prog & \Coloneqq & \coqdoccst{f}(\texttt{@\{} univ\_decl \texttt{\}})?~\textGamma~\texttt{:}~\texttau~(\coqdockw{by}~\textit{annot})?~\textcoloneq~clauses \\
   \texttt{annotation} & annot & \Coloneqq & \kw{struct}~\var{x}? `| \kw{wf}~t~R? \\
   \texttt{user clauses} & clauses & \Coloneqq & \vecplus{cl} `| \texttt{\{}\,\vec{cl}\,\texttt{\}} \\
   \texttt{user clause} & cl & \Coloneqq & \coqdoccst{f}~\vec{up}~n?~\texttt{;} `|
@@ -50,11 +50,11 @@ \subsection{Syntax of programs}
 fresh) identifier, an optional universe annotation, 
 a signature and a list of user clauses (order matters), along with an optional recursion annotation (see next
 section). The signature is simply a list of bindings and a result
-type. The expected type of the function \cst{f} is then $∀~Γ, τ$.
+type. The expected type of the function \cst{f} is then $\forall~\Gamma, \tau$.
 An empty set of clauses denotes that one of the variables has an empty type.
 
 Each user clause comprises a list of patterns that will match the
-bindings $Γ$ and an optional right hand side. Patterns can be named or
+bindings $\textGamma$ and an optional right hand side. Patterns can be named or
 anonymous variables, constructors applied to patterns, the inaccessible
 pattern \texttt{?(}t\texttt{)} (a.k.a. "dot" pattern in \Agda) or the
 empty pattern \texttt{!} indicating a variable has empty type (in this
@@ -168,6 +168,11 @@ \subsection{Local Options}
   graph and elimination principle, respectively. Note that \texttt{eliminator = yes} 
   forces \texttt{equations = yes}.
 
+- \texttt{obligations} (since v1.3.2) for using the obligation system to resolve
+  holes and obligations coming from well-founded recursive definitions (also
+  depending on the global \texttt{Equations Obligations} flag). If the
+  \kw{Equations?} syntax is used, the value this option and its global counterpart is ignored.
+
 The \emph{deprecated} syntax $opts$ is a list of flags among:
 
 \begin{itemize}
@@ -234,6 +239,10 @@ \subsection{Global Options}
   generation of the graph and functional elimination principle
   associated to a definition, governed locally by the
   \texttt{derive(eliminator)} attribute.
+
+\item \texttt{Equations Obligations} (since v1.3.2) this sets the default for the
+  use of the obligation system, governed locally by the \texttt{obligations}
+  attribute.
 \end{itemize}
 
 \section{Derive}
@@ -369,7 +378,7 @@ \section{Functional elimination}
 \newpage
 \section{Changes}
 
-\def\issue#1{\href{https://github.com/mattam82/Coq-Equations/issues/#1}{\texttt{\##1}}}
+\def\issue#1{\href{https://github.com/rocq-prover/equations/issues/#1}{\texttt{\##1}}}
 
 \begin{itemize}
 \item Version 1.3: 

src/equations_common.mli

@@ -33,12 +33,28 @@ val enter_goal : (Environ.env -> Evd.evar_map -> EConstr.t -> unit Proofview.tac
 (* Common flags *)
 type flags = {
   poly : PolyFlags.t;
+  (** Whether to use universe polymorphic or monomorphic definitions. *)
+
   obligations : bool;
+  (** Create obligations for unsolved goals. *)
+
   open_proof : bool;
+  (** Use interactive proof mode instead of obligations for unsolved goals. *)
+
   with_eqns : bool;
+  (** Generate equations corresponding to the clauses. *)
+
   with_ind : bool;
+  (** Generate the inductive graph and derived eliminator.
+      Implies [with_eqns]. *)
+
   allow_aliases : bool;
-  tactic : unit Proofview.tactic }
+  (** Allow two occurrences of a variable to be unified with different
+      values (one shadows the other). *)
+
+  tactic : unit Proofview.tactic;
+  (** The default tactic to try to solve obligations/holes. *)
+}
 
 (* Point-free composition *)
 val ( $ ) : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b