From 21bf57e0b7de37faa4991e136cf6f09cfbf4d0a3 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 22 Jul 2003 08:43:32 +0000 Subject: [PATCH] 1. Modificiations due to the change ot K.Aux 2. Assert false on Lambda with no name removed. Who generates them? --- helm/ocaml/cic_transformations/content2pres.ml | 4 ++-- helm/ocaml/cic_transformations/content_expressions.ml | 11 ++++++----- 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index dfb742810..2404fbea3 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -449,7 +449,7 @@ and proof2pres term2pres p = let module Con = Content in function Con.Aux n -> - P.Mtext ([],"aux " ^ string_of_int n) + P.Mtext ([],"aux " ^ n) | Con.Premise prem -> P.Mtext ([],"premise") | Con.Term t -> @@ -469,7 +469,7 @@ and proof2pres term2pres p = let inductive_arg,args_for_cases = (match conclude.Con.conclude_args with Con.Aux(n)::_::tl -> - let l1,l2 = split n tl in + let l1,l2 = split (int_of_string n) tl in let last_pos = (List.length l2)-1 in List.nth l2 last_pos,l1 | _ -> assert false) in diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml index bb062f9cc..da6eb714a 100644 --- a/helm/ocaml/cic_transformations/content_expressions.ml +++ b/helm/ocaml/cic_transformations/content_expressions.ml @@ -296,11 +296,12 @@ let acic2cexpr ids_to_inner_sorts t = Binder (Some id,binder,decl,acic2cexpr t)) | C.ACast (id,v,t) -> acic2cexpr v | C.ALambda (id,n,s,t) -> - (match n with - Cic.Anonymous -> assert false - | Cic.Name name -> - let decl = (name, acic2cexpr s) in - Binder (Some id,"Lambda",decl,acic2cexpr t)) + let name = + (match n with + Cic.Anonymous -> "_" + | Cic.Name name -> name) in + let decl = (name, acic2cexpr s) in + Binder (Some id,"Lambda",decl,acic2cexpr t) | C.ALetIn (id,n,s,t) -> (match n with Cic.Anonymous -> assert false -- 2.39.2