diff options
| author | herbelin | 2003-09-06 14:41:14 +0000 |
|---|---|---|
| committer | herbelin | 2003-09-06 14:41:14 +0000 |
| commit | d3407458889d4ba4ff6fbf465a92c86976c01ba5 (patch) | |
| tree | 8b72e3033d70b3e9e1a6c50c9d36cca7b252cba5 | |
| parent | 394d2954c31047ca87b0575a1eaff019b247b3d8 (diff) | |
Mise en place possibilité de définitions locales dans les paramètres des inductifs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4319 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/interface/name_to_ast.ml | 9 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 2 | ||||
| -rw-r--r-- | translate/ppvernacnew.ml | 2 |
3 files changed, 7 insertions, 6 deletions
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index ff361e8f4e..6e44f2b114 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -21,16 +21,17 @@ open Nametab open Vernacexpr;; open Decl_kinds;; open Constrextern;; +open Topconstr;; (* This function converts the parameter binders of an inductive definition, in particular you have to be careful to handle each element in the context containing all previously defined variables. This squeleton of this procedure is taken from the function print_env in pretty.ml *) let convert_env = - let convert_binder env (na, _, c) = - match na with - | Name id -> (id, extern_constr true env c) - | Anonymous -> failwith "anomaly: Anonymous variables in inductives" in + let convert_binder env (na, b, c) = + match b with + | Some b -> LocalRawDef ((dummy_loc,na), extern_constr true env b) + | None -> LocalRawAssum ([dummy_loc,na], extern_constr true env c) in let rec cvrec env = function [] -> [] | b::rest -> (convert_binder env b)::(cvrec (push_rel b env) rest) in diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 8d82da7e1f..72cf41ad45 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1547,7 +1547,7 @@ let xlate_vernac = let strip_mutind (s, notopt, parameters, c, constructors) = if notopt = None then CT_ind_spec - (xlate_ident s, cvt_vernac_binders parameters, xlate_formula c, + (xlate_ident s, xlate_binder_list parameters, xlate_formula c, build_constructors constructors) else xlate_error "TODO: Notation in Inductive" in CT_mind_decl diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index 0471d5d14a..f3a0798eff 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -659,7 +659,7 @@ pr_vbinders bl ++ spc()) (fun (env,params) d -> match d with | LocalRawAssum (nal,t) -> let t = Constrintern.interp_type sigma env t in - let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal + let ctx = list_map_i (fun i (_,na) -> (na,None,Term.lift i t)) 0 nal in let ctx = List.rev ctx in (Environ.push_rel_context ctx env, ctx@params) | LocalRawDef ((_,na),c) -> |