diff options
Diffstat (limited to 'vernac/comFixpoint.ml')
| -rw-r--r-- | vernac/comFixpoint.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index a428c42e49..006ac314a5 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -255,7 +255,7 @@ let interp_fixpoint ~cofix l ntns = let uctx,fix = ground_fixpoint env evd fix in (fix,pl,uctx,info) -let declare_fixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns = +let declare_fixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns = let pstate = if List.exists Option.is_empty fixdefs then (* Some bodies to define by proof *) @@ -267,7 +267,7 @@ let declare_fixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx fixdefs) in let evd = Evd.from_ctx ctx in Some - (Lemmas.start_proof_with_initialization ~ontop (local,poly,DefinitionBody Fixpoint) + (Lemmas.start_proof_with_initialization (local,poly,DefinitionBody Fixpoint) evd pl (Some(false,indexes,init_tac)) thms None) else begin (* We shortcut the proof process *) @@ -294,7 +294,7 @@ let declare_fixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; pstate -let declare_cofixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns = +let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns = let pstate = if List.exists Option.is_empty fixdefs then (* Some bodies to define by proof *) @@ -305,7 +305,7 @@ let declare_cofixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,c Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in let evd = Evd.from_ctx ctx in - Some (Lemmas.start_proof_with_initialization ~ontop (Global,poly, DefinitionBody CoFixpoint) + Some (Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint) evd pl (Some(true,[],init_tac)) thms None) else begin (* We shortcut the proof process *) @@ -366,18 +366,18 @@ let check_safe () = let flags = Environ.typing_flags (Global.env ()) in flags.check_universes && flags.check_guarded -let do_fixpoint ~ontop local poly l = +let do_fixpoint local poly l = let fixl, ntns = extract_fixpoint_components ~structonly:true l in let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl ntns in let possible_indexes = List.map compute_possible_guardness_evidences info in - let pstate = declare_fixpoint ~ontop local poly fix possible_indexes ntns in + let pstate = declare_fixpoint local poly fix possible_indexes ntns in if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else (); pstate -let do_cofixpoint ~ontop local poly l = +let do_cofixpoint local poly l = let fixl,ntns = extract_cofixpoint_components l in let cofix = interp_fixpoint ~cofix:true fixl ntns in - let pstate = declare_cofixpoint ~ontop local poly cofix ntns in + let pstate = declare_cofixpoint local poly cofix ntns in if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else (); pstate |