From 8a35d93061c67dcdbb12337b78fcb35d72957f51 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 2 Apr 2017 19:13:33 +0200 Subject: Minor cosmetic commit. --- vernac/command.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/command.ml') diff --git a/vernac/command.ml b/vernac/command.ml index 6eb7037f84..f31fce8859 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -1155,7 +1155,7 @@ let interp_fixpoint l ntns = let interp_cofixpoint l ntns = let (env,_,pl,evd),fix,info = interp_recursive false l ntns in - check_recursive false env evd fix; + check_recursive false env evd fix; (fix,pl,Evd.evar_universe_context evd,info) let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns = -- cgit v1.2.3 From 21d308fc083ee395e7b1ff78e75ec3a1305cb2f4 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 2 Apr 2017 19:12:44 +0200 Subject: Fixing several wrong computations of implicit arguments by position in the presence of let-ins. --- vernac/command.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'vernac/command.ml') diff --git a/vernac/command.ml b/vernac/command.ml index f31fce8859..c24dbdf7c0 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -95,7 +95,7 @@ let interp_definition pl bl p red_option c ctypopt = let ctx = Evd.make_evar_universe_context env pl in let evdref = ref (Evd.from_ctx ctx) in let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in - let nb_args = List.length ctx in + let nb_args = Context.Rel.nhyps ctx in let imps,pl,ce = match ctypopt with None -> @@ -838,7 +838,7 @@ type structured_fixpoint_expr = { let interp_fix_context env evdref isfix fix = let before, after = if isfix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in let impl_env, ((env', ctx), imps) = interp_context_evars env evdref before in - let impl_env', ((env'', ctx'), imps') = interp_context_evars ~impl_env ~shift:(List.length before) env' evdref after in + let impl_env', ((env'', ctx'), imps') = interp_context_evars ~impl_env ~shift:(Context.Rel.nhyps ctx) env' evdref after in let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot) @@ -1100,7 +1100,7 @@ let interp_recursive isfix fixl notations = let fixtypes = List.map2 build_fix_type fixctxs fixccls in let fixtypes = List.map (nf_evar !evdref) fixtypes in let fiximps = List.map3 - (fun ctximps cclimps (_,ctx) -> ctximps@(Impargs.lift_implicits (List.length ctx) cclimps)) + (fun ctximps cclimps (_,ctx) -> ctximps@(Impargs.lift_implicits (Context.Rel.nhyps ctx) cclimps)) fixctximps fixcclimps fixctxs in let rec_sign = List.fold_left2 -- cgit v1.2.3 From 2ddc9d12bd4616f10245c40bc0c87ae548911809 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 2 Apr 2017 19:13:58 +0200 Subject: Fixing #5420 as well as many related bugs due to miscounting let-ins. - Supporting let-ins in tactic "fix", and hence in interactive Fixpoint and mutual theorems. - Documenting more precisely the meaning of n in tactic "fix id n". - Fixing computation of recursive index at interpretation time in the presence of let-ins. --- vernac/command.ml | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) (limited to 'vernac/command.ml') diff --git a/vernac/command.ml b/vernac/command.ml index c24dbdf7c0..a6343a5f5d 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -867,8 +867,10 @@ let prepare_recursive_declaration fixnames fixtypes fixdefs = (* Jump over let-bindings. *) -let compute_possible_guardness_evidences (ids,_,na) = - match na with +let compute_possible_guardness_evidences (ctx,_,recindex) = + (* A recursive index is characterized by the number of lambdas to + skip before finding the relevant inductive argument *) + match recindex with | Some i -> [i] | None -> (* If recursive argument was not given by user, we try all args. @@ -876,7 +878,7 @@ let compute_possible_guardness_evidences (ids,_,na) = but doing it properly involves delta-reduction, and it finally doesn't seem to worth the effort (except for huge mutual fixpoints ?) *) - List.interval 0 (List.length ids - 1) + List.interval 0 (Context.Rel.nhyps ctx - 1) type recursive_preentry = Id.t list * constr option list * types list @@ -1136,10 +1138,10 @@ let interp_recursive isfix fixl notations = let evd, nf = nf_evars_and_universes evd in let fixdefs = List.map (Option.map nf) fixdefs in let fixtypes = List.map nf fixtypes in - let fixctxnames = List.map (fun (_,ctx) -> List.map RelDecl.get_name ctx) fixctxs in + let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in (* Build the fix declaration block *) - (env,rec_sign,all_universes,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxnames fiximps fixannots + (env,rec_sign,all_universes,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots let check_recursive isfix env evd (fixnames,fixdefs,_) = check_evars_are_solved env evd Evd.empty; @@ -1162,7 +1164,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind if List.exists Option.is_empty fixdefs then (* Some bodies to define by proof *) let thms = - List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps)))) + List.map3 (fun id t (ctx,imps,_) -> ((id,pl),(t,(List.map RelDecl.get_name ctx,imps)))) fixnames fixtypes fiximps in let init_tac = Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC) @@ -1199,7 +1201,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n if List.exists Option.is_empty fixdefs then (* Some bodies to define by proof *) let thms = - List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps)))) + List.map3 (fun id t (ctx,imps,_) -> ((id,pl),(t,(List.map RelDecl.get_name ctx,imps)))) fixnames fixtypes fiximps in let init_tac = Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC) -- cgit v1.2.3 From 7d26940665ccce2e4ee1ba6fc157e42f7a639861 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 12 Apr 2017 12:15:40 +0200 Subject: Removing tactic compatibility layer in Command. --- vernac/command.ml | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) (limited to 'vernac/command.ml') diff --git a/vernac/command.ml b/vernac/command.ml index 45ff579552..b27d8a0a35 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -1198,11 +1198,8 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps)))) fixnames fixtypes fiximps in let init_tac = - Some (List.map (Option.cata (EConstr.of_constr %> Tacmach.refine_no_check) Tacticals.tclIDTAC) + Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in - let init_tac = - Option.map (List.map Proofview.V82.tactic) init_tac - in let evd = Evd.from_ctx ctx in Lemmas.start_proof_with_initialization (Global,poly,DefinitionBody Fixpoint) evd (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) @@ -1235,11 +1232,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps)))) fixnames fixtypes fiximps in let init_tac = - Some (List.map (Option.cata (EConstr.of_constr %> Tacmach.refine_no_check) Tacticals.tclIDTAC) + Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in - let init_tac = - Option.map (List.map Proofview.V82.tactic) init_tac - in let evd = Evd.from_ctx ctx in Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint) evd (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) -- cgit v1.2.3 From 2826683746569b9d78aa01e319315ab554e1619b Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 19:36:45 +0200 Subject: Fix omitted labels in function calls --- vernac/command.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'vernac/command.ml') diff --git a/vernac/command.ml b/vernac/command.ml index b27d8a0a35..b2f5755ce6 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -258,7 +258,7 @@ match local with let () = Universes.register_universe_binders gr pl in let () = assumption_message ident in let () = Typeclasses.declare_instance None false gr in - let () = if is_coe then Class.try_add_new_coercion gr local p in + let () = if is_coe then Class.try_add_new_coercion gr ~local p in let inst = if p (* polymorphic *) then Univ.UContext.instance ctx else Univ.Instance.empty @@ -752,7 +752,7 @@ let do_mutual_inductive indl poly prv finite = (* Declare the possible notations of inductive types *) List.iter Metasyntax.add_notation_interpretation ntns; (* Declare the coercions *) - List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false poly) coes; + List.iter (fun qid -> Class.try_add_new_coercion (locate qid) ~local:false poly) coes; (* If positivity is assumed declares itself as unsafe. *) if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else () -- cgit v1.2.3