From 09580d08476cfa3f50b8c9a347293525c9f022fc Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 8 Feb 2008 16:50:17 +0000
Subject: New "Preterm [ of id ] " command to show the preterm before giving it
 to Coq (solves part 2 of bug #1784). Add corresponding documentation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10530 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/subtac/g_subtac.ml4 | 5 +++++
 doc/refman/Program.tex      | 7 +++++--
 2 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index 337cd16967..b7cb7fb233 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -148,3 +148,8 @@ VERNAC COMMAND EXTEND Subtac_Show_Obligations
 | [ "Obligations" "of" ident(name) ] -> [ Subtac_obligations.show_obligations (Some name) ]
 | [ "Obligations" ] -> [ Subtac_obligations.show_obligations None ]
 END
+
+VERNAC COMMAND EXTEND Subtac_Show_Preterm
+| [ "Preterm" "of" ident(name) ] -> [ Subtac_obligations.show_term (Some name) ]
+| [ "Preterm" ] -> [ Subtac_obligations.show_term None ]
+END
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index 0d9422dd9a..6e3cb4c4b2 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -222,6 +222,8 @@ tactic is replaced by the default one if not specified.
   one (useful for mutually recursive definitions).
 \item {\tt Admit Obligations [of \ident]} Admits all
   obligations (does not work with structurally recursive programs).
+\item {\tt Preterm [of \ident]} Shows the term that will be fed to
+  the kernel once the obligations are solved. Useful for debugging.
 \end{itemize}
 
 The module {\tt Coq.Program.Tactics} defines the default tactic for solving
@@ -254,10 +256,11 @@ Program Fixpoint f (x : A | P) { measure size } :=
   You will then just have to prove that the measure decreases at each recursive
   call. There are three drawbacks though: 
   \begin{enumerate}
-  \item You have to define size yourself;
+  \item You have to define the measure yourself;
   \item The reduction is a little more involved, although it works
     using lazy evaluation;
-  \item Mutual recursion isn't possible anymore. What would it mean ?
+  \item Mutual recursion on the underlying inductive type isn't possible
+    anymore, but nested mutual recursion is always possible.
   \end{enumerate}
 \end{itemize}
 
-- 
cgit v1.2.3