diff options
| -rw-r--r-- | test-suite/success/RecTutorial.v | 3 | ||||
| -rw-r--r-- | toplevel/indschemes.ml | 6 |
2 files changed, 4 insertions, 5 deletions
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v index 15af084424..11fbf24d4d 100644 --- a/test-suite/success/RecTutorial.v +++ b/test-suite/success/RecTutorial.v @@ -520,8 +520,7 @@ Inductive typ : Type := Definition typ_inject: typ. split. -exact typ. -Fail Defined. +Fail exact typ. (* Error: Universe Inconsistency. *) diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index ac3bf59295..a5e30b210f 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -351,11 +351,11 @@ let do_mutual_induction_scheme lnamedepindsort = let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort and env0 = Global.env() in let sigma, lrecspec = - List.fold_left - (fun (evd, l) (_,dep,ind,sort) -> + List.fold_right + (fun (_,dep,ind,sort) (evd, l) -> let evd, indu = Evd.fresh_inductive_instance env0 evd ind in (evd, (indu,dep,interp_elimination_sort sort) :: l)) - (Evd.from_env env0,[]) lnamedepindsort + lnamedepindsort (Evd.from_env env0,[]) in let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in let declare decl fi lrecref = |