diff options
| author | herbelin | 2006-10-12 12:59:32 +0000 |
|---|---|---|
| committer | herbelin | 2006-10-12 12:59:32 +0000 |
| commit | 3f1271efd6caf66282926e2a80d90b71b5882b9d (patch) | |
| tree | 7573f6086849188eb08440ba9e685fc6e87fcd3c /kernel | |
| parent | 813f6748aadc060b76e6c4c4484d8e0de48ff7a8 (diff) | |
Protection raise en début de séquence (en attendant que le code caché trouve sa place)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9235 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/subtyping.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 6de7819af9..0acd37da4e 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -176,19 +176,21 @@ let check_constant cst env msid1 l info1 cb2 spec2 = in cst | IndType ((kn,i),mind1) -> - Util.error ("The kernel does not recognize yet that a parameter can be " ^ + ignore (Util.error ( + "The kernel does not recognize yet that a parameter can be " ^ "instantiated by an inductive type. Hint: you can rename the " ^ "inductive type and give a definition to map the old name to the new " ^ - "name.") ; + "name.")); assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ; if cb2.const_body <> None then error () ; let arity1 = type_of_inductive (mind1,mind1.mind_packets.(i)) in check_conv cst conv_leq env arity1 cb2.const_type | IndConstr (((kn,i),j) as cstr,mind1) -> - Util.error ("The kernel does not recognize yet that a parameter can be " ^ + ignore (Util.error ( + "The kernel does not recognize yet that a parameter can be " ^ "instantiated by a constructor. Hint: you can rename the " ^ "constructor and give a definition to map the old name to the new " ^ - "name.") ; + "name.")); assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ; if cb2.const_body <> None then error () ; let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in |