diff options
author | 2001-01-24 16:20:28 +0000 | |
---|---|---|
committer | 2001-01-24 16:20:28 +0000 | |
commit | 2678739dcac301102dfeba7dfb9958d67f1cce0e (patch) | |
tree | bd820ae63d60e8745a9078c56d212e6388056da8 /toplevel | |
parent | 0b96cc38f52d67c657ab68ba1006f77bf5c2a0b6 (diff) |
Réorganisation suite ajout de constantes locales dans les Records
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1268 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/command.ml | 22 | ||||
-rw-r--r-- | toplevel/command.mli | 5 |
2 files changed, 9 insertions, 18 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 2055e5b8a..c4119ccbf 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -148,8 +148,7 @@ let interp_mutual lparams lnamearconstrs finite = (fun acc (id,_,l) -> id::(List.map fst l)@acc) [] lnamearconstrs in if not (list_distinct allnames) then error "Two inductive objects have the same name"; - let lrecnames = List.map (fun (x,_,_) -> x) lnamearconstrs - and nparams = List.length lparams + let nparams = List.length lparams and sigma = Evd.empty and env0 = Global.env() in let env_params, params = @@ -190,24 +189,19 @@ let interp_mutual lparams lnamearconstrs finite = mind_entry_lc = constrs }) (List.rev arityl) lnamearconstrs in - { mind_entry_finite = finite; mind_entry_inds = mispecvec }, - lrecnames + { mind_entry_finite = finite; mind_entry_inds = mispecvec } -let declare_mutual_with_eliminations mie lrecnames finite = +let declare_mutual_with_eliminations mie = + let lrecnames = + List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in let sp = declare_mind mie in if is_verbose() then pPNL(minductive_message lrecnames); - if finite then - for i = 0 to List.length lrecnames - 1 do - declare_eliminations sp i - done; + declare_eliminations sp; sp -let build_mutual_give_path lparams lnamearconstrs finite = - let mie, lrecnames = interp_mutual lparams lnamearconstrs finite in - declare_mutual_with_eliminations mie lrecnames finite - let build_mutual lparams lnamearconstrs finite = - let _ = build_mutual_give_path lparams lnamearconstrs finite in () + let mie = interp_mutual lparams lnamearconstrs finite in + let _ = declare_mutual_with_eliminations mie in () (* try to find non recursive definitions *) diff --git a/toplevel/command.mli b/toplevel/command.mli index 44bf29266..c0479acf6 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -30,10 +30,7 @@ val build_mutual : (identifier * Coqast.t) list -> (identifier * Coqast.t * (identifier * Coqast.t) list) list -> bool -> unit -val build_mutual_give_path : - (identifier * Coqast.t) list -> - (identifier * Coqast.t * (identifier * Coqast.t) list) list -> bool - -> section_path +val declare_mutual_with_eliminations : Declarations.mutual_inductive_entry -> section_path val build_recursive : (identifier * ((identifier * Coqast.t) list) * Coqast.t * Coqast.t) list |