diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.ml4 | 18 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 4 |
2 files changed, 2 insertions, 20 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 835d66434..0f097f7e6 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -39,24 +39,6 @@ let loc_of_binder_let = function | LocalRawDef ((loc,_),_)::_ -> loc | _ -> dummy_loc -let rec mkCProdN loc bll c = - match bll with - | LocalRawAssum ((loc1,_)::_ as idl,t) :: bll -> - CProdN (loc,[idl,t],mkCProdN (join_loc loc1 loc) bll c) - | LocalRawDef ((loc1,_) as id,b) :: bll -> - CLetIn (loc,id,b,mkCProdN (join_loc loc1 loc) bll c) - | [] -> c - | LocalRawAssum ([],_) :: bll -> mkCProdN loc bll c - -let rec mkCLambdaN loc bll c = - match bll with - | LocalRawAssum ((loc1,_)::_ as idl,t) :: bll -> - CLambdaN (loc,[idl,t],mkCLambdaN (join_loc loc1 loc) bll c) - | LocalRawDef ((loc1,_) as id,b) :: bll -> - CLetIn (loc,id,b,mkCLambdaN (join_loc loc1 loc) bll c) - | [] -> c - | LocalRawAssum ([],_) :: bll -> mkCLambdaN loc bll c - let rec index_and_rec_order_of_annot loc bl ann = match names_of_local_assums bl,ann with | [_], (None, r) -> Some 0, r diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 3684074fd..ad42304ce 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -320,9 +320,9 @@ GEXTEND Gram constructor: [ [ id = identref; l = LIST0 binder_let; coe = of_type_with_opt_coercion; c = lconstr -> - (coe,(id,G_constr.mkCProdN loc l c)) + (coe,(id,mkCProdN loc l c)) | id = identref; l = LIST0 binder_let -> - (false,(id,G_constr.mkCProdN loc l (CHole loc))) ] ] + (false,(id,mkCProdN loc l (CHole loc))) ] ] ; of_type_with_opt_coercion: [ [ ":>" -> true |