diff options
author | 2017-05-31 12:30:50 -0400 | |
---|---|---|
committer | 2017-06-02 20:06:05 -0400 | |
commit | 6a67a0e30bdd96df994dd7d309d1f0d8cc22751f (patch) | |
tree | 7f0f8129d69a3dd4fdeacf30dd773bc42e9a95f6 /pretyping | |
parent | 42d510ceea82d617ac4e630049d690acbe900688 (diff) |
Drop '.' from CErrors.anomaly, insert it in args
As per https://github.com/coq/coq/pull/716#issuecomment-305140839
Partially using
```bash
git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i
```
and
```bash
git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i
```
The rest were manually edited by looking at the results of
```bash
git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less
```
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/cases.ml | 24 | ||||
-rw-r--r-- | pretyping/coercion.ml | 4 | ||||
-rw-r--r-- | pretyping/detyping.ml | 4 | ||||
-rw-r--r-- | pretyping/evarconv.ml | 4 | ||||
-rw-r--r-- | pretyping/evarsolve.ml | 4 | ||||
-rw-r--r-- | pretyping/indrec.ml | 6 | ||||
-rw-r--r-- | pretyping/inductiveops.ml | 2 | ||||
-rw-r--r-- | pretyping/locusops.ml | 2 | ||||
-rw-r--r-- | pretyping/nativenorm.ml | 12 | ||||
-rw-r--r-- | pretyping/patternops.ml | 4 | ||||
-rw-r--r-- | pretyping/pretyping.ml | 4 | ||||
-rw-r--r-- | pretyping/reductionops.ml | 6 | ||||
-rw-r--r-- | pretyping/retyping.ml | 2 | ||||
-rw-r--r-- | pretyping/tacred.ml | 4 | ||||
-rw-r--r-- | pretyping/typing.ml | 6 | ||||
-rw-r--r-- | pretyping/vnorm.ml | 2 |
16 files changed, 45 insertions, 45 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 80680e408..efab5b977 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -70,7 +70,7 @@ let error_wrong_numarg_inductive ?loc env c n = let list_try_compile f l = let rec aux errors = function - | [] -> if errors = [] then anomaly (str "try_find_f") else iraise (List.last errors) + | [] -> if errors = [] then anomaly (str "try_find_f.") else iraise (List.last errors) | h::t -> try f h with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ as e -> @@ -162,9 +162,9 @@ let feed_history arg = function | Continuation (n, l, h) when n>=1 -> Continuation (n-1, arg :: l, h) | Continuation (n, _, _) -> - anomaly (str "Bad number of expected remaining patterns: " ++ int n) + anomaly (str "Bad number of expected remaining patterns: " ++ int n ++ str ".") | Result _ -> - anomaly (Pp.str "Exhausted pattern history") + anomaly (Pp.str "Exhausted pattern history.") (* This is for non exhaustive error message *) @@ -190,7 +190,7 @@ let pop_history_pattern = function | Continuation (0, l, MakeConstructor (pci, rh)) -> feed_history (CAst.make @@ PatCstr (pci,List.rev l,Anonymous)) rh | _ -> - anomaly (Pp.str "Constructor not yet filled with its arguments") + anomaly (Pp.str "Constructor not yet filled with its arguments.") let pop_history h = feed_history (CAst.make @@ PatVar Anonymous) h @@ -425,7 +425,7 @@ let lift_tomatch_type n = liftn_tomatch_type n 1 let current_pattern eqn = match eqn.patterns with | pat::_ -> pat - | [] -> anomaly (Pp.str "Empty list of patterns") + | [] -> anomaly (Pp.str "Empty list of patterns.") let alias_of_pat = CAst.with_val (function | PatVar name -> name @@ -438,7 +438,7 @@ let remove_current_pattern eqn = { eqn with patterns = pats; alias_stack = alias_of_pat pat :: eqn.alias_stack } - | [] -> anomaly (Pp.str "Empty list of patterns") + | [] -> anomaly (Pp.str "Empty list of patterns.") let push_current_pattern (cur,ty) eqn = match eqn.patterns with @@ -447,7 +447,7 @@ let push_current_pattern (cur,ty) eqn = { eqn with rhs = { eqn.rhs with rhs_env = rhs_env }; patterns = pats } - | [] -> anomaly (Pp.str "Empty list of patterns") + | [] -> anomaly (Pp.str "Empty list of patterns.") (* spiwack: like [push_current_pattern] but does not introduce an alias in rhs_env. Aliasing binders are only useful for variables at @@ -457,7 +457,7 @@ let push_noalias_current_pattern eqn = match eqn.patterns with | _::pats -> { eqn with patterns = pats } - | [] -> anomaly (Pp.str "push_noalias_current_pattern: Empty list of patterns") + | [] -> anomaly (Pp.str "push_noalias_current_pattern: Empty list of patterns.") @@ -641,7 +641,7 @@ let replace_tomatch sigma n c = | Pushed (initial,((b,tm),l,na)) :: rest -> let b = replace_term sigma n c depth b in let tm = map_tomatch_type (replace_term sigma n c depth) tm in - List.iter (fun i -> if Int.equal i (n + depth) then anomaly (Pp.str "replace_tomatch")) l; + List.iter (fun i -> if Int.equal i (n + depth) then anomaly (Pp.str "replace_tomatch.")) l; Pushed (initial,((b,tm),l,na)) :: replrec depth rest | Alias (initial,(na,b,d)) :: rest -> (* [b] is out of replacement scope *) @@ -882,7 +882,7 @@ let specialize_predicate_var (cur,typ,dep) env tms ccl = (*****************************************************************************) let generalize_predicate sigma (names,na) ny d tms ccl = let () = match na with - | Anonymous -> anomaly (Pp.str "Undetected dependency") + | Anonymous -> anomaly (Pp.str "Undetected dependency.") | _ -> () in let p = List.length names + 1 in let ccl = lift_predicate 1 ccl tms in @@ -1708,7 +1708,7 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t = evdref := evd; (t,tt) in let b = e_cumul env evdref tt (mkSort s) (* side effect *) in - if not b then anomaly (Pp.str "Build_tycon: should be a type"); + if not b then anomaly (Pp.str "Build_tycon: should be a type."); { uj_val = t; uj_type = tt } (* For a multiple pattern-matching problem Xi on t1..tn with return @@ -1872,7 +1872,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = if not (eq_ind ind ind') then user_err ?loc (str "Wrong inductive type."); if not (Int.equal nrealargs_ctxt (List.length realnal)) then - anomaly (Pp.str "Ill-formed 'in' clause in cases"); + anomaly (Pp.str "Ill-formed 'in' clause in cases."); List.rev realnal | None -> List.make nrealargs_ctxt Anonymous in LocalAssum (na, EConstr.of_constr (build_dependent_inductive env0 indf')) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 83c26058a..1282e3cb8 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -67,7 +67,7 @@ let apply_coercion_args env evd check isproj argl funj = if check && not (e_cumul env evdref (Retyping.get_type_of env !evdref h) c1) then raise NoCoercion; apply_rec (h::acc) (subst1 h c2) restl - | _ -> anomaly (Pp.str "apply_coercion_args") + | _ -> anomaly (Pp.str "apply_coercion_args.") in let res = apply_rec [] funj.uj_type argl in !evdref, res @@ -368,7 +368,7 @@ let apply_coercion env sigma p hj typ_cl = (hj,typ_cl,sigma) p in evd, j with NoCoercion as e -> raise e - | e when CErrors.noncritical e -> anomaly (Pp.str "apply_coercion") + | e when CErrors.noncritical e -> anomaly (Pp.str "apply_coercion.") (* Try to coerce to a funclass; raise NoCoercion if not possible *) let inh_app_fun_core env evd j = diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 13e2e5d71..c93b1e568 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -425,7 +425,7 @@ type binder_kind = BProd | BLambda | BLetIn (**********************************************************************) (* Main detyping function *) -let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable")) +let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable.")) let set_detype_anonymous f = detype_anonymous := f let detype_level sigma l = @@ -508,7 +508,7 @@ let rec detype flags avoid env sigma t = CAst.make @@ let body' = EConstr.of_constr body' in substl (c :: List.rev args) body' with Retyping.RetypeError _ | Not_found -> - anomaly (str"Cannot detype an unfolded primitive projection") + anomaly (str"Cannot detype an unfolded primitive projection.") in (detype flags avoid env sigma c').CAst.v else if print_primproj_params () then diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index e2106dab5..1d6b611da 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -605,7 +605,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty postpone to see if other equations help, as in: [Check fun a b c : unit => (eqᵣefl : _ a b = _ c a b)] *) UnifFailure (i,NotSameArgSize) - | _, _ -> anomaly (Pp.str "Unexpected result from ise_stack2") + | _, _ -> anomaly (Pp.str "Unexpected result from ise_stack2.") and f2 i = if Evar.equal sp1 sp2 then @@ -1088,7 +1088,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = let filter' = filter_possible_projections evd c ty ctxt args in (id,t,c,ty,evs,Filter.make filter',occs) :: make_subst (ctxt',l,occsl) | _, _, [] -> [] - | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list") in + | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list.") in let rec set_holes evdref rhs = function | (id,_,c,cty,evsref,filter,occs)::subst -> diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 98e71c7fd..de5a62726 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -634,7 +634,7 @@ let make_projectable_subst aliases sigma evi args = cstrs) | _ -> (rest,Id.Map.add id [a,normalize_alias_opt sigma aliases a,id] all,cstrs)) - | _ -> anomaly (Pp.str "Instance does not match its signature")) + | _ -> anomaly (Pp.str "Instance does not match its signature.")) sign (Array.rev_to_list args,Id.Map.empty,Constrmap.empty) in (full_subst,cstr_subst) @@ -828,7 +828,7 @@ let rec find_projectable_vars with_evars aliases sigma y subst = | _ -> subst' end | [] -> subst' - | _ -> anomaly (Pp.str "More than one non var in aliases class of evar instance") + | _ -> anomaly (Pp.str "More than one non var in aliases class of evar instance.") else subst' in Id.Map.fold is_projectable subst [] diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index c4a74d990..8a902f3a3 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -296,7 +296,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = process_constr (push_rel d env) (i+1) (lift 1 f) (cprest,rest)) | [],[] -> f - | _,[] | [],_ -> anomaly (Pp.str "process_constr") + | _,[] | [],_ -> anomaly (Pp.str "process_constr.") in process_constr env 0 f (List.rev cstr.cs_args, recargs) @@ -533,7 +533,7 @@ let weaken_sort_scheme env evd set sort npars term ty = mkProd (n, t, c'), mkLambda (n, t, term') | LetIn (n,b,t,c) -> let c',term' = drec np c in mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term') - | _ -> anomaly ~label:"weaken_sort_scheme" (Pp.str "wrong elimination type") + | _ -> anomaly ~label:"weaken_sort_scheme" (Pp.str "wrong elimination type.") in let ty, term = drec npars ty in !evdref, ty, term @@ -577,7 +577,7 @@ let build_mutual_induction_scheme env sigma = function in let _ = check_arities env listdepkind in mis_make_indrec env sigma listdepkind mib u - | _ -> anomaly (Pp.str "build_induction_scheme expects a non empty list of inductive types") + | _ -> anomaly (Pp.str "build_induction_scheme expects a non empty list of inductive types.") let build_induction_scheme env sigma pind dep kind = let (mib,mip) = lookup_mind_specif env (fst pind) in diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 7f3bafc68..d8252ea9b 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -538,7 +538,7 @@ let is_predicate_explicitly_dep env sigma pred arsign = | Name _ -> true end - | _ -> anomaly (Pp.str "Non eta-expanded dep-expanded \"match\" predicate") + | _ -> anomaly (Pp.str "Non eta-expanded dep-expanded \"match\" predicate.") in srec env (EConstr.of_constr pred) arsign diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index 211ffbe01..e555742bc 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -84,7 +84,7 @@ let concrete_clause_of enum_hyps cl = (** Miscellaneous functions *) let out_arg = function - | Misctypes.ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable") + | Misctypes.ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable.") | Misctypes.ArgArg x -> x let occurrences_of_hyp id cls = diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 10d9173f1..61118cf77 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -139,7 +139,7 @@ let type_of_var env id = let open Context.Named.Declaration in try env |> lookup_named id |> get_type with Not_found -> - anomaly ~label:"type_of_var" (str "variable " ++ Id.print id ++ str " unbound") + anomaly ~label:"type_of_var" (str "variable " ++ Id.print id ++ str " unbound.") let sort_of_product env domsort rangsort = match (domsort, rangsort) with @@ -183,7 +183,7 @@ let rec nf_val env sigma v typ = try decompose_prod env typ with DestKO -> CErrors.anomaly - (Pp.strbrk "Returned a functional value in a type not recognized as a product type") + (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") in let env = push_rel (LocalAssum (name,dom)) env in let body = nf_val env sigma (f (mk_rel_accu lvl)) codom in @@ -229,7 +229,7 @@ and nf_args env sigma accu t = try decompose_prod env t with DestKO -> CErrors.anomaly - (Pp.strbrk "Returned a functional value in a type not recognized as a product type") + (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") in let c = nf_val env sigma arg dom in (subst1 c codom, c::l) @@ -246,7 +246,7 @@ and nf_bargs env sigma b t = try decompose_prod env !t with DestKO -> CErrors.anomaly - (Pp.strbrk "Returned a functional value in a type not recognized as a product type") + (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") in let c = nf_val env sigma (block_field b i) dom in t := subst1 c codom; c) @@ -357,7 +357,7 @@ and nf_predicate env sigma ind mip params v pT = try decompose_prod env pT with DestKO -> CErrors.anomaly - (Pp.strbrk "Returned a functional value in a type not recognized as a product type") + (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") in let dep,body = nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in @@ -405,7 +405,7 @@ let native_norm env sigma c ty = let time_info = Format.sprintf "Reification done in %.5f@." (t2 -. t1) in if !Flags.debug then Feedback.msg_debug (Pp.str time_info); EConstr.of_constr res - | _ -> anomaly (Pp.str "Compilation failure") + | _ -> anomaly (Pp.str "Compilation failure.") let native_conv_generic pb sigma t = Nativeconv.native_conv_gen pb (evars_of_evar_map sigma) t diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 0818a5525..845ac4fb7 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -112,14 +112,14 @@ let rec head_pattern_bound t = -> raise BoundPattern (* Perhaps they were arguments, but we don't beta-reduce *) | PLambda _ -> raise BoundPattern - | PCoFix _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type") + | PCoFix _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type.") let head_of_constr_reference sigma c = match EConstr.kind sigma c with | Const (sp,_) -> ConstRef sp | Construct (sp,_) -> ConstructRef sp | Ind (sp,_) -> IndRef sp | Var id -> VarRef id - | _ -> anomaly (Pp.str "Not a rigid reference") + | _ -> anomaly (Pp.str "Not a rigid reference.") let pattern_of_constr env sigma t = let rec pattern_of_constr env t = diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index b0663af70..1d12b6d51 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -199,7 +199,7 @@ let interp_universe_level_name ~anon_rigidity evd (loc, s) = let names, _ = Global.global_universe_names () in if CString.string_contains ~where:s ~what:"." then match List.rev (CString.split '.' s) with - | [] -> anomaly (str"Invalid universe name " ++ str s) + | [] -> anomaly (str"Invalid universe name " ++ str s ++ str".") | n :: dp -> let num = int_of_string n in let dp = DirPath.make (List.map Id.of_string dp) in @@ -1149,7 +1149,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function | Sort s -> ESorts.kind sigma s | Evar ev when is_Type (existential_type sigma ev) -> evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev - | _ -> anomaly (Pp.str "Found a type constraint which is not a type") + | _ -> anomaly (Pp.str "Found a type constraint which is not a type.") in { utj_val = v; utj_type = s } diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 5a2328aaa..c976fe66d 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1445,7 +1445,7 @@ let instance sigma s c = let hnf_prod_app env sigma t n = match EConstr.kind sigma (whd_all env sigma t) with | Prod (_,_,b) -> subst1 n b - | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product") + | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product.") let hnf_prod_appvect env sigma t nl = Array.fold_left (fun acc t -> hnf_prod_app env sigma acc t) t nl @@ -1456,7 +1456,7 @@ let hnf_prod_applist env sigma t nl = let hnf_lam_app env sigma t n = match EConstr.kind sigma (whd_all env sigma t) with | Lambda (_,_,b) -> subst1 n b - | _ -> anomaly ~label:"hnf_lam_app" (Pp.str "Need an abstraction") + | _ -> anomaly ~label:"hnf_lam_app" (Pp.str "Need an abstraction.") let hnf_lam_appvect env sigma t nl = Array.fold_left (fun acc t -> hnf_lam_app env sigma acc t) t nl @@ -1693,5 +1693,5 @@ let betazetaevar_applist sigma n c l = | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack | Evar _, _ -> applist (substl env t, stack) - | _ -> anomaly (Pp.str "Not enough lambda/let's") in + | _ -> anomaly (Pp.str "Not enough lambda/let's.") in stacklam n [] c l diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 496c706ec..a1d0977f5 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -48,7 +48,7 @@ let retype_error re = raise (RetypeError re) let anomaly_on_error f x = try f x - with RetypeError e -> anomaly ~label:"retyping" (print_retype_error e) + with RetypeError e -> anomaly ~label:"retyping" (print_retype_error e ++ str ".") let get_type_from_constraints env sigma t = if isEvar sigma (fst (decompose_app_vect sigma t)) then diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 3d41d2ddd..f2b0995b0 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -107,7 +107,7 @@ let destEvalRefU sigma c = match EConstr.kind sigma c with | Var id -> (EvalVar id, EInstance.empty) | Rel n -> (EvalRel n, EInstance.empty) | Evar ev -> (EvalEvar ev, EInstance.empty) - | _ -> anomaly (Pp.str "Not an unfoldable reference") + | _ -> anomaly (Pp.str "Not an unfoldable reference.") let unsafe_reference_opt_value env sigma eval = match eval with @@ -307,7 +307,7 @@ let compute_consteval_mutual_fix env sigma ref = (* Forget all \'s and args and do as if we had started with c' *) let ref,_ = destEvalRefU sigma c' in (match unsafe_reference_opt_value env sigma ref with - | None -> anomaly (Pp.str "Should have been trapped by compute_direct") + | None -> anomaly (Pp.str "Should have been trapped by compute_direct.") | Some c -> srec env (minarg-nargs) [] ref c) | _ -> (* Should not occur *) NotAnElimination in diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 757e12451..7ad988ad0 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -31,7 +31,7 @@ let push_rec_types pfix env = let meta_type evd mv = let ty = try Evd.meta_ftype evd mv - with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv)) in + with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv) ++ str ".") in let ty = Evd.map_fl EConstr.of_constr ty in meta_instance evd ty @@ -121,11 +121,11 @@ let lambda_applist_assum sigma n c l = let rec app n subst t l = if Int.equal n 0 then if l == [] then substl subst t - else anomaly (Pp.str "Not enough arguments") + else anomaly (Pp.str "Not enough arguments.") else match EConstr.kind sigma t, l with | Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l - | _ -> anomaly (Pp.str "Not enough lambda/let's") in + | _ -> anomaly (Pp.str "Not enough lambda/let's.") in app n [] c l let e_type_case_branches env evdref (ind,largs) pj c = diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index ec52da07c..b08666483 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -314,7 +314,7 @@ and nf_fun env sigma f typ = with DestKO -> (* 27/2/13: Turned this into an anomaly *) CErrors.anomaly - (Pp.strbrk "Returned a functional value in a type not recognized as a product type") + (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") in let body = nf_val (push_rel (LocalAssum (name,dom)) env) sigma vb codom in mkLambda(name,dom,body) |