diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 4 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 11 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 6 |
3 files changed, 9 insertions, 12 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 49f073d663..1a879f911b 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -2501,14 +2501,14 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar in let tycon, arity = + let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in match tycon' with - | None -> let ev = mkExistential env evdref in ev, ev + | None -> let ev = mkExistential env evdref in ev, lift nar ev | Some t -> let pred = match prepare_predicate_from_arsign_tycon env !evdref loc tomatchs sign t with | Some (evd, pred) -> evdref := evd; pred | None -> - let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in lift nar t in Option.get tycon, pred in diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index a27debe735..b9cb7ba1b1 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -476,7 +476,7 @@ let rec detype flags avoid env sigma t = CAst.make @@ | _ -> GApp (f',args') in mkapp (detype flags avoid env sigma f) - (detype_array flags avoid env sigma args) + (Array.map_to_list (detype flags avoid env sigma) args) | Const (sp,u) -> GRef (ConstRef sp, detype_instance sigma u) | Proj (p,c) -> let noparams () = @@ -694,15 +694,6 @@ and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c = let t = if s != InProp && not !Flags.raw_print then None else Some (detype (lax,false) avoid env sigma ty) in GLetIn (na', c, t, r) -(** We use a dedicated function here to prevent overallocation from - Array.map_to_list. *) -and detype_array flags avoid env sigma args = - let ans = ref [] in - for i = Array.length args - 1 downto 0 do - ans := detype flags avoid env sigma args.(i) :: !ans; - done; - !ans - let detype_rel_context ?(lax=false) where avoid env sigma sign = let where = Option.map (fun c -> EConstr.it_mkLambda_or_LetIn c sign) where in let rec aux avoid env = function diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 76f35f76f5..708788ab87 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -557,6 +557,12 @@ let match_eval_ref_value env sigma constr stack = Some (EConstr.of_constr (constant_value_in env (sp, u))) else None + | Proj (p, c) when not (Projection.unfolded p) -> + reduction_effect_hook env sigma (EConstr.to_constr sigma constr) + (lazy (EConstr.to_constr sigma (applist (constr,stack)))); + if is_evaluable env (EvalConstRef (Projection.constant p)) then + Some (mkProj (Projection.unfold p, c)) + else None | Var id when is_evaluable env (EvalVarRef id) -> env |> lookup_named id |> NamedDecl.get_value | Rel n -> |