diff options
| author | herbelin | 2002-06-03 10:28:40 +0000 |
|---|---|---|
| committer | herbelin | 2002-06-03 10:28:40 +0000 |
| commit | e860dcf1df4d7042aa872ba4ad914d1d64d574cf (patch) | |
| tree | ccaea77ed45e472307e5b3c9023aebfbb0d6dff9 /contrib/interface | |
| parent | 3eb35bf30c52aad878867650a233744b7028a62d (diff) | |
Intgration uniforme de coercions dans les dclarations (Variable and co) et retouche des Record
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2747 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/name_to_ast.ml | 4 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 5 |
2 files changed, 5 insertions, 4 deletions
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index 0f3dcdf67e..5ba5e0e7e8 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -97,7 +97,7 @@ let convert_constructors envpar names types = array_map2 (fun n t -> let coercion_flag = false (* arbitrary *) in - (n, coercion_flag, ast_of_constr true envpar t)) + (coercion_flag, (n, ast_of_constr true envpar t))) names types in Array.to_list array_idC;; @@ -146,7 +146,7 @@ let make_variable_ast name typ implicits = *) let make_variable_ast name typ implicits = (VernacAssumption - (AssumptionVariable, [name, constr_to_ast (body_of_type typ)])) + (AssumptionVariable, [false,(name, constr_to_ast (body_of_type typ))])) ::(implicits_to_ast_list implicits);; (* diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 2e49ec4e3d..233af4f7d0 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -2290,7 +2290,7 @@ let xlate_check = | _ -> xlate_error "xlate_check";; let build_constructors l = - let f (id,coe,c) = + let f (coe,(id,c)) = if coe then xlate_error "TODO: coercions in constructors" else CT_constr (xlate_ident id, xlate_constr c) in CT_constr_list (List.map f l) @@ -2912,6 +2912,7 @@ let xlate_vernac = CT_variable (xlate_var kind, b) *) | VernacAssumption (kind, b) -> + let b = List.map snd b in (* TODO: handle possible coercions *) CT_variable (xlate_var kind, cvt_vernac_binders b) (* | "Check", ((Varg_string (CT_string kind)) :: (c :: [])) -> @@ -2980,7 +2981,7 @@ let xlate_vernac = *) | (*Record from tactics/Record.v *) VernacRecord - (add_coercion, s, binders, c1, rec_constructor_or_none, field_list) -> + ((add_coercion, s), binders, c1, rec_constructor_or_none, field_list) -> let record_constructor = xlate_ident_opt rec_constructor_or_none in (* match rec_constructor_or_none with | None -> CT_coerce_NONE_to_ID_OPT CT_none |