diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
tree | 074182834cb406d1304aec4233718564a9c06ba1 /plugins/omega/coq_omega.ml | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'plugins/omega/coq_omega.ml')
-rw-r--r-- | plugins/omega/coq_omega.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 37428c39..aac9a7d3 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 @@ -1462,7 +1462,7 @@ let coq_omega = let path = simplify_strong (new_id,new_var_num,display_var) system in if !display_action_flag then display_action display_var path; Tacticals.New.tclTHEN prelude (replay_history tactic_normalisation path) - with NO_CONTRADICTION -> Proofview.tclZERO (UserError ("" , Pp.str"Omega can't solve this system")) + with NO_CONTRADICTION -> Tacticals.New.tclZEROMSG (Pp.str"Omega can't solve this system") end end @@ -1689,7 +1689,7 @@ let onClearedName2 id tac = let destructure_hyps = Proofview.Goal.nf_enter begin fun gl -> - let type_of = Tacmach.New.pf_type_of gl in + let type_of = Tacmach.New.pf_unsafe_type_of gl in let decidability = Tacmach.New.of_old decidability gl in let pf_nf = Tacmach.New.of_old pf_nf gl in let rec loop = function |