From d313bc5c1439f1881b4c77b9d92400579d2168ce Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 1 May 2019 17:22:42 +0200
Subject: Split the hypothesis conversion check in a conversion + ordering
 check.

---
 proofs/logic.ml  | 4 ++--
 proofs/logic.mli | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'proofs')

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 ->
-- 
cgit v1.2.3