diff options
| -rw-r--r-- | engine/termops.ml | 13 | ||||
| -rw-r--r-- | engine/termops.mli | 6 | ||||
| -rw-r--r-- | proofs/logic.ml | 32 |
3 files changed, 34 insertions, 17 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index d60aa69ccb..a0248fa01b 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -839,6 +839,16 @@ let occur_var env sigma id c = in try occur_rec c; false with Occur -> true +let occur_vars env sigma ids c = + let rec occur_rec c = + match EConstr.destRef sigma c with + | gr, _ -> + let vars = vars_of_global env gr in + if not (Id.Set.is_empty (Id.Set.inter ids vars)) then raise Occur + | exception DestKO -> EConstr.iter sigma occur_rec c + in + try occur_rec c; false with Occur -> true + exception OccurInGlobal of GlobRef.t let occur_var_indirectly env sigma id c = @@ -853,6 +863,9 @@ let occur_var_indirectly env sigma id c = let occur_var_in_decl env sigma hyp decl = NamedDecl.exists (occur_var env sigma hyp) decl +let occur_vars_in_decl env sigma hyps decl = + NamedDecl.exists (occur_vars env sigma hyps) decl + let local_occur_var sigma id c = let rec occur c = match EConstr.kind sigma c with | Var id' -> if Id.equal id id' then raise Occur diff --git a/engine/termops.mli b/engine/termops.mli index bdde2c450d..0faebecb1b 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -89,9 +89,9 @@ val occur_metavariable : Evd.evar_map -> metavariable -> constr -> bool val occur_evar : Evd.evar_map -> Evar.t -> constr -> bool val occur_var : env -> Evd.evar_map -> Id.t -> constr -> bool val occur_var_indirectly : env -> Evd.evar_map -> Id.t -> constr -> GlobRef.t option -val occur_var_in_decl : - env -> Evd.evar_map -> - Id.t -> named_declaration -> bool +val occur_var_in_decl : env -> Evd.evar_map -> Id.t -> named_declaration -> bool +val occur_vars : env -> Evd.evar_map -> Id.Set.t -> constr -> bool +val occur_vars_in_decl : env -> Evd.evar_map -> Id.Set.t -> named_declaration -> bool (** As {!occur_var} but assume the identifier not to be a section variable *) val local_occur_var : Evd.evar_map -> Id.t -> constr -> bool diff --git a/proofs/logic.ml b/proofs/logic.ml index c57a9344ff..f5c84be465 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -186,56 +186,60 @@ let move_hyp env sigma toleft (left,declfrom,right) hto = let open EConstr in let push prefix sign = List.fold_right push_named_context_val prefix sign in let push_rev prefix sign = List.fold_left (fun accu d -> push_named_context_val d accu) sign prefix in - let rec moverec_toleft ans first middle = function + let rec moverec_toleft ans first middle midvars = function | [] -> push middle @@ push first ans | d :: _ as right when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) -> push_rev right @@ push middle @@ push first ans | d :: right -> let hyp = NamedDecl.get_id d in - let (first',middle') = - if List.exists (fun d2 -> occur_var_in_decl env sigma (NamedDecl.get_id d2) d) middle then + let (first', middle', midvars') = + if occur_vars_in_decl env sigma midvars d then if not (move_location_eq hto (MoveAfter hyp)) then - (first, d::middle) + (first, d :: middle, Id.Set.add hyp midvars) else user_err ~hdr:"move_hyp" (str "Cannot move " ++ Id.print (NamedDecl.get_id declfrom) ++ pr_move_location Id.print hto ++ str ": it occurs in the type of " ++ Id.print hyp ++ str ".") else - (d::first, middle) + (d::first, middle, midvars) in if move_location_eq hto (MoveAfter hyp) then push_rev right @@ push middle' @@ push first' ans else - moverec_toleft ans first' middle' right + moverec_toleft ans first' middle' midvars' right in - let rec moverec_toright first middle right = match EConstr.match_named_context_val right with + let rec moverec_toright first middle depvars right = match EConstr.match_named_context_val right with | None -> push_rev first @@ push_rev middle right | Some (d, _, _) when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) -> push_rev first @@ push_rev middle @@ right | Some (d, _, right) -> let hyp = NamedDecl.get_id d in - let (first',middle') = - if List.exists (fun d2 -> occur_var_in_decl env sigma hyp d2) middle then + let (first', middle', depvars') = + if Id.Set.mem hyp depvars then if not (move_location_eq hto (MoveAfter hyp)) then - (first, d::middle) + let vars = global_vars_set_of_decl env sigma d in + let depvars = Id.Set.union vars depvars in + (first, d::middle, depvars) else user_err ~hdr:"move_hyp" (str "Cannot move " ++ Id.print (NamedDecl.get_id declfrom) ++ pr_move_location Id.print hto ++ str ": it depends on " ++ Id.print hyp ++ str ".") else - (d::first, middle) + (d::first, middle, depvars) in if move_location_eq hto (MoveAfter hyp) then push_rev first' @@ push_rev middle' @@ right else - moverec_toright first' middle' right + moverec_toright first' middle' depvars' right in if toleft then - moverec_toleft right [] [declfrom] left + let id = NamedDecl.get_id declfrom in + moverec_toleft right [] [declfrom] (Id.Set.singleton id) left else - let right = moverec_toright [] [declfrom] right in + let depvars = global_vars_set_of_decl env sigma declfrom in + let right = moverec_toright [] [declfrom] depvars right in push_rev left @@ right let move_hyp_in_named_context env sigma hfrom hto sign = |