diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-09-12 11:02:30 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-09-12 11:02:30 +0000 |
| commit | 6fcd224c128ae5e81f4cce9d5de1ac45883cfebf (patch) | |
| tree | 9d5c886b18ca44f3a24de7b58c7dd7ca8bc88eec /tactics/wcclausenv.ml | |
| parent | 9248485d71d1c9c1796a22e526e07784493e2008 (diff) | |
Modification mkAppL; abstraction via kind_of_term; changement dans Reduction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@597 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/wcclausenv.ml')
| -rw-r--r-- | tactics/wcclausenv.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml index 4f071980e..de5adc94d 100644 --- a/tactics/wcclausenv.ml +++ b/tactics/wcclausenv.ml @@ -132,15 +132,14 @@ and build_term ce p_0 c = match p_0, kind_of_term c with | ((na,Some t), IsMeta mv) -> (* let mv = new_meta() in *) - (DOP0(Meta mv), - clenv_pose (na,mv,t) ce) + (mkMeta mv, clenv_pose (na,mv,t) ce) | ((na,_), IsCast (c,t)) -> build_term ce (na,Some t) c | ((na,Some t), _) -> if (not((occur_meta c))) then (c,ce) else let (hd,args) = - whd_betadeltaiota_stack env (w_Underlying ce.hook) c [] in + whd_betadeltaiota_stack env (w_Underlying ce.hook) c in let hdty = w_type_of ce.hook hd in let (args,ce') = build_args [] ce (w_whd_betadeltaiota ce.hook hdty) args in @@ -155,7 +154,7 @@ and build_term ce p_0 c = (c,ce) else let (hd,args) = - whd_betadeltaiota_stack env (w_Underlying ce.hook) c [] in + whd_betadeltaiota_stack env (w_Underlying ce.hook) c in let hdty = w_type_of ce.hook hd in let (args,ce') = build_args [] ce (w_whd_betadeltaiota ce.hook hdty) args in |