diff options
| author | Pierre-Marie Pédrot | 2016-01-29 17:27:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-01-29 18:03:50 +0100 |
| commit | 0b644da20c714b01565f88dffcfd51ea8f08314a (patch) | |
| tree | 5a63fe126f7ae1f5d0e9460234291dd3dd55a78b /pretyping | |
| parent | 4953a129858a231e64dec636a3bc15a54a0e771c (diff) | |
| parent | 22a2cc1897f0d9f568ebfb807673e84f6ada491a (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/indrec.ml | 14 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 10 |
2 files changed, 15 insertions, 9 deletions
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 92573a94fe..fb45be6635 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -156,7 +156,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = | Prod (n,t,c) -> let d = (n,None,t) in make_prod env (n,t,prec (push_rel d env) (i+1) (d::sign) c) - | LetIn (n,b,t,c) -> + | LetIn (n,b,t,c) when List.is_empty largs -> let d = (n,Some b,t) in mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::sign) c) | Ind (_,_) -> @@ -167,7 +167,10 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = base [|applist (mkRel (i+1), Context.Rel.to_extended_list 0 sign)|] else base - | _ -> assert false + | _ -> + let t' = whd_betadeltaiota env sigma p in + if Term.eq_constr p' t' then assert false + else prec env i sign t' in prec env 0 [] in @@ -231,14 +234,17 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = | Prod (n,t,c) -> let d = (n,None,t) in mkLambda_name env (n,t,prec (push_rel d env) (i+1) (d::hyps) c) - | LetIn (n,b,t,c) -> + | LetIn (n,b,t,c) when List.is_empty largs -> let d = (n,Some b,t) in mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c) | Ind _ -> let realargs = List.skipn nparrec largs and arg = appvect (mkRel (i+1), Context.Rel.to_extended_vect 0 hyps) in applist(lift i fk,realargs@[arg]) - | _ -> assert false + | _ -> + let t' = whd_betadeltaiota env sigma p in + if Term.eq_constr t' p' then assert false + else prec env i hyps t' in prec env 0 [] in diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 6166fffbc1..11fba7b941 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -133,12 +133,12 @@ let interp_universe_level_name evd (loc,s) = in evd, level else try - let id = - try Id.of_string s with _ -> raise Not_found in - evd, Idmap.find id names + let level = Evd.universe_of_name evd s in + evd, level with Not_found -> - try let level = Evd.universe_of_name evd s in - evd, level + try + let id = try Id.of_string s with _ -> raise Not_found in + evd, Idmap.find id names with Not_found -> if not (is_strict_universe_declarations ()) then new_univ_level_variable ~name:s univ_rigid evd |