diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/interface/name_to_ast.ml | 2 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 5 | ||||
| -rw-r--r-- | contrib/subtac/subtac.ml | 12 | ||||
| -rw-r--r-- | contrib/subtac/subtac_obligations.ml | 2 |
4 files changed, 11 insertions, 10 deletions
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index 9a503cfb5a..bbde91aac3 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -134,7 +134,7 @@ let implicits_to_ast_list implicits = let make_variable_ast name typ implicits = (VernacAssumption - ((Local,Definitional), + ((Local,Definitional),false,(*inline flag*) [false,([dummy_loc,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 6d52be45d9..639b4ae747 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1848,8 +1848,9 @@ let rec xlate_vernac = (xlate_defn kind, xlate_ident s, xlate_binder_list bl, cvt_optional_eval_for_definition c red_option, xlate_formula_opt typ_opt) - | VernacAssumption (kind, b) -> - CT_variable (xlate_var kind, cvt_vernac_binders b) + | VernacAssumption (kind,inline ,b) ->xlate_error "TODO: Parameter Inline" + (*inline : bool -> automatic delta reduction at fonctor application*) + (* CT_variable (xlate_var kind, cvt_vernac_binders b)*) | VernacCheckMayEval (None, numopt, c) -> CT_check (xlate_formula c) | VernacSearch (s,x) -> diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index ff5df49e39..eb1d5baf73 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -78,18 +78,18 @@ let _ = Detyping.set_detype_anonymous (fun loc n -> RVar (loc, id_of_string ("An let assumption_message id = Options.if_verbose message ((string_of_id id) ^ " is assumed") -let declare_assumption env isevars idl is_coe k bl c = +let declare_assumption env isevars idl is_coe k bl c nl = if not (Pfedit.refining ()) then let evm, c, typ = Subtac_pretyping.subtac_process env isevars (snd (List.hd idl)) [] (Command.generalize_constr_expr c bl) None in - List.iter (Command.declare_one_assumption is_coe k c) idl + List.iter (Command.declare_one_assumption is_coe k c nl) idl else errorlabstrm "Command.Assumption" (str "Cannot declare an assumption while in proof editing mode.") -let vernac_assumption env isevars kind l = - List.iter (fun (is_coe,(idl,c)) -> declare_assumption env isevars idl is_coe kind [] c) l +let vernac_assumption env isevars kind l nl = + List.iter (fun (is_coe,(idl,c)) -> declare_assumption env isevars idl is_coe kind [] c nl) l let subtac (loc, command) = @@ -123,8 +123,8 @@ let subtac (loc, command) = start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook - | VernacAssumption (stre,l) -> - vernac_assumption env isevars stre l + | VernacAssumption (stre,nl,l) -> + vernac_assumption env isevars stre l nl (*| VernacEndProof e -> subtac_end_proof e*) diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index e2101a2d9d..34758721fe 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -405,7 +405,7 @@ let admit_obligations n = match x.obl_body with None -> let x = subst_deps_obl obls x in - let kn = Declare.declare_constant x.obl_name (ParameterEntry x.obl_type, IsAssumption Conjectural) in + let kn = Declare.declare_constant x.obl_name (ParameterEntry (x.obl_type,false), IsAssumption Conjectural) in assumption_message x.obl_name; { x with obl_body = Some (mkConst kn) } | Some _ -> x) |