diff options
| author | filliatr | 1999-10-13 12:36:57 +0000 |
|---|---|---|
| committer | filliatr | 1999-10-13 12:36:57 +0000 |
| commit | 002d6cb09f2447134677b438ab09e880a2881151 (patch) | |
| tree | 24ffa08aa1409f87da66216ec924f81357be7846 /kernel/instantiate.ml | |
| parent | e148fce6fa35cc1bd3041ce18c87f5573f5bd596 (diff) | |
plus de recettes pour les corps des constantes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@100 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/instantiate.ml')
| -rw-r--r-- | kernel/instantiate.ml | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml index 679789d6ce..e1f9356df8 100644 --- a/kernel/instantiate.ml +++ b/kernel/instantiate.ml @@ -42,15 +42,14 @@ let constant_value env k = let cb = lookup_constant sp env in if not cb.const_opaque & defined_constant env k then match cb.const_body with - Some { contents = Cooked body } -> - instantiate_constr - (ids_of_sign cb.const_hyps) body (Array.to_list args) - | Some { contents = Recipe _ } -> - anomalylabstrm "termenv__constant_value" - [< 'sTR "a transparent constant which was not cooked" >] - | None -> anomalylabstrm "termenv__constant_value" - [< 'sTR "a defined constant as no body." >] - else failwith "opaque" + | Some body -> + instantiate_constr + (ids_of_sign cb.const_hyps) body (Array.to_list args) + | None -> + anomalylabstrm "termenv__constant_value" + [< 'sTR "a defined constant as no body." >] + else + failwith "opaque" let const_abst_opt_value env c = match c with |