aboutsummaryrefslogtreecommitdiff
path: root/toplevel/command.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/command.ml')
-rw-r--r--toplevel/command.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml
index d9193a8ff4..14381b7d7d 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -248,7 +248,6 @@ let build_recursive lnameargsardef =
(mkFix ((Array.of_list nvrec,i),
(varrec,List.map (fun id -> Name id) lnamerec,
recvec)));
- (* (mkFixDlam (Array.of_list nvrec) i varrec recvec); *)
const_entry_type = None }
in
declare_constant fi (ce, n);