diff options
| author | Matthieu Sozeau | 2014-04-07 13:07:26 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:59 +0200 |
| commit | 484e2c349e68b0284f278f691334d82001ee0f0e (patch) | |
| tree | 929910f466ed8cadbf6bb8a7b470e49f7f187190 | |
| parent | 4bc936b22f9ed1e90286f39c8d51c9f05c37b300 (diff) | |
- Fix RecTutorial, and mutual induction schemes getting the wrong names.
Now the universe inconsistency appears at [exact t] instead of the Defined :)
| -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 = |