diff options
| author | ppedrot | 2013-09-27 19:20:27 +0000 |
|---|---|---|
| committer | ppedrot | 2013-09-27 19:20:27 +0000 |
| commit | 11ca3113365639136cf65a74c345080a9434e69b (patch) | |
| tree | da263c149cd1e90bde14768088730e48e78e4776 /kernel/term_typing.ml | |
| parent | ee2f85396fa0cef65bc4295b5ac6c259e83df134 (diff) | |
Removing a bunch of generic equalities.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index ef0270e9d6..567511c93f 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -54,7 +54,7 @@ let handle_side_effects env body side_eff = let cname c = let name = string_of_con c in for i = 0 to String.length name - 1 do - if name.[i] = '.' || name.[i] = '#' then name.[i] <- '_' done; + if name.[i] == '.' || name.[i] == '#' then name.[i] <- '_' done; Name (id_of_string name) in let rec sub c i x = match kind_of_term x with | Const c' when eq_constant c c' -> mkRel i @@ -83,7 +83,7 @@ let infer_declaration ?(what="UNKNOWN") env dcl = match dcl with | DefinitionEntry c -> let ctx, entry_body = c.const_entry_secctx, c.const_entry_body in - if c.const_entry_opaque && c.const_entry_type <> None then + if c.const_entry_opaque && not (Option.is_empty c.const_entry_type) then let id = "infer_declaration " ^ what in let body_cst = Future.chain ~id entry_body (fun (body, side_eff) -> @@ -138,7 +138,7 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) = (* We try to postpone the computation of used section variables *) let hyps, def = match ctx with - | None when named_context env <> [] -> + | None when not (List.is_empty (named_context env)) -> (* No declared section vars, and non-empty section context: we must look at the body NOW, if any *) let ids_typ = global_vars_set_constant_type env typ in |