diff options
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 90376a431..ea606210b 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -64,7 +64,7 @@ let red_constant_entry n ce = function { ce with const_entry_body = under_binders (Global.env()) (fst (reduction_of_red_expr red)) n body } -let interp_definition bl red_option c ctypopt = +let interp_definition bl p red_option c ctypopt = let env = Global.env() in let evdref = ref Evd.empty in let impls, ((env_bl, ctx), imps1) = interp_context_evars evdref env bl in @@ -78,6 +78,7 @@ let interp_definition bl red_option c ctypopt = imps1@(Impargs.lift_implicits nb_args imps2), { const_entry_body = body; const_entry_type = None; + const_entry_polymorphic = p; const_entry_opaque = false } | Some ctyp -> let ty, impsty = interp_type_evars_impls ~impls ~evdref ~fail_evar:false env_bl ctyp in @@ -89,6 +90,7 @@ let interp_definition bl red_option c ctypopt = imps1@(Impargs.lift_implicits nb_args imps2), { const_entry_body = body; const_entry_type = Some typ; + const_entry_polymorphic = p; const_entry_opaque = false } in red_constant_entry (rel_context_length ctx) ce red_option, imps @@ -126,7 +128,7 @@ let declare_definition ident (local,k) ce imps hook = (* 2| Variable/Hypothesis/Parameter/Axiom declarations *) -let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) = +let declare_assumption is_coe (local,p,kind) c imps impl nl (_,ident) = let r = match local with | Local when Lib.sections_are_opened () -> let _ = @@ -472,6 +474,7 @@ let declare_fix kind f def t imps = let ce = { const_entry_body = def; const_entry_type = Some t; + const_entry_polymorphic = false; const_entry_opaque = false } in let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in @@ -551,7 +554,7 @@ let declare_fixpoint ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns = let init_tac = Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC) fixdefs) in - Lemmas.start_proof_with_initialization (Global,DefinitionBody Fixpoint) + Lemmas.start_proof_with_initialization (Global,false,DefinitionBody Fixpoint) (Some(false,indexes,init_tac)) thms None (fun _ _ -> ()) else begin (* We shortcut the proof process *) @@ -576,7 +579,7 @@ let declare_cofixpoint ((fixnames,fixdefs,fixtypes),fiximps) ntns = let init_tac = Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC) fixdefs) in - Lemmas.start_proof_with_initialization (Global,DefinitionBody CoFixpoint) + Lemmas.start_proof_with_initialization (Global,false,DefinitionBody CoFixpoint) (Some(true,[],init_tac)) thms None (fun _ _ -> ()) else begin (* We shortcut the proof process *) |