diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-06-16 14:41:51 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-06-16 14:41:51 +0000 |
| commit | e978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch) | |
| tree | 0de2a907ee93c795978f3c843155bee91c11ed60 /contrib/field/field.ml4 | |
| parent | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff) | |
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'contrib/field/field.ml4')
| -rw-r--r-- | contrib/field/field.ml4 | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4 index 35591f23..47e583fd 100644 --- a/contrib/field/field.ml4 +++ b/contrib/field/field.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: field.ml4 7837 2006-01-11 09:47:32Z herbelin $ *) +(* $Id: field.ml4 8866 2006-05-28 16:21:04Z herbelin $ *) open Names open Pp @@ -22,19 +22,22 @@ open Vernacinterp open Vernacexpr open Tacexpr open Mod_subst +open Coqlib (* Interpretation of constr's *) let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c (* Construction of constants *) -let constant dir s = Coqlib.gen_constant "Field" ("field"::dir) s +let constant dir s = gen_constant "Field" ("field"::dir) s +let init_constant s = gen_constant_in_modules "Field" init_modules s (* To deal with the optional arguments *) let constr_of_opt a opt = let ac = constr_of a in + let ac3 = mkArrow ac (mkArrow ac ac) in match opt with - | None -> mkApp ((constant ["Field_Compl"] "Field_None"),[|ac|]) - | Some f -> mkApp ((constant ["Field_Compl"] "Field_Some"),[|ac;constr_of f|]) + | None -> mkApp (init_constant "None",[|ac3|]) + | Some f -> mkApp (init_constant "Some",[|ac3;constr_of f|]) (* Table of theories *) let th_tab = ref (Gmap.empty : (constr,constr) Gmap.t) |