diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 8 | ||||
| -rw-r--r-- | pretyping/cbv.ml | 2 | ||||
| -rw-r--r-- | pretyping/evarconv.mli | 2 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 6 | ||||
| -rw-r--r-- | pretyping/globEnv.mli | 2 | ||||
| -rw-r--r-- | pretyping/program.mli | 2 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 4 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 2 | ||||
| -rw-r--r-- | pretyping/unification.ml | 6 |
9 files changed, 17 insertions, 17 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index d7a6c4c832..fadf290d44 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -824,7 +824,7 @@ let push_alias_eqn sigma alias eqn = (**********************************************************************) (* Functions to deal with elimination predicate *) -(* Infering the predicate *) +(* Inferring the predicate *) (* The problem to solve is the following: @@ -1455,7 +1455,7 @@ let compile ~program_mode sigma pb = (* Building the sub-problem when all patterns are variables. Case - where [current] is an intially pushed term. *) + where [current] is an initially pushed term. *) and shift_problem ((current,t),_,na) sigma pb = let ty = type_of_tomatch t in let tomatch = lift_tomatch_stack 1 pb.tomatch in @@ -1542,7 +1542,7 @@ let compile ~program_mode sigma pb = mat = List.map drop_alias_eqn pb.mat } in compile sigma pb in - (* If the "match" was orginally over a variable, as in "match x with + (* If the "match" was originally over a variable, as in "match x with O => true | n => n end", we give preference to non-expansion in the default clause (i.e. "match x with O => true | n => n end" rather than "match x with O => true | S p => S p end"; @@ -2067,7 +2067,7 @@ let prepare_predicate ?loc ~program_mode typing_fun env sigma tomatchs arsign ty let p2 = prepare_predicate_from_arsign_tycon ~program_mode env sigma loc tomatchs arsign t in (* Third strategy: we take the type constraint as it is; of course we could *) - (* need something inbetween, abstracting some but not all of the dependencies *) + (* need something in between, abstracting some but not all of the dependencies *) (* the "inversion" strategy deals with that but unification may not be *) (* powerful enough so strategy 2 and 3 helps; moreover, inverting does not *) (* work (yet) when a constructor has a type not precise enough for the inversion *) diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 5ea9b79336..4aa55e4d0d 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -477,7 +477,7 @@ and cbv_stack_value info env = function cbv_stack_value info env (CONSTR(c, [||]), stack_app args stk) | Some v -> cbv_stack_value info env (v,stk) | None -> mkSTACK(PRIMITIVE(op,c,args), stk) - else (* partical application *) + else (* partial application *) (assert (stk = TOP); PRIMITIVE(op,c,appl)) diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index eae961714d..04f54a1ad4 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -34,7 +34,7 @@ exception UnableToUnify of evar_map * Pretype_errors.unification_error ([unify_delay]) and another that tries to solve such remaining constraints using heuristics ([unify]). *) -(** Theses functions allow to pass arbitrary flags to the unifier and can delay constraints. +(** These functions allow to pass arbitrary flags to the unifier and can delay constraints. In case the flags are not specified, they default to [default_flags_of TransparentState.full] currently. diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 4a941a68b1..0925215b1c 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -285,7 +285,7 @@ let noccur_evar env evd evk c = try occur_rec false (0,env) c; true with Occur -> false (***************************************) -(* Managing chains of local definitons *) +(* Managing chains of local definitions *) (***************************************) type alias = @@ -629,7 +629,7 @@ let solve_pattern_eqn env sigma l c = * If a variable and an alias of it are bound to the same instance, we skip * the alias (we just use eq_constr -- instead of conv --, since anyway, * only instances that are variables -- or evars -- are later considered; - * morever, we can bet that similar instances came at some time from + * moreover, we can bet that similar instances came at some time from * the very same substitution. The removal of aliased duplicates is * useful to ensure the uniqueness of a projection. *) @@ -1738,7 +1738,7 @@ let reconsider_unif_constraints unify flags evd = * Returns an optional list of evars that were instantiated, or None * if the problem couldn't be solved. *) -(* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *) +(* Rq: incomplete algorithm if pbty = CONV_X_LEQ ! *) let solve_simple_eqn unify flags ?(choose=false) ?(imitate_defs=true) env evd (pbty,(evk1,args1 as ev1),t2) = try diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli index cdd36bbba6..bfe3423b11 100644 --- a/pretyping/globEnv.mli +++ b/pretyping/globEnv.mli @@ -40,7 +40,7 @@ type t val make : hypnaming:naming_mode -> env -> evar_map -> ltac_var_map -> t -(** Export the underlying environement *) +(** Export the underlying environment *) val env : t -> env diff --git a/pretyping/program.mli b/pretyping/program.mli index a8f5115788..2614e181d6 100644 --- a/pretyping/program.mli +++ b/pretyping/program.mli @@ -11,7 +11,7 @@ open Names open EConstr -(** A bunch of Coq constants used by Progam *) +(** A bunch of Coq constants used by Program *) val sig_typ : unit -> GlobRef.t val sig_intro : unit -> GlobRef.t diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 85e6f51387..2fc9dc2776 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -886,7 +886,7 @@ module CredNative = RedNative(CNativeEntries) (** Generic reduction function with environment Here is where unfolded constant are stored in order to be - eventualy refolded. + eventually refolded. If tactic_mode is true, it uses ReductionBehaviour, prefers refold constant instead of value and tries to infer constants @@ -1315,7 +1315,7 @@ let whd_allnolet_stack env = let whd_allnolet env = red_of_state_red (whd_allnolet_state env) -(* 4. Ad-hoc eta reduction, does not subsitute evars *) +(* 4. Ad-hoc eta reduction, does not substitute evars *) let shrink_eta c = Stack.zip Evd.empty (local_whd_state_gen eta Evd.empty (c,Stack.empty)) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index ee27aea93f..26801d285e 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -62,7 +62,7 @@ type typeclass = { (* Context of definitions and properties on defs, will not be shared *) cl_props : Constr.rel_context; - (* The method implementaions as projections. *) + (* The method implementations as projections. *) cl_projs : (Name.t * (direction * hint_info) option * Constant.t option) list; diff --git a/pretyping/unification.ml b/pretyping/unification.ml index d134c7319f..ad69cb2890 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1219,12 +1219,12 @@ let merge_instances env sigma flags st1 st2 c1 c2 = * bindings. This may or may not close off all RHSs of * the EVARs. For each EVAR whose RHS is closed off, * we can just apply it, and go on. For each which - * is not closed off, we need to do a mimick step - + * is not closed off, we need to do a mimic step - * in general, we have something like: * * ?X == (c e1 e2 ... ei[Meta(k)] ... en) * - * so we need to do a mimick step, converting ?X + * so we need to do a mimic step, converting ?X * into * * ?X -> (c ?z1 ... ?zn) @@ -1247,7 +1247,7 @@ let merge_instances env sigma flags st1 st2 c1 c2 = * we can reverse the equation, put it into our metavar * substitution, and keep going. * - * The most efficient mimick possible is, for each + * The most efficient mimic possible is, for each * Meta-var remaining in the term, to declare a * new EVAR of the same type. This is supposedly * determinable from the clausale form context - |