diff options
| author | Pierre-Marie Pédrot | 2019-05-01 17:22:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-10 12:53:09 +0200 |
| commit | d313bc5c1439f1881b4c77b9d92400579d2168ce (patch) | |
| tree | ce7a1a70d614a9e679a0002ce88d2cecb3d223aa /proofs | |
| parent | f7c55014aabb0d607449868e2522515db0b40568 (diff) | |
Split the hypothesis conversion check in a conversion + ordering check.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 4 | ||||
| -rw-r--r-- | proofs/logic.mli | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 3fcde56e76..76eb79df39 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -548,7 +548,7 @@ 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 env 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 sign = Environ.named_context_val env in @@ -565,7 +565,7 @@ let convert_hyp ~check env sigma d = 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 check then reorder_val_context env sigma sign' (check_decl_position env sigma sign d) + 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 163d71f69c..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 : check:bool -> Environ.env -> 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 -> |