diff options
| author | Brian Campbell | 2018-09-17 17:01:35 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-09-17 17:03:00 +0100 |
| commit | 7c8bafec648d5fa57f13e4260198c4e4f03da31f (patch) | |
| tree | b0f2c4e0cd8c59908fa93821026c5dcef988c93f | |
| parent | 83478340bb5007443c57e9f1facd3322b9422b7f (diff) | |
Coq: fix types in aarch64_extras undefined_vector and casts for arguments
| -rw-r--r-- | aarch64/aarch64_extras.v | 2 | ||||
| -rw-r--r-- | src/pretty_print_coq.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/aarch64/aarch64_extras.v b/aarch64/aarch64_extras.v index 00ca8601..29e7198c 100644 --- a/aarch64/aarch64_extras.v +++ b/aarch64/aarch64_extras.v @@ -90,7 +90,7 @@ Definition undefined_string {rv e} (_:unit) : monad rv string e := returnm ""%st Definition undefined_unit {rv e} (_:unit) : monad rv unit e := returnm tt. Definition undefined_int {rv e} (_:unit) : monad rv Z e := returnm (0:ii). (*val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monad 'rv (list 'a) 'e*) -Definition undefined_vector {rv a e} len (u : a) : monad rv (list a) e := returnm (repeat (cons u nil) len). +Definition undefined_vector {rv a e} len `{ArithFact (len >= 0)} (u : a) : monad rv (vec a len) e := returnm (vec_init u len). (*val undefined_bitvector : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*) Definition undefined_bitvector {rv e} len `{ArithFact (len >= 0)} : monad rv (mword len) e := returnm (mword_of_int 0). (*val undefined_bits : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*) diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 1614d8de..45efa798 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1152,10 +1152,10 @@ let doc_exp, doc_let = let typ_from_fn = Env.expand_synonyms env typ_from_fn in (* TODO: more sophisticated check *) let () = - debug ctxt (lazy (" arg type found " ^ string_of_typ (general_typ_of arg))); + debug ctxt (lazy (" arg type found " ^ string_of_typ (typ_of arg))); debug ctxt (lazy (" arg type expected " ^ string_of_typ typ_from_fn)) in - let typ_of_arg = Env.expand_synonyms env (general_typ_of arg) in + let typ_of_arg = Env.expand_synonyms env (typ_of arg) in let typ_of_arg = expand_range_type typ_of_arg in let typ_of_arg' = match typ_of_arg with Typ_aux (Typ_exist (_,_,t),_) -> t | t -> t in let typ_from_fn' = match typ_from_fn with Typ_aux (Typ_exist (_,_,t),_) -> t | t -> t in |