Partial review of removed dead code (r13460)

- The code detected unused in notation.ml revealed a bug.
- In term.ml, restored a (short) useless function for
  consistency/symmetry of the interface.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13463 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 0 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index 88bc4cc4ec..0e0d598a08 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -901,6 +901,11 @@ let mkNamedLambda_or_LetIn (id,body,t) c =
     | Some b -> mkNamedLetIn id b t c
 
 (* Constructs either [(x:t)c] or [c] where [x] is replaced by [b] *)
+let mkProd_wo_LetIn (na,body,t) c =
+  match body with
+    | None -> mkProd (na,  t, c)
+    | Some b -> subst1 b c
+
 let mkNamedProd_wo_LetIn (id,body,t) c =
   match body with
     | None -> mkNamedProd id t c