diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-23 22:01:09 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-23 22:01:09 +0000 |
| commit | cd21a1067dcf4506a69f86c42a593c21dca5abd5 (patch) | |
| tree | 8cb7bbaa18e939682c5c456f0f0de6b136aef1fa /pretyping | |
| parent | 41b9c2f328be7232aabb27b7d7385326ca58767f (diff) | |
Prise en compte application partielle dans dependent
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3478 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/termops.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index c93698783..b233ce244 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -386,7 +386,13 @@ let dependent m t = if eq_constr m t then raise Occur else - iter_constr_with_binders (lift 1) deprec m t + match kind_of_term m, kind_of_term t with + | App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt -> + deprec m (mkApp (ft,Array.sub lt 0 (Array.length lm))); + Array.iter (deprec m) + (Array.sub lt + (Array.length lm) ((Array.length lt) - (Array.length lm))) + | _ -> iter_constr_with_binders (lift 1) deprec m t in try deprec m t; false with Occur -> true |