diff options
| -rw-r--r-- | library/states.ml | 7 | ||||
| -rw-r--r-- | library/states.mli | 5 | ||||
| -rw-r--r-- | plugins/subtac/subtac_command.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 23 | ||||
| -rw-r--r-- | theories/Classes/SetoidAxioms.v | 2 | ||||
| -rw-r--r-- | toplevel/command.ml | 4 | ||||
| -rw-r--r-- | toplevel/record.ml | 2 |
7 files changed, 29 insertions, 16 deletions
diff --git a/library/states.ml b/library/states.ml index c985dcf2c..4fbc4c886 100644 --- a/library/states.ml +++ b/library/states.ml @@ -35,3 +35,10 @@ let with_heavy_rollback f x = f x with reraise -> (unfreeze st; raise reraise) + +let with_state_protection f x = + let st = freeze () in + try + let a = f x in unfreeze st; a + with reraise -> + (unfreeze st; raise reraise) diff --git a/library/states.mli b/library/states.mli index 3deb05658..17f62b512 100644 --- a/library/states.mli +++ b/library/states.mli @@ -26,4 +26,9 @@ val unfreeze : state -> unit val with_heavy_rollback : ('a -> 'b) -> 'a -> 'b +(*s [with_state_protection f x] applies [f] to [x] and restores the + state of the whole system as it was before the evaluation of f *) + +val with_state_protection : ('a -> 'b) -> 'a -> 'b + diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml index 6ffb36e41..ec3da0f8c 100644 --- a/plugins/subtac/subtac_command.ml +++ b/plugins/subtac/subtac_command.ml @@ -410,7 +410,7 @@ let interp_recursive fixkind l boxed = (* Interp bodies with rollback because temp use of notations/implicit *) let fixdefs = - States.with_heavy_rollback (fun () -> + States.with_state_protection (fun () -> List.iter (Command.declare_interning_data impls) notations; list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls) () in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9940f04b5..6aadd9124 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1170,9 +1170,6 @@ let forward_general_multi_rewrite = let register_general_multi_rewrite f = forward_general_multi_rewrite := f -let clear_last = onLastHyp (fun c -> (clear [destVar c])) -let case_last = onLastHyp simplest_case - let error_unexpected_extra_pattern loc nb pat = let s1,s2,s3 = match pat with | IntroIdentifier _ -> "name", (plural nb " introduction pattern"), "no" @@ -1183,8 +1180,8 @@ let error_unexpected_extra_pattern loc nb pat = str (if nb = 1 then "was" else "were") ++ strbrk " expected in the branch).") -let intro_or_and_pattern loc b ll l' tac = - onLastHyp (fun c gl -> +let intro_or_and_pattern loc b ll l' tac id gl = + let c = mkVar id in let ind,_ = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in let nv = mis_constr_nargs ind in let bracketed = b or not (l'=[]) in @@ -1198,10 +1195,10 @@ let intro_or_and_pattern loc b ll l' tac = let ll = fix_empty_or_and_pattern (Array.length nv) ll in check_or_and_pattern_size loc ll (Array.length nv); tclTHENLASTn - (tclTHEN case_last clear_last) + (tclTHEN (simplest_case c) (clear [id])) (array_map2 (fun n l -> tac ((adjust_names_length n n l)@l')) nv (Array.of_list ll)) - gl) + gl let rewrite_hyp l2r id gl = let rew_on l2r = @@ -1266,8 +1263,9 @@ let rec intros_patterns b avoid thin destopt = function | (loc, IntroOrAndPattern ll) :: l' -> tclTHEN introf - (intro_or_and_pattern loc b ll l' - (intros_patterns b avoid thin destopt)) + (onLastHypId + (intro_or_and_pattern loc b ll l' + (intros_patterns b avoid thin destopt))) | (loc, IntroRewrite l2r) :: l -> tclTHEN (intro_gen loc (IntroAvoid(avoid@explicit_intro_names l)) no_move true) @@ -1301,8 +1299,10 @@ let prepare_intros s ipat gl = match ipat with | IntroRewrite l2r -> let id = make_id s gl in id, !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) allHypsAndConcl - | IntroOrAndPattern ll -> make_id s gl, - intro_or_and_pattern loc true ll [] (intros_patterns true [] [] no_move) + | IntroOrAndPattern ll -> make_id s gl, + onLastHypId + (intro_or_and_pattern loc true ll [] + (intros_patterns true [] [] no_move)) let ipat_of_name = function | Anonymous -> None @@ -1333,6 +1333,7 @@ let as_tac id ipat = match ipat with !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) allHypsAndConcl | Some (loc,IntroOrAndPattern ll) -> intro_or_and_pattern loc true ll [] (intros_patterns true [] [] no_move) + id | Some (loc, (IntroIdentifier _ | IntroAnonymous | IntroFresh _ | IntroWildcard)) -> user_err_loc (loc,"", str "Disjunctive/conjunctive pattern expected") diff --git a/theories/Classes/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v index 944173893..469b9eae6 100644 --- a/theories/Classes/SetoidAxioms.v +++ b/theories/Classes/SetoidAxioms.v @@ -22,7 +22,7 @@ Unset Strict Implicit. Require Export Coq.Classes.SetoidClass. (* Application of the extensionality axiom to turn a goal on - Leibinz equality to a setoid equivalence (use with care!). *) + Leibniz equality to a setoid equivalence (use with care!). *) Axiom setoideq_eq : forall `{sa : Setoid a} (x y : a), x == y -> x = y. diff --git a/toplevel/command.ml b/toplevel/command.ml index cb772714d..ed21213ef 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -541,7 +541,7 @@ let interp_mutual paramsl indl notations finite = let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in let constructors = - States.with_heavy_rollback (fun () -> + States.with_state_protection (fun () -> (* Temporary declaration of notations and scopes *) List.iter (declare_interning_data impls) notations; (* Interpret the constructor types *) @@ -849,7 +849,7 @@ let interp_recursive fixkind l boxed = (* Interp bodies with rollback because temp use of notations/implicit *) let fixdefs = - States.with_heavy_rollback (fun () -> + States.with_state_protection (fun () -> List.iter (declare_interning_data impls) notations; list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls) () in diff --git a/toplevel/record.ml b/toplevel/record.ml index d22735f1d..b1a56d577 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -392,7 +392,7 @@ let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuil (* Now, younger decl in params and fields is on top *) let sc = interp_and_check_sort s in let implpars, params, implfs, fields = - States.with_heavy_rollback (fun () -> + States.with_state_protection (fun () -> typecheck_params_and_fields idstruc sc ps notations fs) () in let sign = structure_signature (fields@params) in match kind with |