diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-12-03 22:48:37 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-12-03 22:48:37 +0000 |
| commit | f4f2c6d3221caa561a42468f0f9d46c3b80e1807 (patch) | |
| tree | 8b012faa6d7eab18f8823ed13799ff551aceeb12 /parsing | |
| parent | 6aae3bd0da8edc2ec5adcff7d44155e0a59597c6 (diff) | |
Remplacement de la dépendance de G_vernac en G_constr (source
d'incohérences dans les dépendances en l'absence de g_constr.mli) par
une dépendance en Topconstr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9409 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |