diff options
| author | Brian Campbell | 2019-03-01 12:14:45 +0000 |
|---|---|---|
| committer | Brian Campbell | 2019-03-01 12:14:45 +0000 |
| commit | 2e835b683c23aa4a63a9d5dac7628b0953be5f24 (patch) | |
| tree | b8ff62257f4c9b4d5789f45f1abcc9988585ae4e /src/pretty_print_coq.ml | |
| parent | 576fb915bc281ea8e59eba896e3404d2f85e918c (diff) | |
Coq tidying: remove old definition, complete a pattern match
Diffstat (limited to 'src/pretty_print_coq.ml')
| -rw-r--r-- | src/pretty_print_coq.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index d205e46b..d323d639 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -390,8 +390,6 @@ let rec count_bool_vars (NC_aux (nc,_)) = | NC_app (_,args) -> List.fold_left merge_bool_count KBindings.empty (List.map count_arg args) -type prop_dir = Implied_by | Implies | Iff - type atom_bool_prop = Bool_boring | Bool_complex of kinded_id list * n_constraint * n_constraint @@ -2746,6 +2744,9 @@ let rec doc_def unimplemented generic_eq_types def = | DEF_scattered sdef -> failwith "doc_def: shoulnd't have DEF_scattered at this point" | DEF_mapdef (MD_aux (_, (l,_))) -> unreachable l __POS__ "Coq doesn't support mappings" | DEF_pragma _ -> empty + | DEF_measure (id,_,_) -> unreachable (id_loc id) __POS__ + ("Termination measure for " ^ string_of_id id ^ + " should have been rewritten before backend") let find_exc_typ defs = let is_exc_typ_def = function |