diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-18 15:57:24 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-18 15:57:24 +0000 |
| commit | 8cf4e04fa817cf7ff9d73cb5cb7fff8b3b950387 (patch) | |
| tree | 30fbd47a7c79a0bc4e5d8a94db78294e6b62b02f /tactics/tactics.ml | |
| parent | 41dcb1603ea2e212a9167918f3d5dcb6f166e27b (diff) | |
Optimisation de clenv.ml pour que meta_instance ne soit pas appelé
abusivement sur les clauses.
Nettoyage au passage de metamap qui était utilisé à la fois pour les
substitutions de meta et pour les contextes de typage de meta.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11467 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 14 |
1 files changed, 5 insertions, 9 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 02d9544f0..65082c2ee 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -560,11 +560,12 @@ let error_uninstantiated_metas t clenv = in errorlabstrm "" (str "Cannot find an instance for " ++ pr_id id ++ str".") let clenv_refine_in with_evars id clenv gl = + let clenv = clenv_expand_metas clenv in let clenv = clenv_pose_dependent_evars with_evars clenv in - let new_hyp_typ = clenv_type clenv in + let new_hyp_typ = clenv_type clenv in if not with_evars & occur_meta new_hyp_typ then error_uninstantiated_metas new_hyp_typ clenv; - let new_hyp_prf = clenv_value clenv in + let new_hyp_prf = clenv_value_cast_meta clenv in tclTHEN (tclEVARS (evars_of clenv.evd)) (cut_replacing id new_hyp_typ @@ -597,12 +598,6 @@ let elimination_clause_scheme with_evars allow_K elimclause indclause gl = res_pf elimclause' ~with_evars:with_evars ~allow_K:allow_K ~flags:elim_flags gl -(* cast added otherwise tactics Case (n1,n2) generates (?f x y) and - * refine fails *) - -let type_clenv_binding wc (c,t) lbind = - clenv_type (make_clenv_binding wc (c,t) lbind) - (* * Elimination tactic with bindings and using an arbitrary * elimination constant called elimc. This constant should end @@ -947,7 +942,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 clause = clenv_expand_metas clause in + let (thd,tstack) = whd_stack (clenv_direct_value clause) in let nargs = List.length tstack in let tstack = match mopt with | Some m -> |