diff options
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 28fb8cbe..b5228094 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -276,6 +276,7 @@ and align_tree nal isgoal (e,c as rhs) = match nal with match kind_of_term c with | Case (ci,p,c,cl) when eq_constr c (mkRel (List.index Name.equal na (fst (snd e)))) + && not (Int.equal (Array.length cl) 0) && (* don't contract if p dependent *) computable p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) -> let clauses = build_tree na isgoal e ci cl in @@ -301,7 +302,7 @@ and contract_branch isgoal e (cdn,can,mkpat,b) = let is_nondep_branch c l = try (* FIXME: do better using tags from l *) - let sign,ccl = decompose_lam_n_assum (List.length l) c in + let sign,ccl = decompose_lam_n_decls (List.length l) c in noccur_between 1 (rel_context_length sign) ccl with e when Errors.noncritical e -> (* Not eta-expanded or not reduced *) false @@ -400,7 +401,7 @@ let detype_sort sigma = function | Type u -> GType (if !print_universes - then [Pp.string_of_ppcmds (Univ.Universe.pr_with (Evd.pr_evd_level sigma) u)] + then [dl, Pp.string_of_ppcmds (Univ.Universe.pr_with (Evd.pr_evd_level sigma) u)] else []) type binder_kind = BProd | BLambda | BLetIn @@ -412,7 +413,7 @@ let detype_anonymous = ref (fun loc n -> anomaly ~label:"detype" (Pp.str "index let set_detype_anonymous f = detype_anonymous := f let detype_level sigma l = - GType (Some (Pp.string_of_ppcmds (Evd.pr_evd_level sigma l))) + GType (Some (dl, Pp.string_of_ppcmds (Evd.pr_evd_level sigma l))) let detype_instance sigma l = if Univ.Instance.is_empty l then None @@ -512,7 +513,7 @@ let rec detype flags avoid env sigma t = id,l with Not_found -> Id.of_string ("X" ^ string_of_int (Evar.repr evk)), - (Array.map_to_list (fun c -> (Id.of_string "A",c)) cl) + (Array.map_to_list (fun c -> (Id.of_string "__",c)) cl) in GEvar (dl,id, List.map (on_snd (detype flags avoid env sigma)) l) |