diff options
Diffstat (limited to 'vernac/comAssumption.ml')
| -rw-r--r-- | vernac/comAssumption.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 37a33daf8f..d7bd64067b 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -42,7 +42,7 @@ let should_axiom_into_instance = function true | Global | Local -> !axiom_into_instance -let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl {CAst.v=ident} = +let declare_assumption ~pstate is_coe (local,p,kind) (c,ctx) pl imps impl nl {CAst.v=ident} = match local with | Discharge when Lib.sections_are_opened () -> let ctx = match ctx with @@ -53,7 +53,7 @@ match local with let _ = declare_variable ident decl in let () = assumption_message ident in let () = - if not !Flags.quiet && Proof_global.there_are_pending_proofs () then + if not !Flags.quiet && Option.has_some pstate then Feedback.msg_info Pp.(str"Variable" ++ spc () ++ Id.print ident ++ strbrk " is not visible from current goals") in @@ -96,11 +96,11 @@ let next_uctx = | Polymorphic_entry _ as uctx -> uctx | Monomorphic_entry _ -> empty_uctx -let declare_assumptions idl is_coe k (c,uctx) pl imps nl = +let declare_assumptions ~pstate idl is_coe k (c,uctx) pl imps nl = let refs, status, _ = List.fold_left (fun (refs,status,uctx) id -> let ref',u',status' = - declare_assumption is_coe k (c,uctx) pl imps false nl id in + declare_assumption ~pstate is_coe k (c,uctx) pl imps false nl id in (ref',u')::refs, status' && status, next_uctx uctx) ([],true,uctx) idl in @@ -132,7 +132,7 @@ let process_assumptions_udecls kind l = in udecl, List.map (fun (coe, (idl, c)) -> coe, (List.map fst idl, c)) l -let do_assumptions ~program_mode kind nl l = +let do_assumptions ~pstate ~program_mode kind nl l = let open Context.Named.Declaration in let env = Global.env () in let udecl, l = process_assumptions_udecls kind l in @@ -173,7 +173,7 @@ let do_assumptions ~program_mode kind nl l = let ubinders = Evd.universe_binders sigma in pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),t,imps) -> let t = replace_vars subst t in - let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps nl in + let refs, status' = declare_assumptions ~pstate idl is_coe kind (t,uctx) ubinders imps nl in let subst' = List.map2 (fun {CAst.v=id} (c,u) -> (id, Constr.mkRef (c,u))) idl refs |