diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-03-12 09:34:13 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-03-12 09:34:13 +0000 |
| commit | 9dae3bc45e05fc3be987f79b5098248a9d725ce2 (patch) | |
| tree | 1b16f0aeed55fdb19a4744567652ada9ff18c7b1 | |
| parent | afc56703587699447c7a29ba3ae0995d7f0a036b (diff) | |
debut let in
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1450 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/extraction/extraction.ml | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 8233b9f41..4da0bd19e 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -339,17 +339,23 @@ and extract_term c = | Tarity -> assert false (* Cf. precondition *) | Tprop -> Eprop) | IsConst (sp,_) -> - Emlterm (MLglob (ConstRef sp)) (* TODO eta-expansion *) + Emlterm (MLglob (ConstRef sp)) | IsMutConstruct (cp,_) -> - Emlterm (MLglob (ConstructRef cp)) + Emlterm (MLglob (ConstructRef cp)) (* TODO eta-expansion *) | IsMutCase _ -> failwith "todo" | IsFix _ -> failwith "todo" | IsLetIn (n, c1, t1, c2) -> - failwith "todo" - (*i (match get_arity env t1 with - | Some (Prop Null) -> *) + let id = id_of_name n in + let env' = push_rel (n,Some c1,t1) env in + (match get_arity env t1 with + | Some (Prop Null) -> + extract_rec env' ((Tprop,id)::ctx) c2 + | Some _ -> + failwith "todo" (* extract_rec env' *) + | _ -> + failwith "todo") | IsCast (c, _) -> extract_rec env ctx c | IsMutInd _ | IsProd _ | IsSort _ | IsVar _ @@ -390,7 +396,7 @@ and extract_constr_with_type c t = | Some _ -> (match extract_type genv [] c with | Tprop -> Eprop - | Tarity -> Emltype(Miniml.Tarity, [], []) (* any other arity *) + | Tarity -> Emltype (Miniml.Tarity, [], []) (* any other arity *) | Tmltype (t, sign, fl) -> Emltype (t, sign, fl)) | None -> extract_term c |