diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-02-05 15:52:31 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-02-05 15:52:31 +0000 |
| commit | 7da87c68444558218bca2a3b070086712d727bcc (patch) | |
| tree | 75933829be7dec8c908a15131bb7195c3414b66c /contrib/interface | |
| parent | 36c0dbed2d5035c77cd1f2780269b95dc49a621c (diff) | |
Ajout du traducteur
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3664 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/name_to_ast.ml | 2 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index 039127cc5..4150a0948 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -159,7 +159,7 @@ let make_variable_ast name typ implicits = let make_definition_ast name c typ implicits = VernacDefinition (Global, name, DefineBody ([], None, (constr_to_ast c), Some (constr_to_ast (body_of_type typ))), - (fun _ _ -> ())) + (fun _ _ -> ()),GDefinition) ::(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 e9995e559..de4821eee 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1468,11 +1468,11 @@ let xlate_vernac = xlate_error "TODO: VernacStartTheoremProof" | VernacSuspend -> CT_suspend | VernacResume idopt -> CT_resume (xlate_ident_opt (option_app snd idopt)) - | VernacDefinition (k,s,ProveBody (bl,typ),_) -> + | 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_formula typ)) - | VernacDefinition (kind,s,DefineBody(bl,red_option,c,typ_opt),_) -> + | VernacDefinition (kind,s,DefineBody(bl,red_option,c,typ_opt),_,_) -> CT_definition (xlate_defn kind, xlate_ident s, xlate_binder_list bl, cvt_optional_eval_for_definition c red_option, |