diff options
author | 2014-09-25 19:45:38 +0200 | |
---|---|---|
committer | 2014-09-25 19:46:58 +0200 | |
commit | 0fb36157b9ba2a177d2d1ddcf060f4e2f720d6cb (patch) | |
tree | f9e86e8680da3d3f1f195d4342e6538bf42be0b8 /pretyping | |
parent | 8548fbe4dea2869fba10203218bad06bbaf2ed36 (diff) |
Fix incorrect assert false in detyping.
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/detyping.ml | 19 |
1 files changed, 12 insertions, 7 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index d691acb45..07540af57 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -32,6 +32,10 @@ let dl = Loc.ghost let print_universes = Flags.univ_print let add_name na b t (nenv, env) = add_name na nenv, push_rel (na, b, t) env +let add_name_opt na b t (nenv, env) = + match t with + | None -> Termops.add_name na nenv, env + | Some t -> add_name na b t (nenv, env) (****************************************************************************) (* Tools for printing of Cases *) @@ -230,15 +234,16 @@ let rec decomp_branch ndecls nargs nal b (avoid,env as e) c = else let na,c,f,nargs',body,t = match kind_of_term (strip_outer_cast c) with - | Lambda (na,t,c) -> na,c,compute_displayed_let_name_in,nargs-1,None,t + | Lambda (na,t,c) -> na,c,compute_displayed_let_name_in,nargs-1,None,Some t | LetIn (na,b,t,c) when ndecls>nargs -> - na,c,compute_displayed_name_in,nargs,Some b,t - | LetIn (na,b,t,c) -> - Name default_dependent_ident,(applist (lift 1 c, [mkRel 1])), - compute_displayed_name_in,nargs-1,Some b,t - | _ -> assert false in + na,c,compute_displayed_name_in,nargs,Some b,Some t + | _ -> + Name default_dependent_ident,(applist (lift 1 c, [mkRel 1])), + compute_displayed_name_in,nargs-1,None,None + in let na',avoid' = f flag avoid na c in - decomp_branch (ndecls-1) nargs' (na'::nal) b (avoid',add_name na' body t env) c + decomp_branch (ndecls-1) nargs' (na'::nal) b + (avoid', add_name_opt na' body t env) c let rec build_tree na isgoal e ci cl = let mkpat n rhs pl = PatCstr(dl,(ci.ci_ind,n+1),pl,update_name na rhs) in |