diff options
| author | herbelin | 2009-10-25 07:36:43 +0000 |
|---|---|---|
| committer | herbelin | 2009-10-25 07:36:43 +0000 |
| commit | b02da518c51456b003c61f9775050fbfe6090629 (patch) | |
| tree | fd9d603b8829a6dfa1190ae111e84b136be59060 /pretyping | |
| parent | 28623d59a6381c7fb1c198ddca2dc382ba5c0e4c (diff) | |
Improved the treatment of Local/Global options (noneffective Local on
Implicit Arguments, Arguments Scope and Coercion fixed, noneffective
Global in sections for Hints and Notation detected).
Misc. improvements (comments + interpretation of Hint Constructors +
dev printer for hint_db).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12411 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 2 | ||||
| -rw-r--r-- | pretyping/classops.ml | 5 |
2 files changed, 5 insertions, 2 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 9406a57d79..7fa80b9a4d 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1286,7 +1286,7 @@ let matx_of_eqns env tomatchl eqns = We then look for a type U(..a1jk..b1 .. ..amjk..bm) so that T = U(..v1jk..t1 .. ..vmjk..tm). This a higher-order matching - problem with a priori different solution (one of them if T itself!). + problem with a priori different solutions (one of them if T itself!). We finally invert the uij and the ti and build the return clause diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 7ec77f7dca..2379632582 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -377,12 +377,15 @@ let discharge_coercion (_,(coe,stre,isid,cls,clt,ps)) = discharge_cl clt, n + ps) +let classify_coercion (coe,stre,isid,cls,clt,ps as obj) = + if stre = Local then Dispose else Substitute obj + let (inCoercion,_) = declare_object {(default_object "COERCION") with load_function = load_coercion; cache_function = cache_coercion; subst_function = subst_coercion; - classify_function = (fun x -> Substitute x); + classify_function = classify_coercion; discharge_function = discharge_coercion } let declare_coercion coef stre ~isid ~src:cls ~target:clt ~params:ps = |