diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-11-19 10:39:34 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-11-19 10:39:34 +0000 |
| commit | 043345f19f76a0a2f45a2281a57d45f6d2459e8a (patch) | |
| tree | 83f4b32d7abeb0d8768b588d2d27b0fef2ea175f /pretyping/evd.mli | |
| parent | 11e1487d594d633b4db9a24eb4e12b25c755d88a (diff) | |
Raffinement de l'unification de "apply": mémorisation de certains
degrés de liberté concernant les instances de méta (cumulativité et
possibilité d'éta-expansion) de telle sorte que la fusion d'équations
se fasse modulo ces degrés de liberté.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9389 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evd.mli')
| -rw-r--r-- | pretyping/evd.mli | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 601c6c8b0..b4aa5fa5e 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -99,9 +99,18 @@ val metavars_of : constr -> Metaset.t val mk_freelisted : constr -> constr freelisted val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted +(* Status of an instance wrt to the meta it solves: + - a supertype of the meta (e.g. the solution to ?X <= T is a supertype of ?X) + - a subtype of the meta (e.g. the solution to T <= ?X is a supertype of ?X) + - a term that can be eta-expanded n times while still being a solution + (e.g. the solution [P] to [?X u v = P u v] can be eta-expanded twice) +*) + +type instance_status = IsSuperType | IsSubType | ConvUpToEta of int + type clbinding = | Cltyp of name * constr freelisted - | Clval of name * constr freelisted * constr freelisted + | Clval of name * (constr freelisted * instance_status) * constr freelisted val map_clb : (constr -> constr) -> clbinding -> clbinding @@ -146,13 +155,14 @@ val meta_list : evar_defs -> (metavariable * clbinding) list val meta_defined : evar_defs -> metavariable -> bool (* [meta_fvalue] raises [Not_found] if meta not in map or [Anomaly] if meta has no value *) -val meta_fvalue : evar_defs -> metavariable -> constr freelisted +val meta_fvalue : evar_defs -> metavariable -> constr freelisted * instance_status val meta_ftype : evar_defs -> metavariable -> constr freelisted val meta_name : evar_defs -> metavariable -> name val meta_with_name : evar_defs -> identifier -> metavariable val meta_declare : metavariable -> types -> ?name:name -> evar_defs -> evar_defs -val meta_assign : metavariable -> constr -> evar_defs -> evar_defs +val meta_assign : metavariable -> constr * instance_status -> evar_defs -> evar_defs +val meta_reassign : metavariable -> constr * instance_status -> evar_defs -> evar_defs (* [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *) val meta_merge : evar_defs -> evar_defs -> evar_defs |