diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 17 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 2 |
2 files changed, 12 insertions, 7 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 46de560b46..30548d74d2 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -456,7 +456,8 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list) = (* Declare the notations for the recursive types pushed in local context*) let (rec_sign,arityl) = List.fold_left - (fun (env,arl) ((recname,_,_,arityc,_),_) -> + (fun (env,arl) ((recname,_,bl,arityc,_),_) -> + let arityc = prod_rawconstr arityc bl in let arity = interp_type sigma env0 arityc in (Environ.push_named (recname,None,arity) env, (arity::arl))) (env0,[]) lnameargsardef in @@ -479,7 +480,8 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list) = (Lib.cwd(),SectionLocalAssum arity, IsAssumption Definitional) in ()) lrecnames arityl; List.map2 - (fun ((_,_,_,_,def),_) arity -> + (fun ((_,_,bl,_,def),_) arity -> + let def = abstract_rawconstr def bl in interp_casted_constr sigma rec_sign def arity) lnameargsardef arityl with e -> @@ -521,14 +523,15 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list) = Metasyntax.add_notation_interpretation df [] c scope) notations let build_corecursive lnameardef = - let lrecnames = List.map (fun (f,_,_) -> f) lnameardef + let lrecnames = List.map (fun (f,_,_,_) -> f) lnameardef and sigma = Evd.empty and env0 = Global.env() in let fs = States.freeze() in let (rec_sign,arityl) = try List.fold_left - (fun (env,arl) (recname,arityc,_) -> + (fun (env,arl) (recname,bl,arityc,_) -> + let arityc = prod_rawconstr arityc bl in let arj = type_judgment_of_rawconstr Evd.empty env0 arityc in let arity = arj.utj_val in let _ = declare_variable recname @@ -540,8 +543,10 @@ let build_corecursive lnameardef = let arityl = List.rev arityl in let recdef = try - List.map (fun (_,arityc,def) -> - let arity = interp_constr sigma rec_sign arityc in + List.map (fun (_,bl,arityc,def) -> + let arityc = prod_rawconstr arityc bl in + let def = abstract_rawconstr def bl in + let arity = interp_constr sigma rec_sign arityc in interp_casted_constr sigma rec_sign def arity) lnameardef with e -> diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 8438e9b02b..f72c533e1e 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -154,7 +154,7 @@ let pr_new_syntax loc ocom = if !translate_file then msg (hov 0 (comment (fst loc) ++ com ++ comment (snd loc))) else - msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ com)); + msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com))); States.unfreeze fs; Constrintern.set_temporary_implicits_in []; Constrextern.set_temporary_implicits_out []; |