aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/interface/name_to_ast.ml2
-rw-r--r--contrib/interface/xlate.ml5
-rw-r--r--contrib/subtac/subtac.ml12
-rw-r--r--contrib/subtac/subtac_obligations.ml2
-rw-r--r--ide/coq.ml2
-rw-r--r--kernel/cooking.ml2
-rw-r--r--kernel/cooking.mli3
-rw-r--r--kernel/declarations.ml6
-rw-r--r--kernel/declarations.mli3
-rw-r--r--kernel/entries.ml2
-rw-r--r--kernel/entries.mli2
-rw-r--r--kernel/modops.ml26
-rw-r--r--kernel/term_typing.ml11
-rw-r--r--kernel/term_typing.mli4
-rw-r--r--library/declare.ml2
-rw-r--r--parsing/g_vernac.ml411
-rw-r--r--parsing/ppvernac.ml2
-rw-r--r--tactics/setoid_replace.ml2
-rw-r--r--tactics/tactics.ml2
-rw-r--r--toplevel/command.ml10
-rw-r--r--toplevel/command.mli7
-rw-r--r--toplevel/vernacentries.ml6
-rw-r--r--toplevel/vernacexpr.ml2
23 files changed, 76 insertions, 50 deletions
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 9a503cfb5..bbde91aac 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -134,7 +134,7 @@ let implicits_to_ast_list implicits =
let make_variable_ast name typ implicits =
(VernacAssumption
- ((Local,Definitional),
+ ((Local,Definitional),false,(*inline flag*)
[false,([dummy_loc,name], constr_to_ast (body_of_type typ))]))
::(implicits_to_ast_list implicits);;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 6d52be45d..639b4ae74 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1848,8 +1848,9 @@ let rec xlate_vernac =
(xlate_defn kind, xlate_ident s, xlate_binder_list bl,
cvt_optional_eval_for_definition c red_option,
xlate_formula_opt typ_opt)
- | VernacAssumption (kind, b) ->
- CT_variable (xlate_var kind, cvt_vernac_binders b)
+ | VernacAssumption (kind,inline ,b) ->xlate_error "TODO: Parameter Inline"
+ (*inline : bool -> automatic delta reduction at fonctor application*)
+ (* CT_variable (xlate_var kind, cvt_vernac_binders b)*)
| VernacCheckMayEval (None, numopt, c) ->
CT_check (xlate_formula c)
| VernacSearch (s,x) ->
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index ff5df49e3..eb1d5baf7 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -78,18 +78,18 @@ let _ = Detyping.set_detype_anonymous (fun loc n -> RVar (loc, id_of_string ("An
let assumption_message id =
Options.if_verbose message ((string_of_id id) ^ " is assumed")
-let declare_assumption env isevars idl is_coe k bl c =
+let declare_assumption env isevars idl is_coe k bl c nl =
if not (Pfedit.refining ()) then
let evm, c, typ =
Subtac_pretyping.subtac_process env isevars (snd (List.hd idl)) [] (Command.generalize_constr_expr c bl) None
in
- List.iter (Command.declare_one_assumption is_coe k c) idl
+ List.iter (Command.declare_one_assumption is_coe k c nl) idl
else
errorlabstrm "Command.Assumption"
(str "Cannot declare an assumption while in proof editing mode.")
-let vernac_assumption env isevars kind l =
- List.iter (fun (is_coe,(idl,c)) -> declare_assumption env isevars idl is_coe kind [] c) l
+let vernac_assumption env isevars kind l nl =
+ List.iter (fun (is_coe,(idl,c)) -> declare_assumption env isevars idl is_coe kind [] c nl) l
let subtac (loc, command) =
@@ -123,8 +123,8 @@ let subtac (loc, command) =
start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook
- | VernacAssumption (stre,l) ->
- vernac_assumption env isevars stre l
+ | VernacAssumption (stre,nl,l) ->
+ vernac_assumption env isevars stre l nl
(*| VernacEndProof e ->
subtac_end_proof e*)
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index e2101a2d9..34758721f 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -405,7 +405,7 @@ let admit_obligations n =
match x.obl_body with
None ->
let x = subst_deps_obl obls x in
- let kn = Declare.declare_constant x.obl_name (ParameterEntry x.obl_type, IsAssumption Conjectural) in
+ let kn = Declare.declare_constant x.obl_name (ParameterEntry (x.obl_type,false), IsAssumption Conjectural) in
assumption_message x.obl_name;
{ x with obl_body = Some (mkConst kn) }
| Some _ -> x)
diff --git a/ide/coq.ml b/ide/coq.ml
index a7d8da813..16b2460ad 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -354,7 +354,7 @@ let compute_reset_info = function
| VernacDefineModule (_,(_,id), _, _, _)
| VernacDeclareModule (_,(_,id), _, _)
| VernacDeclareModuleType ((_,id), _, _)
- | VernacAssumption (_, (_,((_,id)::_,_))::_)
+ | VernacAssumption (_,_ ,(_,((_,id)::_,_))::_)
| VernacInductive (_, (((_,id),_,_,_),_) :: _) ->
Reset (id, ref true)
| VernacDefinition (_, (_,id), ProveBody _, _)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 7751e5bf6..e9200cd75 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -131,4 +131,4 @@ let cook_constant env r =
let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in
Typeops.make_polymorphic_if_arity env typ in
let boxed = Cemitcodes.is_boxed cb.const_body_code in
- (body, typ, cb.const_constraints, cb.const_opaque, boxed)
+ (body, typ, cb.const_constraints, cb.const_opaque, boxed,false)
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 0646b1c22..4afdaa55e 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -25,7 +25,8 @@ type recipe = {
val cook_constant :
env -> recipe ->
- constr_substituted option * constant_type * constraints * bool * bool
+ constr_substituted option * constant_type * constraints * bool * bool
+ * bool
(*s Utility functions used in module [Discharge]. *)
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index d0f2289dc..1be251a50 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -49,7 +49,8 @@ type constant_body = {
const_body_code : Cemitcodes.to_patch_substituted;
(* const_type_code : Cemitcodes.to_patch; *)
const_constraints : constraints;
- const_opaque : bool }
+ const_opaque : bool;
+ const_inline : bool}
(*s Inductive types (internal representation with redundant
information). *)
@@ -202,7 +203,8 @@ let subst_const_body sub cb = {
const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
(*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*)
const_constraints = cb.const_constraints;
- const_opaque = cb.const_opaque }
+ const_opaque = cb.const_opaque;
+ const_inline = cb.const_inline}
let subst_arity sub = function
| Monomorphic s ->
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 22cfd62a0..7f7f7dcc3 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -47,7 +47,8 @@ type constant_body = {
const_body_code : to_patch_substituted;
(*i const_type_code : to_patch;i*)
const_constraints : constraints;
- const_opaque : bool }
+ const_opaque : bool;
+ const_inline : bool}
val subst_const_body : substitution -> constant_body -> constant_body
diff --git a/kernel/entries.ml b/kernel/entries.ml
index fb134b1c7..17da967c2 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -62,7 +62,7 @@ type definition_entry = {
const_entry_opaque : bool;
const_entry_boxed : bool}
-type parameter_entry = types
+type parameter_entry = types*bool
type constant_entry =
| DefinitionEntry of definition_entry
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 61c0b8c3b..56ea852da 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -61,7 +61,7 @@ type definition_entry = {
const_entry_opaque : bool;
const_entry_boxed : bool }
-type parameter_entry = types
+type parameter_entry = types*bool (*inline flag*)
type constant_entry =
| DefinitionEntry of definition_entry
diff --git a/kernel/modops.ml b/kernel/modops.ml
index e9e1d67eb..96d19552a 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -235,13 +235,29 @@ and constants_of_modtype env mp modtype =
| MTBfunsig _ -> []
(* returns a resolver for kn that maps mbid to mp *)
-(* Nota: Some delta-expansions used to happen here.
- Browse SVN if you want to know more. *)
let resolver_of_environment mbid modtype mp env =
let constants = constants_of_modtype env (MPbound mbid) modtype in
- let resolve = List.map (fun (con,_) -> con,None) constants in
- Mod_subst.make_resolver resolve
-
+ let resolve =
+ List.map
+ (fun (con,expecteddef) ->
+ let con' = replace_mp_in_con (MPbound mbid) mp con in
+ let constr =
+ try
+ if expecteddef.Declarations.const_inline then
+ let constant = lookup_constant con' env in
+ if constant.Declarations.const_opaque then
+ None
+ else
+ option_map Declarations.force
+ constant.Declarations.const_body
+ else
+ None
+ with Not_found -> error_no_such_label (con_label con')
+ in
+ con,constr
+ ) constants
+ in
+ Mod_subst.make_resolver resolve
let strengthen_const env mp l cb =
match cb.const_opaque, cb.const_body with
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 8b0f45ac9..aedc44ac8 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -93,11 +93,11 @@ let infer_declaration env dcl =
let (j,cst) = infer env c.const_entry_body in
let (typ,cst) = constrain_type env j cst c.const_entry_type in
Some (Declarations.from_val j.uj_val), typ, cst,
- c.const_entry_opaque, c.const_entry_boxed
- | ParameterEntry t ->
+ c.const_entry_opaque, c.const_entry_boxed, false
+ | ParameterEntry (t,nl) ->
let (j,cst) = infer env t in
None, NonPolymorphicType (Typeops.assumption_of_judgment env j), cst,
- false, false
+ false, false, nl
let global_vars_set_constant_type env = function
| NonPolymorphicType t -> global_vars_set env t
@@ -107,7 +107,7 @@ let global_vars_set_constant_type env = function
(fun t c -> Idset.union (global_vars_set env t) c))
ctx ~init:Idset.empty
-let build_constant_declaration env kn (body,typ,cst,op,boxed) =
+let build_constant_declaration env kn (body,typ,cst,op,boxed,inline) =
let ids =
match body with
| None -> global_vars_set_constant_type env typ
@@ -124,7 +124,8 @@ let build_constant_declaration env kn (body,typ,cst,op,boxed) =
const_body_code = tps;
(* const_type_code = to_patch env typ;*)
const_constraints = cst;
- const_opaque = op }
+ const_opaque = op;
+ const_inline = inline}
(*s Global and local constant declaration. *)
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 83434e2ec..abff3e8b7 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -26,10 +26,10 @@ val translate_local_assum : env -> types ->
types * Univ.constraints
val infer_declaration : env -> constant_entry ->
- constr_substituted option * constant_type * constraints * bool * bool
+ constr_substituted option * constant_type * constraints * bool * bool * bool
val build_constant_declaration : env -> 'a ->
- constr_substituted option * constant_type * constraints * bool * bool ->
+ constr_substituted option * constant_type * constraints * bool * bool * bool ->
constant_body
val translate_constant : env -> constant -> constant_entry -> constant_body
diff --git a/library/declare.ml b/library/declare.ml
index f729f133d..6e9835487 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -177,7 +177,7 @@ let discharge_constant ((sp,kn),(cdt,dhyps,kind)) =
Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,kind)
(* Hack to reduce the size of .vo: we keep only what load/open needs *)
-let dummy_constant_entry = ConstantEntry (ParameterEntry mkProp)
+let dummy_constant_entry = ConstantEntry (ParameterEntry (mkProp,false))
let dummy_constant (ce,_,mk) = dummy_constant_entry,[],mk
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 34d799745..6d0e3ffc4 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -120,11 +120,11 @@ GEXTEND Gram
[ [ thm = thm_token; id = identref; bl = LIST0 binder_let; ":";
c = lconstr ->
VernacStartTheoremProof (thm, id, (bl, c), false, no_hook)
- | stre = assumption_token; bl = assum_list ->
- VernacAssumption (stre, bl)
- | stre = assumptions_token; bl = assum_list ->
+ | stre = assumption_token; nl = inline; bl = assum_list ->
+ VernacAssumption (stre, nl, bl)
+ | stre = assumptions_token; nl = inline; bl = assum_list ->
test_plurial_form bl;
- VernacAssumption (stre, bl)
+ VernacAssumption (stre, nl, bl)
| IDENT "Boxed";"Definition";id = identref; b = def_body ->
VernacDefinition ((Global,true,Definition), id, b, no_hook)
| IDENT "Unboxed";"Definition";id = identref; b = def_body ->
@@ -193,6 +193,9 @@ GEXTEND Gram
| IDENT "Axioms" -> (Global, Logical)
| IDENT "Parameters" -> (Global, Definitional) ] ]
;
+ inline:
+ [ ["Inline" -> true | -> false] ]
+ ;
finite_token:
[ [ "Inductive" -> true
| "CoInductive" -> false ] ]
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 7d4104db3..c2571ad0a 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -515,7 +515,7 @@ let rec pr_vernac = function
| Some tok -> str"Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id))
| VernacExactProof c ->
hov 2 (str"Proof" ++ pr_lconstrarg c)
- | VernacAssumption (stre,l) ->
+ | VernacAssumption (stre,_,l) ->
let n = List.length (List.flatten (List.map fst (List.map snd l))) in
hov 2
(pr_assumption_token (n > 1) stre ++ spc() ++
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 1273c65e4..269c40fec 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -908,7 +908,7 @@ let new_morphism m signature id hook =
begin
ignore
(Declare.declare_internal_constant id
- (ParameterEntry lem, IsAssumption Logical)) ;
+ (ParameterEntry (lem,false), IsAssumption Logical)) ;
let mor_name = morphism_theory_id_of_morphism_proof_id id in
let lemma_infos = Some (id,argsconstr,outputconstr) in
add_morphism lemma_infos mor_name
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c496ffe64..defb7b749 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2524,7 +2524,7 @@ let admit_as_an_axiom gls =
let concl = it_mkNamedProd_or_LetIn (pf_concl gls) sign in
if occur_existential concl then error "\"admit\" cannot handle existentials";
let axiom =
- let cd = Entries.ParameterEntry concl in
+ let cd = Entries.ParameterEntry (concl,false) in
let con = Declare.declare_internal_constant na (cd,IsAssumption Logical) in
constr_of_global (ConstRef con)
in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index f73fe5e9c..f0a9792fd 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -161,7 +161,7 @@ let syntax_definition ident c local onlyparse =
let assumption_message id =
if_verbose message ((string_of_id id) ^ " is assumed")
-let declare_one_assumption is_coe (local,kind) c (_,ident) =
+let declare_one_assumption is_coe (local,kind) c nl (_,ident) =
let r = match local with
| Local when Lib.sections_are_opened () ->
let _ =
@@ -174,7 +174,7 @@ let declare_one_assumption is_coe (local,kind) c (_,ident) =
VarRef ident
| (Global|Local) ->
let kn =
- declare_constant ident (ParameterEntry c, IsAssumption kind) in
+ declare_constant ident (ParameterEntry (c,nl), IsAssumption kind) in
assumption_message ident;
if local=Local & Options.is_verbose () then
msg_warning (pr_id ident ++ str" is declared as a parameter" ++
@@ -182,11 +182,11 @@ let declare_one_assumption is_coe (local,kind) c (_,ident) =
ConstRef kn in
if is_coe then Class.try_add_new_coercion r local
-let declare_assumption idl is_coe k bl c =
+let declare_assumption idl is_coe k bl c nl=
if not (Pfedit.refining ()) then
let c = generalize_constr_expr c bl in
let c = interp_type Evd.empty (Global.env()) c in
- List.iter (declare_one_assumption is_coe k c) idl
+ List.iter (declare_one_assumption is_coe k c nl) idl
else
errorlabstrm "Command.Assumption"
(str "Cannot declare an assumption while in proof editing mode.")
@@ -799,7 +799,7 @@ let admit () =
error "Only statements declared as conjecture can be admitted";
*)
let kn =
- declare_constant id (ParameterEntry typ, IsAssumption Conjectural) in
+ declare_constant id (ParameterEntry (typ,false), IsAssumption Conjectural) in
Pfedit.delete_current_proof ();
assumption_message id;
hook Global (ConstRef kn)
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 4fae32805..cf05f691b 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -36,11 +36,12 @@ val declare_definition : identifier -> definition_kind ->
val syntax_definition : identifier -> constr_expr -> bool -> bool -> unit
-val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types ->
- Names.variable located -> unit
+val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types -> bool
+ -> Names.variable located -> unit
val declare_assumption : identifier located list ->
- coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> unit
+ coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> bool
+ ->unit
val build_mutual : (inductive_expr * decl_notation) list -> bool -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 7dacbeaba..4c0fb5046 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -348,8 +348,8 @@ let vernac_exact_proof c =
errorlabstrm "Vernacentries.ExactProof"
(str "Command 'Proof ...' can only be used at the beginning of the proof")
-let vernac_assumption kind l =
- List.iter (fun (is_coe,(idl,c)) -> declare_assumption idl is_coe kind [] c) l
+let vernac_assumption kind l nl=
+ List.iter (fun (is_coe,(idl,c)) -> declare_assumption idl is_coe kind [] c nl) l
let vernac_inductive f indl = build_mutual indl f
@@ -1134,7 +1134,7 @@ let interp c = match c with
vernac_start_proof k (Some id) t top f
| VernacEndProof e -> vernac_end_proof e
| VernacExactProof c -> vernac_exact_proof c
- | VernacAssumption (stre,l) -> vernac_assumption stre l
+ | VernacAssumption (stre,nl,l) -> vernac_assumption stre l nl
| VernacInductive (finite,l) -> vernac_inductive finite l
| VernacFixpoint (l,b) -> vernac_fixpoint l b
| VernacCoFixpoint (l,b) -> vernac_cofixpoint l b
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index cd0fb899c..042ef1e85 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -194,7 +194,7 @@ type vernac_expr =
(local_binder list * constr_expr) * bool * declaration_hook
| VernacEndProof of proof_end
| VernacExactProof of constr_expr
- | VernacAssumption of assumption_kind * simple_binder with_coercion list
+ | VernacAssumption of assumption_kind * bool * simple_binder with_coercion list
| VernacInductive of inductive_flag * (inductive_expr * decl_notation) list
| VernacFixpoint of (fixpoint_expr * decl_notation) list * bool
| VernacCoFixpoint of (cofixpoint_expr * decl_notation) list * bool
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 21:29:22 +0000