From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- plugins/decl_mode/decl_interp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/decl_mode/decl_interp.ml') diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 1c56586cea..2a44dca219 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published. --- plugins/decl_mode/decl_interp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/decl_mode/decl_interp.ml') diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 2a44dca219..7cfca53c50 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -403,7 +403,7 @@ let interp_suffices_clause env sigma (hyps,cot)= match hyp with (Hprop st | Hvar st) -> match st.st_label with - Name id -> Environ.push_named (id,None,st.st_it) env0 + Name id -> Environ.push_named (Context.Named.Declaration.LocalAssum (id,st.st_it)) env0 | _ -> env in let nenv = List.fold_right push_one locvars env in nenv,res -- cgit v1.2.3 From f358d7b4c962f5288ad9ce2dc35802666c882422 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 22 Feb 2016 10:32:57 +0100 Subject: The tactic generic argument now returns a value rather than a glob_expr. The glob_expr was actually always embedded as a VFun, so this patch should not change anything semantically. The only change occurs in the plugin API where one should use the Tacinterp.tactic_of_value function instead of Tacinterp.eval_tactic. Moreover, this patch allows to use tactics returning arguments from the ML side. --- plugins/decl_mode/decl_interp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/decl_mode/decl_interp.ml') diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 7cfca53c50..4874552d6a 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -384,7 +384,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps = let interp_cut interp_it env sigma cut= let nenv,nstat = interp_it env sigma cut.cut_stat in - {cut with + { cut_using=Option.map (Tacinterp.Value.of_closure (Tacinterp.default_ist ())) cut.cut_using; cut_stat=nstat; cut_by=interp_justification_items nenv sigma cut.cut_by} -- cgit v1.2.3 From d868820ad1f00b896c5f44f18678fac2f8e0f720 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 13 Mar 2016 13:18:10 +0100 Subject: Supporting "(@foo) args" in patterns, where "@foo" has no arguments. --- plugins/decl_mode/decl_interp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/decl_mode/decl_interp.ml') diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 4874552d6a..34307a358f 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -96,7 +96,7 @@ let rec add_vars_of_simple_pattern globs = function add_vars_of_simple_pattern globs p | CPatCstr (_,_,pl1,pl2) -> List.fold_left add_vars_of_simple_pattern - (List.fold_left add_vars_of_simple_pattern globs pl1) pl2 + (Option.fold_left (List.fold_left add_vars_of_simple_pattern) globs pl1) pl2 | CPatNotation(_,_,(pl,pll),pl') -> List.fold_left add_vars_of_simple_pattern globs (List.flatten (pl::pl'::pll)) | CPatAtom (_,Some (Libnames.Ident (_,id))) -> add_var id globs -- cgit v1.2.3