diff options
| author |  Stephane Glondu <steph@glondu.net> | 2009-02-19 13:13:14 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2009-02-19 13:13:14 +0100 |
| commit | a0a94c1340a63cdb824507b973393882666ba52a (patch) | |
| tree | 73aa4eb32cbd176379bc91b21c184e2a6882bfe3 /tactics/tactics.ml | |
| parent | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (diff) | |
Imported Upstream version 8.2-1+dfsgupstream/8.2-1+dfsg
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5af5c0d5..2c567034 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tactics.ml 11745 2009-01-04 18:43:08Z herbelin $ *) +(* $Id: tactics.ml 11897 2009-02-09 19:28:02Z barras $ *) open Pp open Util @@ -759,7 +759,7 @@ let general_apply with_delta with_destruct with_evars (c,lbind) gl0 = let concl_nprod = nb_prod (pf_concl gl0) in let evm, c = c in let rec try_main_apply c gl = - let thm_ty0 = nf_betaiota (pf_type_of gl c) in + let thm_ty0 = nf_betaiota (project gl) (pf_type_of gl c) in let try_apply thm_ty nprod = let n = nb_prod thm_ty - nprod in if n<0 then error "Applied theorem has not enough premisses."; @@ -850,7 +850,7 @@ let progress_with_clause flags innerclause clause = with Failure _ -> error "Unable to unify." let apply_in_once_main flags innerclause (d,lbind) gl = - let thm = nf_betaiota (pf_type_of gl d) in + let thm = nf_betaiota gl.sigma (pf_type_of gl d) in let rec aux clause = try progress_with_clause flags innerclause clause with err -> @@ -985,7 +985,8 @@ let specialize mopt (c,lbind) g = else let clause = make_clenv_binding g (c,pf_type_of g c) lbind in let clause = clenv_unify_meta_types clause in - let (thd,tstack) = whd_stack (clenv_value clause) in + let (thd,tstack) = + whd_stack (evars_of clause.evd) (clenv_value clause) in let nargs = List.length tstack in let tstack = match mopt with | Some m -> |