diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 27 | ||||
| -rw-r--r-- | plugins/ltac/tacexpr.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacexpr.mli | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 4 | ||||
| -rw-r--r-- | plugins/ltac/tactic_matching.ml | 2 |
5 files changed, 19 insertions, 18 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 963b7189f9..164bd7e118 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -30,7 +30,6 @@ open Evd open Tactypes open Locus open Locusops -open Decl_kinds open Elimschemes open Environ open Termops @@ -207,7 +206,7 @@ end) = struct let mk_relation env evd a = app_poly env evd relation [| a |] - (** Build an infered signature from constraints on the arguments and expected output + (** Build an inferred signature from constraints on the arguments and expected output relation *) let build_signature evars env m (cstrs : (types * types option) option list) @@ -1791,15 +1790,15 @@ let rec strategy_of_ast = function let mkappc s l = CAst.make @@ CAppExpl ((None,qualid_of_ident (Id.of_string s),None),l) let declare_an_instance n s args = - (((CAst.make @@ Name n),None), Explicit, + (((CAst.make @@ Name n),None), CAst.make @@ CAppExpl ((None, qualid_of_string s,None), args)) let declare_instance a aeq n s = declare_an_instance n s [a;aeq] -let anew_instance ~pstate atts binders instance fields = +let anew_instance ~pstate atts binders (name,t) fields = let program_mode = atts.program in new_instance ~pstate ~program_mode atts.polymorphic - binders instance (Some (true, CAst.make @@ CRecord (fields))) + name binders t (Some (true, CAst.make @@ CRecord (fields))) ~global:atts.global ~generalize:false Hints.empty_hint_info let declare_instance_refl ~pstate atts binders a aeq n lemma = @@ -2014,16 +2013,18 @@ let add_morphism_infer ~pstate atts m n : Proof_global.t option = let add_morphism ~pstate atts binders m s n = init_setoid (); let instance_id = add_suffix n "_Proper" in - let instance = - (((CAst.make @@ Name instance_id),None), Explicit, - CAst.make @@ CAppExpl ( - (None, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper",None), - [cHole; s; m])) + let instance_name = (CAst.make @@ Name instance_id),None in + let instance_t = + CAst.make @@ CAppExpl + ((None, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper",None), + [cHole; s; m]) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in - let _, pstate = new_instance ~pstate ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance - None - ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info in + let _, pstate = new_instance ~pstate + ~program_mode:atts.program ~global:atts.global atts.polymorphic + instance_name binders instance_t None + ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info + in pstate (** Bind to "rewrite" too *) diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 0eb7726a18..8bd69dd4fd 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -24,7 +24,7 @@ type direction_flag = bool (* true = Left-to-right false = right-to-right *) type lazy_flag = | General (* returns all possible successes *) | Select (* returns all successes of the first matching branch *) - | Once (* returns the first success in a maching branch + | Once (* returns the first success in a matching branch (not necessarily the first) *) type global_flag = (* [gfail] or [fail] *) | TacGlobal diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index fd303f5d94..f839c3e886 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -24,7 +24,7 @@ type direction_flag = bool (* true = Left-to-right false = right-to-right *) type lazy_flag = | General (* returns all possible successes *) | Select (* returns all successes of the first matching branch *) - | Once (* returns the first success in a maching branch + | Once (* returns the first success in a matching branch (not necessarily the first) *) type global_flag = (* [gfail] or [fail] *) | TacGlobal diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 800be2565d..4a0b01bcdc 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -855,7 +855,7 @@ let interp_binding_name ist env sigma = function | NamedHyp id -> (* If a name is bound, it has to be a quantified hypothesis *) (* user has to use other names for variables if these ones clash with *) - (* a name intented to be used as a (non-variable) identifier *) + (* a name intended to be used as a (non-variable) identifier *) try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist (Some (env,sigma)) (make id) with Not_found -> NamedHyp id @@ -2075,7 +2075,7 @@ let _ = let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in let ist = { lfun; poly; extra; } in let tac = interp_tactic ist tac in - (* EJGA: We sould also pass the proof name if desired, for now + (* EJGA: We should also pass the proof name if desired, for now poly seems like enough to get reasonable behavior in practice *) let name, poly = Id.of_string "ltac_gen", poly in diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index 2b5e496168..7783661787 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -128,7 +128,7 @@ module PatternMatching (E:StaticEnvironment) = struct (** To focus on the algorithmic portion of pattern-matching, the bookkeeping is relegated to a monad: the composition of the - bactracking monad of {!IStream.t} with a "writer" effect. *) + backtracking monad of {!IStream.t} with a "writer" effect. *) (* spiwack: as we don't benefit from the various stream optimisations of Haskell, it may be costly to give the monad in direct style such as here. We may want to use some continuation passing style. *) |