diff options
| author | msozeau | 2006-04-10 12:05:05 +0000 |
|---|---|---|
| committer | msozeau | 2006-04-10 12:05:05 +0000 |
| commit | 264af456f928ee4e329b07449fec6846f78e0d93 (patch) | |
| tree | 0c2a369bd369134d60e2e12c7b169b72f89031ef /pretyping/evarutil.mli | |
| parent | 79fa2898ba31a2bfa484f3e9ac693ff714365758 (diff) | |
Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous and current version work).
Changed the type of typing constraints so as to have all the necessary information on abstract tycons.
Updates of subtac to use the new type.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8693 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 7260b5ad35..8c5fe9c99b 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -87,7 +87,7 @@ val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts val judge_of_new_Type : unit -> unsafe_judgment -type type_constraint_type = int * constr +type type_constraint_type = (int * int) option * constr type type_constraint = type_constraint_type option type val_constraint = constr option |