diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 50 | ||||
| -rw-r--r-- | proofs/logic.mli | 2 |
2 files changed, 23 insertions, 29 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index a01ddf2388..b79e1e6024 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -78,14 +78,6 @@ let error_no_such_hypothesis env sigma id = raise (RefinerError (env, sigma, NoS let check = ref false let with_check = Flags.with_option check -(* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and - returns [tail::(f head (id,_,_) (rev tail))] *) -let apply_to_hyp env sigma check sign id f = - try apply_to_hyp sign id f - with Hyp_not_found -> - if check then error_no_such_hypothesis env sigma id - else sign - let check_typability env sigma c = if !check then let _ = unsafe_type_of env sigma (EConstr.of_constr c) in () @@ -161,12 +153,14 @@ let reorder_context env sigma sign ord = step ord ords sign mt_q [] let reorder_val_context env sigma sign ord = +match ord with +| [] | [_] -> + (* Single variable-free definitions need not be reordered *) + sign +| _ :: _ :: _ -> let open EConstr in val_of_named_context (reorder_context env sigma (named_context_of_val sign) ord) - - - let check_decl_position env sigma sign d = let open EConstr in let x = NamedDecl.get_id d in @@ -556,25 +550,25 @@ and treat_case sigma goal ci lbrty lf acc' = (lacc,sigma,fi::bacc)) (acc',sigma,[]) lbrty lf ci.ci_pp_info.cstr_tags -let convert_hyp check sign sigma d = +let convert_hyp ~check ~reorder env sigma d = let id = NamedDecl.get_id d in let b = NamedDecl.get_value d in - let env = Global.env () in - let reorder = ref [] in - let sign' = - apply_to_hyp env sigma check sign id - (fun _ d' _ -> - let c = Option.map EConstr.of_constr (NamedDecl.get_value d') in - let env = Global.env_of_context sign in - if check && not (is_conv env sigma (NamedDecl.get_type d) (EConstr.of_constr (NamedDecl.get_type d'))) then - user_err ~hdr:"Logic.convert_hyp" - (str "Incorrect change of the type of " ++ Id.print id ++ str "."); - if check && not (Option.equal (is_conv env sigma) b c) then - user_err ~hdr:"Logic.convert_hyp" - (str "Incorrect change of the body of "++ Id.print id ++ str "."); - if check then reorder := check_decl_position env sigma sign d; - map_named_decl EConstr.Unsafe.to_constr d) in - reorder_val_context env sigma sign' !reorder + let sign = Environ.named_context_val env in + match lookup_named_ctxt id sign with + | exception Not_found -> + if check then error_no_such_hypothesis env sigma id + else sign + | d' -> + let c = Option.map EConstr.of_constr (NamedDecl.get_value d') in + if check && not (is_conv env sigma (NamedDecl.get_type d) (EConstr.of_constr (NamedDecl.get_type d'))) then + user_err ~hdr:"Logic.convert_hyp" + (str "Incorrect change of the type of " ++ Id.print id ++ str "."); + if check && not (Option.equal (is_conv env sigma) b c) then + user_err ~hdr:"Logic.convert_hyp" + (str "Incorrect change of the body of "++ Id.print id ++ str "."); + let sign' = apply_to_hyp sign id (fun _ _ _ -> EConstr.Unsafe.to_named_decl d) in + if reorder then reorder_val_context env sigma sign' (check_decl_position env sigma sign d) + else sign' (************************************************************************) (************************************************************************) diff --git a/proofs/logic.mli b/proofs/logic.mli index f99076db23..406fe57985 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -62,7 +62,7 @@ type 'id move_location = val pr_move_location : ('a -> Pp.t) -> 'a move_location -> Pp.t -val convert_hyp : bool -> Environ.named_context_val -> evar_map -> +val convert_hyp : check:bool -> reorder:bool -> Environ.env -> evar_map -> EConstr.named_declaration -> Environ.named_context_val val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t move_location -> |