diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 2 | ||||
| -rw-r--r-- | interp/constrintern.ml | 20 | ||||
| -rw-r--r-- | interp/declare.ml | 8 | ||||
| -rw-r--r-- | interp/declare.mli | 2 | ||||
| -rw-r--r-- | interp/impargs.ml | 4 | ||||
| -rw-r--r-- | interp/impargs.mli | 6 | ||||
| -rw-r--r-- | interp/syntax_def.ml | 2 |
7 files changed, 21 insertions, 23 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index bb66658a37..fe50bd4b08 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -107,7 +107,7 @@ let _show_inactive_notations () = let deactivate_notation nr = match nr with | SynDefRule kn -> - (* shouldn't we check wether it is well defined? *) + (* shouldn't we check whether it is well defined? *) inactive_notations_table := IRuleSet.add nr !inactive_notations_table | NotationRule (scopt, ntn) -> match availability_of_notation (scopt, ntn) (scopt, []) with diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 753065b7dd..1dd68f2abf 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1229,7 +1229,7 @@ let add_local_defs_and_check_length loc env g pl args = match g with let maxargs = Inductiveops.constructor_nalldecls env cstr in if List.length pl' + List.length args > maxargs then error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs env cstr); - (* Two possibilities: either the args are given with explict + (* Two possibilities: either the args are given with explicit variables for local definitions, then we give the explicit args extended with local defs, so that there is nothing more to be added later on; or the args are not enough to have all arguments, @@ -1467,7 +1467,7 @@ let alias_of als = match als.alias_ids with @returns a raw_case_pattern_expr : - no notations and syntactic definition - - global reference and identifeir instead of reference + - global reference and identifier instead of reference *) @@ -1642,15 +1642,13 @@ let drop_notations_pattern looked_for genv = | CPatCast (_,_) -> (* We raise an error if the pattern contains a cast, due to current restrictions on casts in patterns. Cast in patterns - are supportted only in local binders and only at top - level. In fact, they are currently eliminated by the - parser. The only reason why they are in the - [cases_pattern_expr] type is that the parser needs to factor - the "(c : t)" notation with user defined notations (such as - the pair). In the long term, we will try to support such - casts everywhere, and use them to print the domains of - lambdas in the encoding of match in constr. This check is - here and not in the parser because it would require + are supported only in local binders and only at top level. + The only reason they are in the [cases_pattern_expr] type + is that the parser needs to factor the "c : t" notation + with user defined notations. In the long term, we will try to + support such casts everywhere, and perhaps use them to print + the domains of lambdas in the encoding of match in constr. + This check is here and not in the parser because it would require duplicating the levels of the [pattern] rule. *) CErrors.user_err ?loc ~hdr:"drop_notations_pattern" (Pp.strbrk "Casts are not supported in this pattern.") diff --git a/interp/declare.ml b/interp/declare.ml index 7ee7ecb5e8..b3595b2dae 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -163,7 +163,8 @@ let define_constant ?role ?(export_seff=false) id cd = not de.const_entry_opaque || is_poly de -> (* This globally defines the side-effects in the environment. *) - let de, export = Global.export_private_constants ~in_section de in + let body, export = Global.export_private_constants ~in_section (Future.force de.const_entry_body) in + let de = { de with const_entry_body = Future.from_val (body, ()) } in export, ConstantEntry (PureEntry, DefinitionEntry de) | _ -> [], ConstantEntry (EffectEntry, cd) in @@ -214,11 +215,10 @@ let cache_variable ((sp,_),o) = let impl = if impl then Implicit else Explicit in impl, true, poly, ctx | SectionLocalDef (de) -> - let (de, eff) = Global.export_private_constants ~in_section:true de in - let () = List.iter register_side_effect eff in (* The body should already have been forced upstream because it is a section-local definition, but it's not enforced by typing *) - let (body, uctx), () = Future.force de.const_entry_body in + let ((body, uctx), eff) = Global.export_private_constants ~in_section:true (Future.force de.const_entry_body) in + let () = List.iter register_side_effect eff in let poly, univs = match de.const_entry_universes with | Monomorphic_entry uctx -> false, uctx | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx diff --git a/interp/declare.mli b/interp/declare.mli index 2ffde31fc0..795d9a767d 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -40,7 +40,7 @@ type internal_flag = | InternalTacticRequest | UserIndividualRequest -(* Defaut definition entries, transparent with no secctx or proj information *) +(* Default definition entries, transparent with no secctx or proj information *) val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:types -> ?univs:Entries.universes_entry -> diff --git a/interp/impargs.ml b/interp/impargs.ml index 806fe93297..f3cdd64633 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -96,11 +96,11 @@ let set_maximality imps b = this kind if there is enough arguments to infer them) - [DepFlex] means that the implicit argument can be found by unification - along a collapsable path only (e.g. as x in (P x) where P is another + along a collapsible path only (e.g. as x in (P x) where P is another argument) (we do (defensively) print the arguments of this kind) - [DepFlexAndRigid] means that the least argument from which the - implicit argument can be inferred is following a collapsable path + implicit argument can be inferred is following a collapsible path but there is a greater argument from where the implicit argument is inferable following a rigid path (useful to know how to print a partial application) diff --git a/interp/impargs.mli b/interp/impargs.mli index ccdd448460..1099074c63 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -34,7 +34,7 @@ val with_implicit_protection : ('a -> 'b) -> 'a -> 'b (** {6 ... } *) (** An [implicits_list] is a list of positions telling which arguments - of a reference can be automatically infered *) + of a reference can be automatically inferred *) type argument_position = @@ -50,11 +50,11 @@ type implicit_explanation = this kind if there is enough arguments to infer them) *) | DepFlex of argument_position (** means that the implicit argument can be found by unification - along a collapsable path only (e.g. as x in (P x) where P is another + along a collapsible path only (e.g. as x in (P x) where P is another argument) (we do (defensively) print the arguments of this kind) *) | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position (** means that the least argument from which the - implicit argument can be inferred is following a collapsable path + implicit argument can be inferred is following a collapsible path but there is a greater argument from where the implicit argument is inferable following a rigid path (useful to know how to print a partial application) *) diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 49273c4146..a7e1de736c 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -48,7 +48,7 @@ let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = match onlyparse with | None -> (* Redeclare it to be used as (short) name in case an other (distfix) - notation was declared inbetween *) + notation was declared in between *) Notation.declare_uninterpretation (Notation.SynDefRule kn) pat | _ -> () end |