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/record.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/record.ml')
| -rw-r--r-- | toplevel/record.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml index 9801045a2e..f3169a066a 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -4,7 +4,7 @@ open Pp open Util open Names -open Generic +(*i open Generic i*) open Term open Declarations open Declare @@ -127,14 +127,14 @@ let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) = print_id_list bad_projs; 'sTR " were not defined" >]); (None::sp_projs,fi::ids_not_ok,subst) end else - let p = mkLambda x rp2 (replace_vars subst ti) in + let p = mkLambda (x, rp2, replace_vars subst ti) in let branch = mk_LambdaCit newfs (VAR fi) in let ci = Inductive.make_case_info (Global.lookup_mind_specif (destMutInd r)) (Some PrintLet) [| RegularPat |] in let proj = mk_LambdaCit newps - (mkLambda x rp1 - (mkMutCaseA ci p (Rel 1) [|branch|])) in + (mkLambda (x, rp1, + mkMutCaseA ci p (Rel 1) [|branch|])) in let ok = try let cie = |