diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-29 14:57:58 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-29 14:57:58 +0000 |
| commit | 2040379ec1d79ff588498ca6f20d8c7b75d74533 (patch) | |
| tree | 030ab3eebf66961746ba164ca72a821a88d18851 /pretyping/recordops.mli | |
| parent | 42088723410c0aef9767ee0cd18735eb081f05a6 (diff) | |
Préférence donnée aux constantes qui ne sont pas des projections
canoniques lors d'une unification constante/constante s'apprêtant à
déplier l'une des deux constantes (suggestion des utilisateurs de
structures canoniques), ceci afin de préserver des possibilités
ultérieures de résolution d'evars par équipement en structure
canonique.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11187 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/recordops.mli')
| -rwxr-xr-x | pretyping/recordops.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 348407ae1..d41ede8bb 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -53,5 +53,6 @@ val cs_pattern_of_constr : constr -> cs_pattern * int * constr list val lookup_canonical_conversion : (global_reference * cs_pattern) -> obj_typ val declare_canonical_structure : global_reference -> unit +val is_canonical_projection : constr -> bool val canonical_projections : unit -> ((global_reference * cs_pattern) * obj_typ) list |