diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/classes.ml | 339 | ||||
| -rw-r--r-- | vernac/classes.mli | 2 | ||||
| -rw-r--r-- | vernac/explainErr.ml | 4 | ||||
| -rw-r--r-- | vernac/himsg.ml | 28 | ||||
| -rw-r--r-- | vernac/himsg.mli | 2 | ||||
| -rw-r--r-- | vernac/indschemes.ml | 45 |
6 files changed, 218 insertions, 202 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index e491761aec..c738d14af9 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -121,19 +121,167 @@ let declare_instance_constant k info global imps ?hook id decl poly sigma term t Evd.restrict_universe_context sigma levels in let uctx = Evd.check_univ_decl ~poly sigma decl in - let entry = - Declare.definition_entry ~types:termtype ~univs:uctx term - in + let entry = Declare.definition_entry ~types:termtype ~univs:uctx term in let cdecl = (DefinitionEntry entry, kind) in let kn = Declare.declare_constant id cdecl in - Declare.definition_message id; - Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders sigma); - instance_hook k info global imps ?hook (ConstRef kn); - id + Declare.definition_message id; + Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders sigma); + instance_hook k info global imps ?hook (ConstRef kn) + +let do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imps subst id = + let subst = List.fold_left2 + (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst') + [] subst (snd k.cl_context) + in + let (_, ty_constr) = instance_constructor (k,u) subst in + let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in + let sigma = Evd.minimize_universes sigma in + Pretyping.check_evars env (Evd.from_env env) sigma termtype; + let univs = Evd.check_univ_decl ~poly sigma decl in + let termtype = to_constr sigma termtype in + let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id + (ParameterEntry + (None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical) + in + Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma); + instance_hook k pri global imps ?hook (ConstRef cst); id -let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) - ~program_mode poly ctx (instid, bk, cl) props ?(generalize=true) - ?(tac:unit Proofview.tactic option) ?hook pri = +let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl len term termtype = + let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in + if program_mode then + let hook vis gr _ = + let cst = match gr with ConstRef kn -> kn | _ -> assert false in + Impargs.declare_manual_implicits false gr ~enriching:false [imps]; + let pri = intern_info pri in + Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst) + in + let obls, constr, typ = + match term with + | Some t -> + let obls, _, constr, typ = + Obligations.eterm_obligations env id sigma 0 t termtype + in obls, Some constr, typ + | None -> [||], None, termtype + in + let hook = Lemmas.mk_hook hook in + let ctx = Evd.evar_universe_context sigma in + ignore (Obligations.add_definition id ?term:constr + ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls) + else + Flags.silently (fun () -> + (* spiwack: it is hard to reorder the actions to do + the pretyping after the proof has opened. As a + consequence, we use the low-level primitives to code + the refinement manually.*) + let gls = List.rev (Evd.future_goals sigma) in + let sigma = Evd.reset_future_goals sigma in + Lemmas.start_proof id ~pl:decl kind sigma (EConstr.of_constr termtype) + (Lemmas.mk_hook + (fun _ -> instance_hook k pri global imps ?hook)); + (* spiwack: I don't know what to do with the status here. *) + if not (Option.is_empty term) then + let init_refine = + Tacticals.New.tclTHENLIST [ + Refine.refine ~typecheck:false (fun sigma -> (sigma,EConstr.of_constr (Option.get term))); + Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls); + Tactics.New.reduce_after_refine; + ] + in + ignore (Pfedit.by init_refine) + else if Flags.is_auto_intros () then + ignore (Pfedit.by (Tacticals.New.tclDO len Tactics.intro)); + (match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) () + +let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props len = + let props = + match props with + | Some (true, { CAst.v = CRecord fs }) -> + if List.length fs > List.length k.cl_props then + mismatched_props env' (List.map snd fs) k.cl_props; + Some (Inl fs) + | Some (_, t) -> Some (Inr t) + | None -> + if program_mode then Some (Inl []) + else None + in + let subst, sigma = + match props with + | None -> + (if List.is_empty k.cl_props then Some (Inl subst) else None), sigma + | Some (Inr term) -> + let sigma, c = interp_casted_constr_evars env' sigma term cty in + Some (Inr (c, subst)), sigma + | Some (Inl props) -> + let get_id qid = CAst.make ?loc:qid.CAst.loc @@ qualid_basename qid in + let props, rest = + List.fold_left + (fun (props, rest) decl -> + if is_local_assum decl then + try + let is_id (id', _) = match RelDecl.get_name decl, get_id id' with + | Name id, {CAst.v=id'} -> Id.equal id id' + | Anonymous, _ -> false + in + let (loc_mid, c) = List.find is_id rest in + let rest' = List.filter (fun v -> not (is_id v)) rest + in + let {CAst.loc;v=mid} = get_id loc_mid in + List.iter (fun (n, _, x) -> + if Name.equal n (Name mid) then + Option.iter (fun x -> Dumpglob.add_glob ?loc (ConstRef x)) x) k.cl_projs; + c :: props, rest' + with Not_found -> + ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Namegen.IntroAnonymous, None)) :: props), rest + else props, rest) + ([], props) k.cl_props + in + match rest with + | (n, _) :: _ -> + unbound_method env' k.cl_impl (get_id n) + | _ -> + let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in + let sigma, res = type_ctx_instance (push_rel_context ctx' env') sigma kcl_props props subst in + Some (Inl res), sigma + in + let term, termtype = + match subst with + | None -> let termtype = it_mkProd_or_LetIn cty ctx in + None, termtype + | Some (Inl subst) -> + let subst = List.fold_left2 + (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst') + [] subst (k.cl_props @ snd k.cl_context) + in + let (app, ty_constr) = instance_constructor (k,u) subst in + let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in + let term = it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in + Some term, termtype + | Some (Inr (def, subst)) -> + let termtype = it_mkProd_or_LetIn cty ctx in + let term = it_mkLambda_or_LetIn def ctx in + Some term, termtype + in + let sigma = Evarutil.nf_evar_map sigma in + let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals_or_obligations ~fail:true env sigma in + (* Try resolving fields that are typeclasses automatically. *) + let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:false env sigma in + let sigma = Evarutil.nf_evar_map_undefined sigma in + (* Beware of this step, it is required as to minimize universes. *) + let sigma = Evd.minimize_universes sigma in + (* Check that the type is free of evars now. *) + Pretyping.check_evars env (Evd.from_env env) sigma termtype; + let termtype = to_constr sigma termtype in + let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in + if not (Evd.has_undefined sigma) && not (Option.is_empty term) then + declare_instance_constant k pri global imps ?hook id decl poly sigma (Option.get term) termtype + else if program_mode || refine || Option.is_empty term then + declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl len term termtype + else CErrors.user_err Pp.(str "Unsolved obligations remaining."); + id + +let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~program_mode + poly ctx (instid, bk, cl) props + ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri = let env = Global.env() in let ({CAst.loc;v=instid}, pl) = instid in let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in @@ -150,9 +298,9 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) cl | Explicit -> cl, Id.Set.empty in - let tclass = - if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass) - else tclass + let tclass = + if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass) + else tclass in let sigma, k, u, cty, ctx', ctx, len, imps, subst = let sigma, (impls, ((env', ctx), imps)) = interp_context_evars env sigma ctx in @@ -189,163 +337,12 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) let env' = push_rel_context ctx env in let sigma = Evarutil.nf_evar_map sigma in let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in - if abstract then - begin - let subst = List.fold_left2 - (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst') - [] subst (snd k.cl_context) - in - let (_, ty_constr) = instance_constructor (k,u) subst in - let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - let sigma = Evd.minimize_universes sigma in - Pretyping.check_evars env (Evd.from_env env) sigma termtype; - let univs = Evd.check_univ_decl ~poly sigma decl in - let termtype = to_constr sigma termtype in - let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id - (ParameterEntry - (None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical) - in - Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma); - instance_hook k pri global imps ?hook (ConstRef cst); id - end - else ( - let props = - match props with - | Some (true, { CAst.v = CRecord fs }) -> - if List.length fs > List.length k.cl_props then - mismatched_props env' (List.map snd fs) k.cl_props; - Some (Inl fs) - | Some (_, t) -> Some (Inr t) - | None -> - if program_mode then Some (Inl []) - else None - in - let subst, sigma = - match props with - | None -> - (if List.is_empty k.cl_props then Some (Inl subst) else None), sigma - | Some (Inr term) -> - let sigma, c = interp_casted_constr_evars env' sigma term cty in - Some (Inr (c, subst)), sigma - | Some (Inl props) -> - let get_id qid = CAst.make ?loc:qid.CAst.loc @@ qualid_basename qid in - let props, rest = - List.fold_left - (fun (props, rest) decl -> - if is_local_assum decl then - try - let is_id (id', _) = match RelDecl.get_name decl, get_id id' with - | Name id, {CAst.v=id'} -> Id.equal id id' - | Anonymous, _ -> false - in - let (loc_mid, c) = - List.find is_id rest - in - let rest' = - List.filter (fun v -> not (is_id v)) rest - in - let {CAst.loc;v=mid} = get_id loc_mid in - List.iter (fun (n, _, x) -> - if Name.equal n (Name mid) then - Option.iter (fun x -> Dumpglob.add_glob ?loc (ConstRef x)) x) - k.cl_projs; - c :: props, rest' - with Not_found -> - ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Namegen.IntroAnonymous, None)) :: props), rest - else props, rest) - ([], props) k.cl_props - in - match rest with - | (n, _) :: _ -> - unbound_method env' k.cl_impl (get_id n) - | _ -> - let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in - let sigma, res = type_ctx_instance (push_rel_context ctx' env') sigma kcl_props props subst in - Some (Inl res), sigma - in - let term, termtype = - match subst with - | None -> let termtype = it_mkProd_or_LetIn cty ctx in - None, termtype - | Some (Inl subst) -> - let subst = List.fold_left2 - (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst') - [] subst (k.cl_props @ snd k.cl_context) - in - let (app, ty_constr) = instance_constructor (k,u) subst in - let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - let term = it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in - Some term, termtype - | Some (Inr (def, subst)) -> - let termtype = it_mkProd_or_LetIn cty ctx in - let term = it_mkLambda_or_LetIn def ctx in - Some term, termtype - in - let sigma = Evarutil.nf_evar_map sigma in - let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals_or_obligations ~fail:true env sigma in - (* Try resolving fields that are typeclasses automatically. *) - let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:false env sigma in - let sigma = Evarutil.nf_evar_map_undefined sigma in - (* Beware of this step, it is required as to minimize universes. *) - let sigma = Evd.minimize_universes sigma in - (* Check that the type is free of evars now. *) - Pretyping.check_evars env (Evd.from_env env) sigma termtype; - let termtype = to_constr sigma termtype in - let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in - if not (Evd.has_undefined sigma) && not (Option.is_empty term) then - declare_instance_constant k pri global imps ?hook id decl - poly sigma (Option.get term) termtype - else if program_mode || refine || Option.is_empty term then begin - let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in - if program_mode then - let hook vis gr _ = - let cst = match gr with ConstRef kn -> kn | _ -> assert false in - Impargs.declare_manual_implicits false gr ~enriching:false [imps]; - let pri = intern_info pri in - Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst) - in - let obls, constr, typ = - match term with - | Some t -> - let obls, _, constr, typ = - Obligations.eterm_obligations env id sigma 0 t termtype - in obls, Some constr, typ - | None -> [||], None, termtype - in - let hook = Lemmas.mk_hook hook in - let ctx = Evd.evar_universe_context sigma in - ignore (Obligations.add_definition id ?term:constr - ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls); - id - else - (Flags.silently - (fun () -> - (* spiwack: it is hard to reorder the actions to do - the pretyping after the proof has opened. As a - consequence, we use the low-level primitives to code - the refinement manually.*) - let gls = List.rev (Evd.future_goals sigma) in - let sigma = Evd.reset_future_goals sigma in - Lemmas.start_proof id ~pl:decl kind sigma (EConstr.of_constr termtype) - (Lemmas.mk_hook - (fun _ -> instance_hook k pri global imps ?hook)); - (* spiwack: I don't know what to do with the status here. *) - if not (Option.is_empty term) then - let init_refine = - Tacticals.New.tclTHENLIST [ - Refine.refine ~typecheck:false (fun sigma -> (sigma,EConstr.of_constr (Option.get term))); - Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls); - Tactics.New.reduce_after_refine; - ] - in - ignore (Pfedit.by init_refine) - else if Flags.is_auto_intros () then - ignore (Pfedit.by (Tacticals.New.tclDO len Tactics.intro)); - (match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) (); - id) - end - else CErrors.user_err Pp.(str "Unsolved obligations remaining.")) - + if abstract then + do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imps subst id + else + do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode + cty k u ctx ctx' pri decl imps subst id props len + let named_of_rel_context l = let open Vars in let acc, ctx = @@ -433,5 +430,5 @@ let context poly l = Lib.sections_are_opened () || Lib.is_modtype_strict () in status && nstatus - in + in List.fold_left fn true (List.rev ctx) diff --git a/vernac/classes.mli b/vernac/classes.mli index 9c37364cb0..bb70334342 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -37,7 +37,7 @@ val declare_instance_constant : Evd.evar_map -> (* Universes *) Constr.t -> (** body *) Constr.types -> (** type *) - Names.Id.t + unit val new_instance : ?abstract:bool -> (** Not abstract by default. *) diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index 7cf4e64805..b37fce645a 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -76,8 +76,8 @@ let process_vernac_interp_error exn = match fst exn with wrap_vernac_error exn (Himsg.explain_module_error e) | Modintern.ModuleInternalizationError e -> wrap_vernac_error exn (Himsg.explain_module_internalization_error e) - | RecursionSchemeError e -> - wrap_vernac_error exn (Himsg.explain_recursion_scheme_error e) + | RecursionSchemeError (env,e) -> + wrap_vernac_error exn (Himsg.explain_recursion_scheme_error env e) | Cases.PatternMatchingError (env,sigma,e) -> wrap_vernac_error exn (Himsg.explain_pattern_matching_error env sigma e) | Tacred.ReductionTacticError e -> diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 71155d7921..a4b3a75c9f 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -601,12 +601,12 @@ let explain_var_not_found env id = spc () ++ str "in the current" ++ spc () ++ str "environment" ++ str "." let explain_wrong_case_info env (ind,u) ci = - let pi = pr_inductive (Global.env()) ind in + let pi = pr_inductive env ind in if eq_ind ci.ci_ind ind then str "Pattern-matching expression on an object of inductive type" ++ spc () ++ pi ++ spc () ++ str "has invalid information." else - let pc = pr_inductive (Global.env()) ci.ci_ind in + let pc = pr_inductive env ci.ci_ind in str "A term of inductive type" ++ spc () ++ pi ++ spc () ++ str "was given to a pattern-matching expression on the inductive type" ++ spc () ++ pc ++ str "." @@ -1156,24 +1156,24 @@ let error_large_non_prop_inductive_not_in_type () = (* Recursion schemes errors *) -let error_not_allowed_case_analysis isrec kind i = +let error_not_allowed_case_analysis env isrec kind i = str (if isrec then "Induction" else "Case analysis") ++ strbrk " on sort " ++ pr_sort Evd.empty kind ++ strbrk " is not allowed for inductive definition " ++ - pr_inductive (Global.env()) (fst i) ++ str "." + pr_inductive env (fst i) ++ str "." -let error_not_allowed_dependent_analysis isrec i = +let error_not_allowed_dependent_analysis env isrec i = str "Dependent " ++ str (if isrec then "induction" else "case analysis") ++ strbrk " is not allowed for inductive definition " ++ - pr_inductive (Global.env()) i ++ str "." + pr_inductive env i ++ str "." -let error_not_mutual_in_scheme ind ind' = +let error_not_mutual_in_scheme env ind ind' = if eq_ind ind ind' then - str "The inductive type " ++ pr_inductive (Global.env()) ind ++ + str "The inductive type " ++ pr_inductive env ind ++ str " occurs twice." else - str "The inductive types " ++ pr_inductive (Global.env()) ind ++ spc () ++ - str "and" ++ spc () ++ pr_inductive (Global.env()) ind' ++ spc () ++ + str "The inductive types " ++ pr_inductive env ind ++ spc () ++ + str "and" ++ spc () ++ pr_inductive env ind' ++ spc () ++ str "are not mutually defined." (* Inductive constructions errors *) @@ -1194,12 +1194,12 @@ let explain_inductive_error = function (* Recursion schemes errors *) -let explain_recursion_scheme_error = function +let explain_recursion_scheme_error env = function | NotAllowedCaseAnalysis (isrec,k,i) -> - error_not_allowed_case_analysis isrec k i - | NotMutualInScheme (ind,ind')-> error_not_mutual_in_scheme ind ind' + error_not_allowed_case_analysis env isrec k i + | NotMutualInScheme (ind,ind')-> error_not_mutual_in_scheme env ind ind' | NotAllowedDependentAnalysis (isrec, i) -> - error_not_allowed_dependent_analysis isrec i + error_not_allowed_dependent_analysis env isrec i (* Pattern-matching errors *) diff --git a/vernac/himsg.mli b/vernac/himsg.mli index 02b3c45501..db05aaa125 100644 --- a/vernac/himsg.mli +++ b/vernac/himsg.mli @@ -29,7 +29,7 @@ val explain_mismatched_contexts : env -> contexts -> Constrexpr.constr_expr list val explain_typeclass_error : env -> typeclass_error -> Pp.t -val explain_recursion_scheme_error : recursion_scheme_error -> Pp.t +val explain_recursion_scheme_error : env -> recursion_scheme_error -> Pp.t val explain_refiner_error : env -> Evd.evar_map -> refiner_error -> Pp.t diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 0a74a8cc4a..b354ad0521 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -82,7 +82,7 @@ let _ = let is_eq_flag () = !eq_flag -let eq_dec_flag = ref false +let eq_dec_flag = ref false let _ = declare_bool_option { optdepr = false; @@ -330,11 +330,10 @@ let declare_sym_scheme ind = (* Scheme command *) let smart_global_inductive y = smart_global_inductive y -let rec split_scheme l = - let env = Global.env() in +let rec split_scheme env l = match l with | [] -> [],[] - | (Some id,t)::q -> let l1,l2 = split_scheme q in + | (Some id,t)::q -> let l1,l2 = split_scheme env q in ( match t with | InductionScheme (x,y,z) -> ((id,x,smart_global_inductive y,z)::l1),l2 | CaseScheme (x,y,z) -> ((id,x,smart_global_inductive y,z)::l1),l2 @@ -345,7 +344,7 @@ let rec split_scheme l = requested *) | (None,t)::q -> - let l1,l2 = split_scheme q in + let l1,l2 = split_scheme env q in let names inds recs isdep y z = let ind = smart_global_inductive y in let sort_of_ind = inductive_sort_family (snd (lookup_mind_specif env ind)) in @@ -384,7 +383,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort = and env0 = Global.env() in let sigma, lrecspec, _ = List.fold_right - (fun (_,dep,ind,sort) (evd, l, inst) -> + (fun (_,dep,ind,sort) (evd, l, inst) -> let evd, indu, inst = match inst with | None -> @@ -408,12 +407,12 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort = let _ = List.fold_right2 declare listdecl lrecnames [] in fixpoint_message None lrecnames -let get_common_underlying_mutual_inductive = function +let get_common_underlying_mutual_inductive env = function | [] -> assert false | (id,(mind,i as ind))::l as all -> match List.filter (fun (_,(mind',_)) -> not (MutInd.equal mind mind')) l with | (_,ind')::_ -> - raise (RecursionSchemeError (NotMutualInScheme (ind,ind'))) + raise (RecursionSchemeError (env, NotMutualInScheme (ind,ind'))) | [] -> if not (List.distinct_f Int.compare (List.map snd (List.map snd all))) then user_err Pp.(str "A type occurs twice"); @@ -422,7 +421,8 @@ let get_common_underlying_mutual_inductive = function (function (Some id,(_,i)) -> Some (i,id.CAst.v) | (None,_) -> None) all let do_scheme l = - let ischeme,escheme = split_scheme l in + let env = Global.env() in + let ischeme,escheme = split_scheme env l in (* we want 1 kind of scheme at a time so we check if the user tried to declare different schemes at once *) if not (List.is_empty ischeme) && not (List.is_empty escheme) @@ -431,7 +431,7 @@ tried to declare different schemes at once *) else ( if not (List.is_empty ischeme) then do_mutual_induction_scheme ischeme else - let mind,l = get_common_underlying_mutual_inductive escheme in + let mind,l = get_common_underlying_mutual_inductive env escheme in declare_beq_scheme_with l mind; declare_eq_decidability_scheme_with l mind ) @@ -454,6 +454,9 @@ let fold_left' f = function let mk_coq_and sigma = Evarutil.new_global sigma (Coqlib.build_coq_and ()) let mk_coq_conj sigma = Evarutil.new_global sigma (Coqlib.build_coq_conj ()) +let mk_coq_prod sigma = Evarutil.new_global sigma (Coqlib.build_coq_prod ()) +let mk_coq_pair sigma = Evarutil.new_global sigma (Coqlib.build_coq_pair ()) + let build_combined_scheme env schemes = let evdref = ref (Evd.from_env env) in let defs = List.map (fun cst -> @@ -471,10 +474,25 @@ let build_combined_scheme env schemes = in let (c, t) = List.hd defs in let ctx, ind, nargs = find_inductive t in + (* We check if ALL the predicates are in Prop, if so we use propositional + conjunction '/\', otherwise we use the simple product '*'. + *) + let inprop = + let inprop (_,t) = + Retyping.get_sort_family_of env !evdref (EConstr.of_constr t) + == Sorts.InProp + in + List.for_all inprop defs + in + let mk_and, mk_conj = + if inprop + then (mk_coq_and, mk_coq_conj) + else (mk_coq_prod, mk_coq_pair) + in (* Number of clauses, including the predicates quantification *) let prods = nb_prod !evdref (EConstr.of_constr t) - (nargs + 1) in - let sigma, coqand = mk_coq_and !evdref in - let sigma, coqconj = mk_coq_conj sigma in + let sigma, coqand = mk_and !evdref in + let sigma, coqconj = mk_conj sigma in let () = evdref := sigma in let relargs = rel_vect 0 prods in let concls = List.rev_map @@ -492,7 +510,8 @@ let build_combined_scheme env schemes = (List.rev_map (fun (x, y) -> LocalAssum (x, y)) ctx) in let typ = List.fold_left (fun d c -> Term.mkProd_wo_LetIn c d) concl_typ ctx in let body = it_mkLambda_or_LetIn concl_bod ctx in - (!evdref, body, typ) + let sigma = Typing.check env !evdref (EConstr.of_constr body) (EConstr.of_constr typ) in + (sigma, body, typ) let do_combined_scheme name schemes = let open CAst in |