diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-02-22 18:15:04 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-02-22 18:15:04 +0000 |
| commit | 6211008540c9b61c10df25eea54ff9116eb08e4a (patch) | |
| tree | dc94120a5ef5df3106cfc7d3a10c3aa058f0400b /pretyping/clenv.mli | |
| parent | 79685e0611dff650b8185f5531c4da40840c1a08 (diff) | |
Ajout fonction clenv_conv_leq pour résoudre les pbs de la forme
"R ?1 ... ?n <= T". Utilisation de cette fonction dans Setoid_replace au
au lieu de w_unify (suggestion de GG).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9673 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/clenv.mli')
| -rw-r--r-- | pretyping/clenv.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index 98950458e..b855ee7e0 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -125,6 +125,10 @@ val clenv_environments : val clenv_environments_evars : env -> evar_defs -> int option -> types -> evar_defs * constr list * types +(* [clenv_conv_leq env sigma t c n] looks for c1...cn s.t. [t <= c c1...cn] *) +val clenv_conv_leq : + env -> evar_map -> types -> constr -> int -> constr list + (* if the clause is a product, add an extra meta for this product *) exception NotExtensibleClause val clenv_push_prod : clausenv -> clausenv |