diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 15 | ||||
| -rw-r--r-- | vernac/obligations.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 27 |
3 files changed, 30 insertions, 14 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 0e51849058..2be10a0397 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -100,17 +100,18 @@ let pr_ljudge_env e s c = let v,t = pr_ljudge_env e s c in (quote v,quote t) (** A canonisation procedure for constr such that comparing there externalisation catches more equalities *) -let canonize_constr c = +let canonize_constr sigma c = (* replaces all the names in binders by [dn] ("default name"), ensures that [alpha]-equivalent terms will have the same externalisation. *) + let open EConstr in let dn = Name.Anonymous in let rec canonize_binders c = - match Term.kind_of_term c with + match EConstr.kind sigma c with | Prod (_,t,b) -> mkProd(dn,t,b) | Lambda (_,t,b) -> mkLambda(dn,t,b) | LetIn (_,u,t,b) -> mkLetIn(dn,u,t,b) - | _ -> Term.map_constr canonize_binders c + | _ -> EConstr.map sigma canonize_binders c in canonize_binders c @@ -118,8 +119,8 @@ let canonize_constr c = let display_eq ~flags env sigma t1 t2 = (* terms are canonized, then their externalisation is compared syntactically *) let open Constrextern in - let t1 = canonize_constr t1 in - let t2 = canonize_constr t2 in + let t1 = canonize_constr sigma t1 in + let t2 = canonize_constr sigma t2 in let ct1 = Flags.with_options flags (fun () -> extern_constr false env sigma t1) () in let ct2 = Flags.with_options flags (fun () -> extern_constr false env sigma t2) () in Constrexpr_ops.constr_expr_eq ct1 ct2 @@ -129,7 +130,7 @@ let display_eq ~flags env sigma t1 t2 = let rec pr_explicit_aux env sigma t1 t2 = function | [] -> (** no specified flags: default. *) - (quote (Printer.pr_lconstr_env env sigma t1), quote (Printer.pr_lconstr_env env sigma t2)) + (quote (Printer.pr_leconstr_env env sigma t1), quote (Printer.pr_leconstr_env env sigma t2)) | flags :: rem -> let equal = display_eq ~flags env sigma t1 t2 in if equal then @@ -153,7 +154,7 @@ let explicit_flags = [print_universes; print_implicits; print_coercions; print_no_symbol] (** and more! *) ] let pr_explicit env sigma t1 t2 = - pr_explicit_aux env sigma (EConstr.to_constr sigma t1) (EConstr.to_constr sigma t2) explicit_flags + pr_explicit_aux env sigma t1 t2 explicit_flags let pr_db env i = try diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 28aeaa725e..a4fe49020a 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -650,7 +650,7 @@ let declare_obligation prg obl body ty uctx = let constant = Declare.declare_constant obl.obl_name ~local:true (DefinitionEntry ce,IsProof Property) in - if not opaque then add_hint false prg constant; + if not opaque then add_hint (Locality.make_section_locality None) prg constant; definition_message obl.obl_name; true, { obl with obl_body = if poly then diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index adf24d23b1..4f63ed6f48 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -522,7 +522,21 @@ let vernac_assumption locality poly (local, kind) l nl = let status = do_assumptions kind nl l in if not status then Feedback.feedback Feedback.AddedAxiom +let should_treat_as_cumulative cum poly = + if poly then + match cum with + | GlobalCumulativity | LocalCumulativity -> true + | GlobalNonCumulativity | LocalNonCumulativity -> false + else + match cum with + | GlobalCumulativity | GlobalNonCumulativity -> false + | LocalCumulativity -> + user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.") + | LocalNonCumulativity -> + user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.") + let vernac_record cum k poly finite struc binders sort nameopt cfs = + let is_cumulative = should_treat_as_cumulative cum poly in let const = match nameopt with | None -> add_prefix "Build_" (snd (fst (snd struc))) | Some (_,id as lid) -> @@ -533,13 +547,14 @@ let vernac_record cum k poly finite struc binders sort nameopt cfs = match x with | Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj" | _ -> ()) cfs); - ignore(Record.definition_structure (k,cum,poly,finite,struc,binders,cfs,const,sort)) + ignore(Record.definition_structure (k,is_cumulative,poly,finite,struc,binders,cfs,const,sort)) (** When [poly] is true the type is declared polymorphic. When [lo] is true, then the type is declared private (as per the [Private] keyword). [finite] indicates whether the type is inductive, co-inductive or neither. *) let vernac_inductive cum poly lo finite indl = + let is_cumulative = should_treat_as_cumulative cum poly in if Dumpglob.dump () then List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) -> match cstrs with @@ -576,7 +591,7 @@ let vernac_inductive cum poly lo finite indl = | _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.") in let indl = List.map unpack indl in - do_mutual_inductive indl cum poly lo finite + do_mutual_inductive indl is_cumulative poly lo finite let vernac_fixpoint locality poly local l = let local = enforce_locality_exp locality local in @@ -1363,10 +1378,10 @@ let _ = let _ = declare_bool_option { optdepr = false; - optname = "inductive cumulativity"; - optkey = ["Inductive"; "Cumulativity"]; - optread = Flags.is_inductive_cumulativity; - optwrite = Flags.make_inductive_cumulativity } + optname = "Polymorphic inductive cumulativity"; + optkey = ["Polymorphic"; "Inductive"; "Cumulativity"]; + optread = Flags.is_polymorphic_inductive_cumulativity; + optwrite = Flags.make_polymorphic_inductive_cumulativity } let _ = declare_int_option |