diff options
| author | corbinea | 2007-04-26 08:54:28 +0000 |
|---|---|---|
| committer | corbinea | 2007-04-26 08:54:28 +0000 |
| commit | ea1eaa9b152b73652f417e02bd469e5b289cec47 (patch) | |
| tree | 4d654ad1434bac0781eb4f3e6f1505c3895df4ba /tactics/decl_interp.ml | |
| parent | 40425048feff138e6c67555c7ee94142452d1cae (diff) | |
fin des conclusions multiples
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9796 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/decl_interp.ml')
| -rw-r--r-- | tactics/decl_interp.ml | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml index 87a472003f..02c688e251 100644 --- a/tactics/decl_interp.ml +++ b/tactics/decl_interp.ml @@ -166,11 +166,7 @@ let decompose_eq env id = | _ -> error "previous step is not an equality" let get_eq_typ info env = - let last_id = - match info.pm_last with - None -> error "no previous equality" - | Some (id,_) -> id in - let typ = decompose_eq env last_id in + let typ = decompose_eq env (get_last env) in typ let interp_constr_in_type typ sigma env c = @@ -352,8 +348,6 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = let pat_vars,aliases,patt = interp_pattern env pat in let inject = function Thesis (Plain) -> Rawterm.RSort(dummy_loc,RProp Null) - | Thesis (Sub n) -> - error "thesis[_] is not allowed here" | Thesis (For rec_occ) -> if not (List.mem rec_occ pat_vars) then errorlabstrm "suppose it is" @@ -405,7 +399,7 @@ let interp_suffices_clause sigma env (hyps,cot)= This (c,_) -> let nhyps,nc = interp_hyps_gen fst (fun x _ -> x) sigma env hyps c in nhyps,This nc - | Thesis (Plain| Sub _) as th -> interp_hyps sigma env hyps,th + | Thesis Plain as th -> interp_hyps sigma env hyps,th | Thesis (For n) -> error "\"thesis for\" is not applicable here" in let push_one hyp env0 = match hyp with |