aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--toplevel/command.ml8
1 files changed, 5 insertions, 3 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 9267e236d8..47d4965285 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -215,9 +215,11 @@ let interp_assumption evdref env bl c =
let declare_assumptions idl is_coe k c imps impl_is_on nl =
!declare_assumptions_hook c;
- List.fold_left (fun (refs,status) id ->
- let ref',status' = declare_assumption is_coe k c imps impl_is_on nl id in
- ref'::refs, status' && status) ([],true) idl
+ let refs, status =
+ List.fold_left (fun (refs,status) id ->
+ let ref',status' = declare_assumption is_coe k c imps impl_is_on nl id in
+ ref'::refs, status' && status) ([],true) idl in
+ List.rev refs, status
let do_assumptions kind nl l =
let env = Global.env () in