diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-11 07:03:51 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-11 07:03:51 +0000 |
| commit | 1d152b81fe952a0ed20468e2e5d3d7063aa54d07 (patch) | |
| tree | 9c72bbf488ca77365318e7f4458bb05b4c81cdf0 /contrib | |
| parent | df9a4f1ae642cbbd2a6f1a3b82ad8169b7ec5ae6 (diff) | |
Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pour
les définitions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2852 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/interface/name_to_ast.ml | 6 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 13 |
2 files changed, 12 insertions, 7 deletions
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index 5ba5e0e7e..8c6293ae2 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -161,9 +161,9 @@ let make_definition_ast name c typ implicits = (implicits_to_ast_list implicits);; *) let make_definition_ast name c typ implicits = - VernacDefinition (Definition, name, None, - (ope("CAST", [(constr_to_ast c);(constr_to_ast (body_of_type typ))])), - None, (fun _ _ -> ())) + VernacDefinition (Definition, name, DefineBody ([], None, + (constr_to_ast c), Some (constr_to_ast (body_of_type typ))), + (fun _ _ -> ())) ::(implicits_to_ast_list implicits);; (* This function is inspired by print_constant *) diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 233af4f7d..d1af58df7 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -2582,7 +2582,7 @@ let xlate_vernac = | "FOCUS", [Varg_int n] -> CT_focus (CT_coerce_INT_to_INT_OPT n) | "UNFOCUS", [] -> CT_unfocus *) - | VernacStartProof (_, None, c, _, _) -> + | VernacGoal c -> CT_coerce_THEOREM_GOAL_to_COMMAND (CT_goal (xlate_constr c)) | VernacAbort (Some id) -> CT_abort(ctf_ID_OPT_OR_ALL_SOME(xlate_ident id)) | VernacAbort None -> CT_abort ctv_ID_OPT_OR_ALL_NONE @@ -2869,9 +2869,9 @@ let xlate_vernac = | "StartProof", ((Varg_string (CT_string kind)) :: ((Varg_ident s) :: (c :: []))) -> *) - | VernacStartProof (kind, Some s, c, _, _) -> + | VernacStartTheoremProof (k, s, c, _, _) -> CT_coerce_THEOREM_GOAL_to_COMMAND( - CT_theorem_goal (xlate_defn_or_thm kind, xlate_ident s,xlate_constr c)) + CT_theorem_goal (CT_coerce_THM_to_DEFN_OR_THM (xlate_thm k), xlate_ident s,xlate_constr c)) (* | (*My attempt: suspend and resume as separate nodes *) "SUSPEND", [] -> CT_suspend @@ -2898,7 +2898,12 @@ let xlate_vernac = (CT_coerce_SORT_TYPE_to_FORMULA b), None | _ -> assert false in *) - | VernacDefinition (kind,s,red_option,c,typ_opt,_) -> + | VernacDefinition (k,s,ProveBody (bl,typ),_) -> + if bl <> [] then xlate_error "TODO: Def bindings"; + CT_coerce_THEOREM_GOAL_to_COMMAND( + CT_theorem_goal (CT_coerce_DEFN_to_DEFN_OR_THM (xlate_defn k), xlate_ident s,xlate_constr typ)) + | VernacDefinition (kind,s,DefineBody(bl,red_option,c,typ_opt),_) -> + if bl <> [] then xlate_error "TODO: Def bindings"; CT_definition (xlate_defn kind, xlate_ident s, cvt_optional_eval_for_definition c red_option, |