diff options
| author | herbelin | 2000-09-10 07:13:23 +0000 |
|---|---|---|
| committer | herbelin | 2000-09-10 07:13:23 +0000 |
| commit | c0ff579606f2eba24bc834316d8bb7bcc076000d (patch) | |
| tree | e192389ccddcb9bb6f6e50039b4f31e6f5fcbc0b /toplevel/command.ml | |
| parent | ebfbb2cf101b83f4b3a393e68dbdfdc3bfbcaf1a (diff) | |
Ajout d'un LetIn primitif.
Abstraction de constr via kind_of_constr dans une bonne partie du code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@590 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 7da510029f..2a15741bf6 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -4,7 +4,7 @@ open Pp open Util open Options -open Generic +(*i open Generic i*) open Term open Declarations open Inductive @@ -201,7 +201,7 @@ let collect_non_rec = | _ -> [] (* nrec=[] for cofixpoints *) with Failure "list_chop" -> [] in - searchrec ((f,DOP2(Cast,def,body_of_type ar))::lnonrec) + searchrec ((f,mkCast (def,body_of_type ar))::lnonrec) (lf1@lf2) (ldef1@ldef2) (lar1@lar2) newlnv with Failure "try_find_i" -> (lnonrec, (lnamerec,ldefrec,larrec,nrec)) @@ -267,7 +267,7 @@ let build_recursive lnameargsardef = let _ = List.fold_left (fun subst (f,def) -> - let ce = { const_entry_body = Cooked (Generic.replace_vars subst def); + let ce = { const_entry_body = Cooked (replace_vars subst def); const_entry_type = None } in declare_constant f (ce,n); warning ((string_of_id f)^" is non-recursively defined"); @@ -333,7 +333,7 @@ let build_corecursive lnameardef = let _ = List.fold_left (fun subst (f,def) -> - let ce = { const_entry_body = Cooked (Generic.replace_vars subst def); + let ce = { const_entry_body = Cooked (replace_vars subst def); const_entry_type = None } in declare_constant f (ce,n); warning ((string_of_id f)^" is non-recursively defined"); |