aboutsummaryrefslogtreecommitdiff
path: root/toplevel/command.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/command.ml')
-rw-r--r--toplevel/command.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 14381b7d7d..1fd4fc4034 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -223,7 +223,7 @@ let build_recursive lnameargsardef =
with e ->
States.unfreeze fs; raise e
in
- let recdef =
+ let recdef = (* TODO: remplacer mkCast par un appel à interp_casted_constr *)
try
List.map (fun (_,lparams,arityc,def) ->
interp_constr sigma rec_sign