From ed95f122f3c68becc09c653471dc2982b346d343 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 13 Oct 2015 18:30:47 +0200 Subject: Fix some typos. --- plugins/omega/coq_omega.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/omega') diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 710a2394d..aac9a7d31 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -539,7 +539,7 @@ let context operation path (t : constr) = in loop 1 path t -let occurence path (t : constr) = +let occurrence path (t : constr) = let rec loop p0 t = match (p0,kind_of_term t) with | (p, Cast (c,_,_)) -> loop p c | ([], _) -> t @@ -555,7 +555,7 @@ let occurence path (t : constr) = | ((P_TYPE :: p), Lambda (n,term,c)) -> loop p term | ((P_TYPE :: p), LetIn (n,b,term,c)) -> loop p term | (p, _) -> - failwith ("occurence " ^ string_of_int(List.length p)) + failwith ("occurrence " ^ string_of_int(List.length p)) in loop path t @@ -660,7 +660,7 @@ let clever_rewrite_gen_nat p result (t,args) = let clever_rewrite p vpath t gl = let full = pf_concl gl in let (abstracted,occ) = abstract_path (Lazy.force coq_Z) (List.rev p) full in - let vargs = List.map (fun p -> occurence p occ) vpath in + let vargs = List.map (fun p -> occurrence p occ) vpath in let t' = applist(t, (vargs @ [abstracted])) in exact (applist(t',[mkNewMeta()])) gl -- cgit v1.2.3