diff options
| author | soubiran | 2007-04-25 15:13:45 +0000 |
|---|---|---|
| committer | soubiran | 2007-04-25 15:13:45 +0000 |
| commit | 40425048feff138e6c67555c7ee94142452d1cae (patch) | |
| tree | b26134c830f386838f219b92a1c8960dd50c4287 /contrib/interface | |
| parent | 2c75beb4e24c91d3ecab07ca9279924205002ada (diff) | |
New keyword "Inline" for Parameters and Axioms for automatic
delta-reduction at fonctor application.
Example:
Module Type S.
Parameter Inline N : Set.
End S.
Module F (X:S).
Definition t := X.N.
End F.
Module M.
Definition N := nat.
End M.
Module G := F M.
Print G.t.
G.t = nat
: Set
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9795 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 | 5 |
2 files changed, 4 insertions, 3 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) -> |