diff options
| author | herbelin | 2000-05-22 13:10:03 +0000 |
|---|---|---|
| committer | herbelin | 2000-05-22 13:10:03 +0000 |
| commit | f9031792f714bb468c2dc8bfb49f34cfef44b27a (patch) | |
| tree | 7d67852c2ec622df3520ef08a71a63e9d55b2fd9 /toplevel | |
| parent | 2476b8a3397dccc8cadd7422929c844040ecc987 (diff) | |
Suite restructuration inductifs; changement nom module Constant en Declarations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@458 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 17 | ||||
| -rw-r--r-- | toplevel/discharge.ml | 2 | ||||
| -rw-r--r-- | toplevel/minicoq.ml | 2 | ||||
| -rw-r--r-- | toplevel/record.ml | 5 |
4 files changed, 11 insertions, 15 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 93426fde9b..9c56db03a5 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -6,7 +6,7 @@ open Util open Options open Generic open Term -open Constant +open Declarations open Inductive open Reduction open Tacred @@ -359,17 +359,12 @@ let build_scheme lnamedepindsort = (inductive_of_ident indid,dep,s)) lnamedepindsort in let n = NeverDischarge in - let listdecl = Indrec.build_indrec env0 sigma lrecspec in - let rec declare i = function - | fi::lf -> - let ce = - { const_entry_body = Cooked listdecl.(i); const_entry_type = None } - in - declare_constant fi (ce,n); - declare (i+1) lf - | _ -> () + let listdecl = Indrec.build_mutual_indrec env0 sigma lrecspec in + let rec declare decl fi = + let ce = { const_entry_body = Cooked decl; const_entry_type = None } + in declare_constant fi (ce,n) in - declare 0 lrecnames; + List.iter2 declare listdecl lrecnames; if is_verbose() then pPNL(recursive_message lrecnames) let start_proof_com s stre com = diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index aa1e1e96b8..1e8501f127 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -7,7 +7,7 @@ open Names open Sign open Generic open Term -open Constant +open Declarations open Inductive open Instantiate open Reduction diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml index 7af018585a..7df256f199 100644 --- a/toplevel/minicoq.ml +++ b/toplevel/minicoq.ml @@ -7,7 +7,7 @@ open Names open Generic open Term open Sign -open Constant +open Declarations open Inductive open Type_errors open Safe_typing diff --git a/toplevel/record.ml b/toplevel/record.ml index c4cc168d7d..8f3052441a 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -6,6 +6,7 @@ open Util open Names open Generic open Term +open Declarations open Declare open Coqast open Ast @@ -135,8 +136,8 @@ let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) = let ok = try let cie = - { Constant.const_entry_body = Constant.Cooked proj; - Constant.const_entry_type = None } in + { const_entry_body = Cooked proj; + const_entry_type = None } in (declare_constant fi (cie,NeverDischarge); true) with UserError(s,pps) -> ((warning_or_error coe |