diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-29 17:13:46 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-29 17:13:46 +0000 |
| commit | 9a75bfec45650d7b95288125d6e00777c890bc25 (patch) | |
| tree | d3d29de077ace56c1104afb7e63c620eda6509eb /toplevel | |
| parent | 378edbeede113c3bfdb9d2b46d5bfae19e96be65 (diff) | |
Suppression cast inutile
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1033 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/class.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml index e6e4654b5..7b803fb4d 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -244,11 +244,11 @@ let build_id_coercion idf_opt ids = (mkProd (Anonymous, applistc vs (rel_list 0 llams), lift 1 t)) lams in - let constr_f = mkCast (val_f, typ_f) in (* juste pour verification *) let _ = try - Typing.type_of env Evd.empty constr_f + Reduction.conv_leq env Evd.empty + (Typing.type_of env Evd.empty val_f) typ_f with _ -> error ("cannot be defined as coercion - "^ "may be a bad number of arguments") @@ -261,7 +261,7 @@ let build_id_coercion idf_opt ids = (string_of_cl (fst (constructor_at_head t)))) in let constr_entry = - { const_entry_body = constr_f; const_entry_type = None } in + { const_entry_body = val_f; const_entry_type = None } in declare_constant idf (ConstantEntry constr_entry,NeverDischarge); idf |