diff options
Diffstat (limited to 'vernac/comDefinition.ml')
| -rw-r--r-- | vernac/comDefinition.ml | 27 |
1 files changed, 15 insertions, 12 deletions
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index b9ed4f838d..37b7106856 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -29,14 +29,17 @@ let warn_implicits_in_term = let check_imps ~impsty ~impsbody = let rec aux impsty impsbody = - match impsty, impsbody with - | a1 :: impsty, a2 :: impsbody -> - (match a1.CAst.v, a2.CAst.v with - | None , None -> aux impsty impsbody - | Some _ , Some _ -> aux impsty impsbody - | _, _ -> warn_implicits_in_term ?loc:a2.CAst.loc ()) - | _ :: _, [] | [], _ :: _ -> (* Information only on one side *) () - | [], [] -> () in + match impsty, impsbody with + | a1 :: impsty, a2 :: impsbody -> + let () = match a1.CAst.v, a2.CAst.v with + | None , None | Some _, None -> () + | Some (_,b1) , Some (_,b2) -> + if not ((b1:bool) = b2) then warn_implicits_in_term ?loc:a2.CAst.loc () + | None, Some _ -> warn_implicits_in_term ?loc:a2.CAst.loc () + in + aux impsty impsbody + | _ :: _, [] | [], _ :: _ -> (* Information only on one side *) () + | [], [] -> () in aux impsty impsbody let protect_pattern_in_binder bl c ctypopt = @@ -122,14 +125,14 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = Declare.declare_definition ~info ~cinfo ~opaque:false ~body evd in () -let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = +let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = let program_mode = true in let (body, types), evd, udecl, impargs = interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in let term, typ, uctx, obls = Declare.Obls.prepare_obligation ~name ~body ~types evd in - let _ : Declare.Obls.progress = + let pm, _ = let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in let info = Declare.Info.make ~udecl ~scope ~poly ~kind ?hook () in - Declare.Obls.add_definition ~cinfo ~info ~term ~uctx obls - in () + Declare.Obls.add_definition ~pm ~cinfo ~info ~term ~uctx obls + in pm |